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
2020-11-25
Separate interning and pretyping of universes
Gaëtan Gilbert
2020-11-20
A step towards supporting pattern cast deeplier.
Hugo Herbelin
2020-11-20
Add preliminary support for notations with large class (non-recursive) binders.
Hugo Herbelin
2020-11-16
Syntax for specifying cumulative inductives
Gaëtan Gilbert
2020-10-30
Renaming Numeral into Number
Pierre Roux
2020-10-10
Add location in existential variable names (CEvar/GEvar).
Hugo Herbelin
2020-10-10
Adding and using locations on identifiers in constr_expr where they were miss...
Hugo Herbelin
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-07-03
Fix #11121: Simultaneous definition of term and notation in custom grammar
Maxime Dénès
2020-03-22
Centralizing all kinds of numeral string management in numTok.ml.
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-22
Making structure of type "tolerability" and related clearer.
Hugo Herbelin
2020-02-19
Addressing #6082 and #7766 (overriding format of notation).
Hugo Herbelin
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
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
