aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-04-27Rewriting [lapply] tactic in the new monad.Pierre-Marie Pédrot
2014-04-27Giving true proof-terms in inversion instead of metas.Pierre-Marie Pédrot
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-24Writing tclABSTRACT in the new monad. In particular the unsafe status is nowPierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-22Removing the compatibility layer from Leminv. Also removed an undocumentedPierre-Marie Pédrot
2014-04-22Using the new monad tactic in Inv.Pierre-Marie Pédrot
2014-04-22Removing tactic compatibility layer from Elim.Pierre-Marie Pédrot
2014-04-22Small code cleaning in Tacticals.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-04-20Fixing bug #3285.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
2014-04-06Removing unused functions in Refiner.Pierre-Marie Pédrot
2014-04-04Closing bug #3164Julien Forest
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-28Using the new refine interface to define ML tactics.Pierre-Marie Pédrot
2014-03-28Define Tactics.bring_hyps in the new monad.Pierre-Marie Pédrot
2014-03-27Removing tactic compatibility layer from Eqdecide.Pierre-Marie Pédrot
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-26Removing tactic compatibility layer from Inv.Pierre-Marie Pédrot
2014-03-26Adding an interface to Eqdecide and putting the grammar rules in a dedicatedPierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-19Using non-normalized goals in tactic interpretation.Pierre-Marie Pédrot
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
2014-03-17Fix test-suite 2255.vPierre Boutillier
2014-03-07Useless tactic bindings in Tacticals.Pierre-Marie Pédrot
2014-03-07Tentative fix for a very strange pervasive equality in Auto.Pierre-Marie Pédrot
2014-03-07Fixing generic equality in Auto.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Fixing pervasive equalities. In particular, I removed the code that deletedPierre-Marie Pédrot
2014-03-03Term dnets do no need to contain the afferent constr pattern in their nodes.Pierre-Marie Pédrot
2014-03-03Removing Termdn, and putting the relevant code in Btermdn. The current TermdnPierre-Marie Pédrot
2014-03-03Extruding code not depending of the functor argument in Termdn.Pierre-Marie Pédrot
2014-03-03Replacing arguments of Trie by a cancellable monoid.Pierre-Marie Pédrot
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-03-01Removing a fishy use of pervasive equality in Ltac backtrace printing.Pierre-Marie Pédrot
2014-02-28Removing Pervasives.compare in Termdn.Pierre-Marie Pédrot
2014-02-27Tacinterp: more refactoring.Arnaud Spiwack
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-27Remove unsafe code (Obj.magic) in Tacinterp.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:44:33 +0000