aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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
preserved.
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
variant of the Derive Inversion command which took the current goal as the targeted inductive. It was unused in the contribs and it seemed rather bad from the STM point of view, as it generated a lemma inside a proof.
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
that should be changed anyway.
2014-04-20Fixing bug #3285.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
adding a new grammar entry for clauses
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
file.
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
observe non-normalized goals.
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
The removed code isn't used locally and isn't exported in the signature
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2014-03-03Fixing pervasive equalities. In particular, I removed the code that deletedPierre-Marie Pédrot
duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite.
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
file was useless and duplicated code from Btermdn itself.
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
There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching.
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
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
Introducing List.fold_right and List.fold_left in Monad.
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
Adds a combinator List.map_right which chains effects from right to left.
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-27Remove unsafe code (Obj.magic) in Tacinterp.Arnaud Spiwack
This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
Impacts MapleMode.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 22:30:53 +0000