| Age | Commit message (Collapse) | Author |
|---|
|
Actual documentation was interpreted as a comment.
|
|
|
|
of a match.
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: SkySkimmer
|
|
|
|
mixed terms and pattern
Reviewed-by: ejgallego
|
|
Reviewed-by: jfehrle
|
|
|
|
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
a correct typing environment
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Prefer the term 'solver' to 'decision procedure'.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Added Changelog
|
|
|
|
As noted by Hugo Herbelin, Dec is rather used for "decidable".
|
|
As suggested by Jim Fehrle while reviewing #12218
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
|
|
|
|
|
|
|
|
|
|
|
