aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
AgeCommit message (Expand)Author
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
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-09-02Removing more association lists in Constrintern.ppedrot
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
2013-06-25Useless use of maps in constr internalizing.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-19Dir_path --> DirPathletouzey
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-11-25More equality functionsppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10local variables can have implicits locallypboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2011-02-10More comments and less doublons in some mlipboutill
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:16:34 +0000