aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
AgeCommit message (Expand)Author
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-02-05Make Program a regular attributeMaxime Dénès
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-10-31Fixes rest of #3468 (tactic-in-term was not respecting scopes).Hugo Herbelin
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20More precise explanation when a notation is not reversible for printing.Hugo Herbelin
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Maxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-05-31Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
2017-05-31More precise on preventing clash between bound vars name and hidden impargs.Hugo Herbelin
2017-05-31Fixing a failure to interpret some local implicit arguments in Inductive.Hugo Herbelin
2017-05-29Cleanup: removal of constr_of_global.Matthieu Sozeau
2017-05-03Allowing to pass arbitrary data in internalization environments.Pierre-Marie Pédrot
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-24Merging glob_binder and glob_decl.Hugo Herbelin
2017-03-24Cleaning phase around local binder at glob level:Hugo Herbelin
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2016-10-04Quick fix to #4595 (making notations containing "ltac:" unused for printing).Hugo Herbelin
2016-02-28Printing notations: Cleaning in anticipation of fixing #4592.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-26Documenting a bit more interpretation functions in passing.Hugo Herbelin
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-04-14Function now supports puniveresjforest
2015-01-12Update headers.Maxime Dénès
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-08-06Revert the change in Constrintern introduced by "Add a type of untyped term t...Arnaud Spiwack
2014-08-02Better struture for Ltac internalization environments in Constrintern.Pierre-Marie Pédrot
2014-08-01Faster uconstr.Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 03:16:15 +0000