aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Improving error message when applying rewrite to an expression which is not a...Hugo Herbelin
2014-08-18Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-07In Hipattern: some functions not working modulo evar instantiation.Arnaud Spiwack
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-08-01Remove spurious [1] in equality.ml.Arnaud Spiwack
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-24Fix program cases and inversion tactic to correctly record universe constraints.Matthieu Sozeau
2014-06-23Removing opens to Clenvtac to track its use more easily.Pierre-Marie Pédrot
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-05-31Fixing introduction patterns * and ** when used in a branch so that they do n...Hugo Herbelin
2014-05-31Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:31:51 +0000