aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.mli
Commit message (Expand)AuthorAge
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
* [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
* [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\
* \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \
| * | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| | * More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | * Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| |/
* / Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
|/
* Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
| * Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * Merging glob_binder and glob_decl.Gravatar Hugo Herbelin2017-03-24
| * Cleaning phase around local binder at glob level:Gravatar Hugo Herbelin2017-03-24
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
* Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Function now supports puniveresGravatar jforest2015-04-14
* Update headers.Gravatar Maxime Dénès2015-01-12
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Revert the change in Constrintern introduced by "Add a type of untyped term t...Gravatar Arnaud Spiwack2014-08-06
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* Faster uconstr.Gravatar Arnaud Spiwack2014-08-01
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Useless use of maps in constr internalizing.Gravatar ppedrot2013-06-25
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 13:40:52 +0000