aboutsummaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
AgeCommit message (Expand)Author
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Shorter message for "Test Asymmetric Patterns".Hugo Herbelin
2016-09-21Fix an error-prone error API.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-04-27Reformatting + removal of some useless data + some cut-eliminationHugo Herbelin
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Fixing #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-01-12Update headers.Maxime Dénès
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-06-17Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).Hugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-02Removing more association lists in Constrintern.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-18Unset Asymmetric Patternspboutill
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-06-04Replacing some str with strbrkppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:34:40 +0000