| Age | Commit message (Expand) | Author |
|---|
| 2017-01-26 | Fixing #5326 (anomaly on some unsupported case of 'pat). | Hugo Herbelin |
| 2016-10-12 | Shorter message for "Test Asymmetric Patterns". | Hugo Herbelin |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-04-27 | Reformatting + removal of some useless data + some cut-elimination | Hugo Herbelin |
| 2016-03-13 | Supporting "(@foo) args" in patterns, where "@foo" has no arguments. | Hugo Herbelin |
| 2016-03-12 | A more explicit name to the asymmetric boolean flag. | Hugo Herbelin |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-13 | Fixing #4467 (continued). | Hugo Herbelin |
| 2016-01-12 | Fixing #4467 (missing shadowing of variables in cases pattern). | Hugo Herbelin |
| 2016-01-11 | CLEANUP: removing unused field | Matej Kosik |
| 2015-12-18 | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified | Matej Kosik |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-06-17 | Fixing #3292 (locations of notations shifted by 1 in glob files in trunk). | Hugo Herbelin |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-02 | Removing more association lists in Constrintern. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (interp) | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-14 | Internalization of pattern is done in two phases. | pboutill |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-05-30 | More uniformisation in Pp.warn functions. | ppedrot |
| 2012-05-29 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | Stuff about notation_constr (ex-aconstr) now in notation_ops.ml | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-05-15 | Notations are back in the "in" clause of pattern matching. | pboutill |
| 2012-04-12 | "A -> B" is a notation for "forall _ : A, B". | pboutill |
| 2012-04-06 | Fixing a few bugs (see #2571) related to interpretation of multiple binders | herbelin |
| 2012-03-20 | Fixing bug #2724 (using notations with binders in cases patterns | herbelin |
| 2012-03-02 | Glob_term.predicate_pattern: No number of parameters with letins. | pboutill |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-02-29 | In the syntax of pattern matching, "in" clauses are patterns. | pboutill |
| 2012-01-20 | Notations with binders: Accepting using notations for functional terms | herbelin |
| 2012-01-19 | Boolean Option Patterns Compatibility | pboutill |
