aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/glob_term.mli
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: added to some variants of "Glob_term.glob_constr" type.Gravatar Matej Kosik2015-12-18
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Ltac's [uconstr] values now use the identifier context to give names to binders.Gravatar Arnaud Spiwack2014-09-05
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* Correcting a comment in pattern-matching compilation.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Glob_term: minor formattingGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29