index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrexpr_ops.ml
Age
Commit message (
Expand
)
Author
2021-04-23
Merge PR #13965: [abbreviation] user syntax to set interp scope of argument
Pierre-Marie Pédrot
2021-04-07
cleanup: less exceptions, removal of try_interp_name_alias
Enrico Tassi
2021-03-30
Remove the :> type cast
Jim Fehrle
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-12
Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...
Pierre-Marie Pédrot
2020-11-04
Moving interpretation of user-level universes in constrintern.ml.
Hugo Herbelin
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-05-16
Merge PR #11566: [misc] Better preserve backtraces in several modules
Pierre-Marie Pédrot
2020-05-15
[misc] Better preserve backtraces in several modules
Emilio Jesus Gallego Arias
2020-05-09
Add hexadecimal numerals
Pierre Roux
2020-04-06
Fix #11934 equality on constrexpr ignores instances of explicit applications
Gaëtan Gilbert
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-19
Addressing #6082 and #7766 (overriding format of notation).
Hugo Herbelin
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
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-01
Replace type sign = bool with SPlus | SMinus
Pierre Roux
2018-12-30
Fixing an interpretation bug of the "in" clause of "match".
Hugo Herbelin
2018-12-18
Fixes #9229 (Infix not robust wrt choice of variable names).
Hugo Herbelin
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-28
[options] New helper for creation of boolean options plus reference.
Emilio Jesus Gallego Arias
2018-11-23
s/let _ =/let () =/ in some places (mostly goptions related)
Gaëtan Gilbert
2018-10-05
Documenting constr_expr constructors; adding smart CLam/CProd.
Hugo Herbelin
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] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-30
[api] Remove deprecated objects in engine / interp / library
Emilio Jesus Gallego Arias
2018-03-09
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-20
Adding general support for irrefutable disjunctive patterns.
Hugo Herbelin
2018-02-20
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-01-30
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2017-12-12
Removing cumbersome location in multiple patterns.
Hugo Herbelin
2017-11-23
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-19
[parser] Remove unnecessary statically initialized hook.
Emilio Jesus Gallego Arias
[next]
