aboutsummaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
AgeCommit message (Expand)Author
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-01Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-19Fix bug #5476: Ltac has an inconsistent view of hypotheses.Pierre-Marie Pédrot
2017-04-13Silence a few OCaml warnings.Guillaume Melquiond
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Fix interpretation of Ltac patterns episode 2.Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Intern names bound in match patternsTej Chajed
2017-02-14Quick hack to fix interpretation of patterns in Ltac.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Tactic_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Patternops API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio 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-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-04-22Fixing non exhaustive pattern-matching.Hugo Herbelin
2015-04-21Fixing #3383 (a "return" clause without an "in" clause is not enoughHugo Herbelin
2015-04-09Really fix constr_of_pattern and bugs #3590 and #4120 byMatthieu Sozeau
2015-04-09Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...Matthieu Sozeau
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-03Fixing #3623 (unbound evars in types in a call to "change with").Hugo Herbelin
2014-10-02Completing fixing order of parameters when translating fromHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:27:28 +0000