aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
Commit message (Expand)AuthorAge
* Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
* A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar 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
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
* Fixing bug #2724 (using notations with binders in cases patternsGravatar herbelin2012-03-20
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
* Noise for nothingGravatar pboutill2012-03-02
* In the syntax of pattern matching, "in" clauses are patterns.Gravatar pboutill2012-02-29
* Boolean Option Patterns CompatibilityGravatar pboutill2012-01-19
* Parameters in pattern first step.Gravatar pboutill2012-01-16
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Quick improvement of some error messages related to module applicationGravatar herbelin2011-08-30
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
* Rather quick hack to avoid using notations involving "Type" whenGravatar herbelin2011-06-12
* Annotations at functor applications:Gravatar letouzey2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16