aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/constrexpr.mli
Commit message (Expand)AuthorAge
* Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
* Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: added to the "Constrexpr.CCases" variant.Gravatar Matej Kosik2016-01-11
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | COMMENTS: added to some variants of the "Constrexpr.prim_token" 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
* 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
* - 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
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 11:00:05 +0000