index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrexpr.ml
Age
Commit message (
Expand
)
Author
2019-08-19
[api] Move handling of variable implicit data to impargs
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-16
binder_kind Generalized: remove 1st arg as it's always Implicit
Gaëtan Gilbert
2019-04-16
[ast] [constrexpr] Make recursion_order_expr an AST node.
Emilio Jesus Gallego Arias
2019-04-16
Clean the representation of recursive annotation in Constrexpr
Maxime Dénès
2019-04-02
Add parsing of decimal constants (e.g., 1.02e+01)
Pierre Roux
2019-04-02
Rename raw_natural_number to raw_numeral
Pierre Roux
2019-04-01
Replace type sign = bool with SPlus | SMinus
Pierre Roux
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-10-02
Revert #6651: Use r.(p) syntax to print primitive projections
Maxime Dénès
2018-07-29
Adding support for custom entries in notations.
Hugo Herbelin
2018-06-18
Remove reference name type.
Maxime Dénès
2018-06-12
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
