aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
AgeCommit message (Expand)Author
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-07cleanup: less exceptions, removal of try_interp_name_aliasEnrico Tassi
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-04Adding a typed interpretation of patterns.Hugo Herbelin
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-09-30interp_context_evars: removed unused [shift] argumentGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:38:17 +0000