aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
AgeCommit message (Expand)Author
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-04-15Making type interning_data abstract in constrintern.ml.Hugo Herbelin
2020-03-31Remove check_hidden_implicit_parameters (not needed anymore)Gaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-03Remove constrintern global_level dead codeGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Merge PR #10226: Simplify implicit_quantifiersEmilio Jesus Gallego Arias
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:55:09 +0000