As the first major circuit proofs using cava2, this also involved making some infrastructure improvements:
Circuit type notations were globally Opened in the Types.v file, meaning that anyone importing that file (even transitively) couldn't disable them. They directly conflict with list notations, so this was problematic. Instead, I've used Bind Scope to make Coq automatically interpret things it knows are types in circuit_type_scope. The previous behavior can be recreated using Local Open Scope circuit_type_scope, but in practice the Bind Scope was enough in most places.
Moved the various primitive circuits out of PrimitiveNotations so that it's possible to not import PrimitiveNotations (in proofs, I find circuit notations are unhelpful because I just translate it all into Gallina immediately anyway) and not have everything prefixed by PrimitiveNotations.
As the first major circuit proofs using cava2, this also involved making some infrastructure improvements:
Opened in theTypes.vfile, meaning that anyone importing that file (even transitively) couldn't disable them. They directly conflict with list notations, so this was problematic. Instead, I've usedBind Scopeto make Coq automatically interpret things it knows aretypes incircuit_type_scope. The previous behavior can be recreated usingLocal Open Scope circuit_type_scope, but in practice theBind Scopewas enough in most places.PrimitiveNotationsso that it's possible to not importPrimitiveNotations(in proofs, I find circuit notations are unhelpful because I just translate it all into Gallina immediately anyway) and not have everything prefixed byPrimitiveNotations.