| Age | Commit message (Expand) | Author |
|---|
| 2016-03-04 | Uniformizing the parsing of argument scopes in Ltac. | Pierre-Marie Pédrot |
| 2016-02-24 | Removing the METAIDENT token, as it is not used anymore. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 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-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin |
| 2015-10-07 | Record fields accept an optional final semicolon separator. | Pierre-Marie Pédrot |
| 2015-10-07 | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau |
| 2015-07-01 | Notation: use same level for "@" in constr: and pattern: (Close: #4272) | Enrico Tassi |
| 2015-04-20 | Inlining "fun" and "forall" tokens in parser, so that alternative notations for | Hugo Herbelin |
| 2015-02-12 | Fixing #3982 (conflict with max notation for universes). | Hugo Herbelin |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-10-13 | Parsing of "?[" as two tokens (makes ssr compile). | Enrico Tassi |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-13 | Checking typability of evar instances. Using ";" to separate bindings | Hugo Herbelin |
| 2014-09-12 | Parsing evar instances. | Hugo Herbelin |
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-04 | - Better parsing and printing of named universes: Type{ident} and foo@{(ident... | Matthieu Sozeau |
| 2014-06-04 | - Allow parsing of @const@{instance} for specifying universe instances of pol... | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-11-27 | Actually adding the grammar entry to handle tactics in terms. | Pierre-Marie Pédrot |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-10-02 | avoid referring to Term in constrexpr.mli and glob_term.mli | letouzey |
| 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-05-29 | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey |
| 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 | 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-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-02 | Noise for nothing | pboutill |
| 2012-02-29 | In the syntax of pattern matching, "in" clauses are patterns. | pboutill |
| 2012-01-19 | Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}. | msozeau |
| 2011-07-22 | Add a syntax entry for fully applied constructor pattern | pboutill |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-05 | Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notation | herbelin |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-30 | r13359 continued: removed native treatment for λ (lambda) and Π (Pi) | herbelin |
