aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2014-05-06Fixes after rebase. The use of pf_constr_of_global is problematic in presence...Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-30Trying to improve the error messages of injection.Maxime Dénès
2014-04-29Injection: do not fail when arguments have sort Prop.Maxime Dénès
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
2014-03-27Cosmetic changes in Equality.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Inv.Pierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-17Fix test-suite 2255.vPierre Boutillier
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02Clean up a warning.aspiwack
2013-11-02Cleanup of comments.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-10-05Fixing potential evar leak in Equality.ppedrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-07-10Continuing r16621 on injection intro-patterns:herbelin
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-06-02Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anherbelin
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-10Equality: avoid some unprotected List.nth (fix #2837)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 23:55:47 +0000