aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
Commit message (Expand)AuthorAge
* 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
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* 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
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* 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
* Glob_term now mli-only, operations now in Glob_opsGravatar 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 a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* 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
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
* Boolean Option Patterns CompatibilityGravatar pboutill2012-01-19
* Parameters in pattern first step.Gravatar pboutill2012-01-16
* Fixing amazing loop when using eta-expansion in pattern-matching forGravatar herbelin2011-12-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
* Make Notation works with anonymous-level "Type".Gravatar herbelin2011-06-08
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
* 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
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fixed a bug introduced (r13316/r13329) in the printing of notationsGravatar herbelin2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22