aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.mli
Commit message (Expand)AuthorAge
* 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
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
* More equality functionsGravatar ppedrot2012-11-25
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Added new command "Set Parsing Explicit" for deactivating parsing (andGravatar herbelin2012-01-20
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* local variables can have implicits locallyGravatar pboutill2011-02-10
* Data structure telling implicits of local variables is a map in theGravatar pboutill2011-02-10
* More comments and less doublons in some mliGravatar pboutill2011-02-10
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22