[ ] documentation on transformations : explanations + coqdoc
Miscellanous
[x] sniper_no_check
[x] snipe parametric : definitions and inductive types we do not want to unfold
[x] port to coq-8.14
[x] port to coq-8.15
Improvements of existing transformations
Inductives
[x] Projections used to state that an element of an inductive type is one of the constructors: their definitions prove injectivity of constructors -> use them also for this property?
Monomorphization
[x] Heuristics to generate fewer instances
Pattern matching/if
[x] Translation of pattern matching on non dependent expressions
[ ] Deal with the definitions generated in the translation
[x] Dependent pattern matching on expressions
[ ] Translations in hypotheses and in the goal
Misc
[ ] Allow snipe to take as arguments a list of definitions and inductives not to unfolded, to be added to prod_of_symb and prod_types.
[ ] Add sig to the inductives not to be unfolded.
Future transformations
[x] Inductive predicates
[ ] Skolemization
Global improvements
[ ] where to use trakt in the strategy
[ ] code organization
Users
[ ] FreeSpec
[x] dependent pattern matching
[ ] bug fix
[ ] Michelson: goals of the form (exists y, f x = Some y) <-> (exists y, ...) (with nested existentials)
Release 1.0
with-trakt(dependent on SMTCoq)Miscellanous
sniper_no_checksnipeparametric : definitions and inductive types we do not want to unfoldImprovements of existing transformations
Inductives
Projections used to state that an element of an inductive type is one of the constructors: their definitions prove injectivity of constructors -> use them also for this property?Monomorphization
Pattern matching/if
Misc
snipeto take as arguments a list of definitions and inductives not to unfolded, to be added toprod_of_symbandprod_types.sigto the inductives not to be unfolded.Future transformations
Global improvements
traktin the strategyUsers