aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
Commit message (Expand)AuthorAge
* Shorter message for "Test Asymmetric Patterns".Gravatar Hugo Herbelin2016-10-12
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
* Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| * Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).Gravatar Hugo Herbelin2014-06-17
* 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