aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2014-05-18When discrimination is not possible, try to project.Maxime Dénès
2014-05-18Suggest Set Injection On Proofs in error message for injection.Maxime Dénès
2014-05-18Restored old behavior of injection on proofs by default.Maxime Dénès
2014-05-09Code cleaning & factorizing functions in Equality.Pierre-Marie Pédrot
2014-05-08Encapsulating some clausenv uses. This simplifies the control flow of somePierre-Marie Pédrot
2014-05-08Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Hugo Herbelin
2014-05-08Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Hugo Herbelin
2014-05-08Simplification and improvement of "subst x" in such a way that itHugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 13:36:34 +0000