Engine: rework global name representation#1199

Merged

W95Psp merged 21 commits intomainfrom rework-name-repr

Jan 30, 2025

+3,682-1,908

Commits on Jan 30, 2025

Revert "New test snapshot."
maximebuyse
committed
Revert "Rename trait methods in bundles for all backends, but include them only for fstar (hack)."
maximebuyse
committed
Revert "Move trait methods in cyclic dependencies bundling."
maximebuyse
committed
feat(ocaml): derive more for types

W95Psp
authored and
maximebuyse
committed
Complete redesign of concrete identifiers

W95Psp
authored and
maximebuyse
committed
refactor: make inline lib require no new concrete identifiers

W95Psp
authored and
maximebuyse
committed
Remove dummy method in opaque trait impls.
maximebuyse
committed
Keep renamings for sub-idents that are NOT anonymous.
maximebuyse
committed
Fix clash of names between enums and structs in bundles.
maximebuyse
committed
Avoid importing constructors from bundles when they don't exist.
maximebuyse
committed
Avoid disambiguating fields of the same struct.
maximebuyse
committed
Allow type aliases in concrete idents.
maximebuyse
committed
We shouldn't produce aliases for Quote items in bundles.
maximebuyse
committed
Make sure refinement types end up in their original module.
maximebuyse
committed
Correct origin for quote items.
maximebuyse
committed
Lower-case prefix for anonymous constants.
maximebuyse
committed
Test snapshots for new naming.
maximebuyse
committed
Adapt core lib to new naming.
maximebuyse
committed
Better documentation for new naming.
maximebuyse
committed
misc(engine): drop stale comment

W95Psp
authored and
maximebuyse
committed
Fix proverif backend with new naming.
maximebuyse
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Engine: rework global name representation#1199

Commits on Jan 30, 2025

Revert "New test snapshot."

Revert "Rename trait methods in bundles for all backends, but include them only for fstar (hack)."

Revert "Move trait methods in cyclic dependencies bundling."

feat(ocaml): derive more for types

Complete redesign of concrete identifiers

refactor: make inline lib require no new concrete identifiers

Remove dummy method in opaque trait impls.

Keep renamings for sub-idents that are NOT anonymous.

Fix clash of names between enums and structs in bundles.

Avoid importing constructors from bundles when they don't exist.

Avoid disambiguating fields of the same struct.

Allow type aliases in concrete idents.

We shouldn't produce aliases for Quote items in bundles.

Make sure refinement types end up in their original module.

Correct origin for quote items.

Lower-case prefix for anonymous constants.

Test snapshots for new naming.

Adapt core lib to new naming.

Better documentation for new naming.

misc(engine): drop stale comment

Fix proverif backend with new naming.