aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_constr.ml4
Commit message (Expand)AuthorAge
* Parsing of "?[" as two tokens (makes ssr compile).Gravatar Enrico Tassi2014-10-13
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
* - Allow parsing of @const@{instance} for specifying universe instances of pol...Gravatar Matthieu Sozeau2014-06-04
* - 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
* Actually adding the grammar entry to handle tactics in terms.Gravatar Pierre-Marie Pédrot2013-11-27
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* 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
* Strongly reduce the dependencies of grammar.cma, modulo two hacksGravatar letouzey2012-05-29
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* Noise for nothingGravatar pboutill2012-03-02
* In the syntax of pattern matching, "in" clauses are patterns.Gravatar pboutill2012-02-29
* Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.Gravatar msozeau2012-01-19
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationGravatar herbelin2011-03-05
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* r13359 continued: removed native treatment for λ (lambda) and Π (Pi)Gravatar herbelin2010-07-30
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Some dead code removal + cleanupsGravatar letouzey2009-04-08