aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2014-02-27Get rid of the enterl/glist API for Proofview.Goal.Arnaud Spiwack
2014-02-27Tacinterp: yet another superfluous enterl.Arnaud Spiwack
2014-02-27Tacinterp: spurious enterl.Arnaud Spiwack
2014-02-27Dead code: eval_ltac_constr.Arnaud Spiwack
2014-02-25Tacinterp: remove the is_value check in Ltac's let-in.Arnaud Spiwack
2014-02-25Tacinterp: fewer enterl still.Arnaud Spiwack
2014-02-25Tacinterp: fewer Proofview.Goal.enterl.Arnaud Spiwack
2014-02-25Tacinterp: clean up.Arnaud Spiwack
2014-02-25Tacinterp: remove unnecessary return/bind pairs.Arnaud Spiwack
2014-02-24TacticMatching: avoid some closure allocation in (<*>).Arnaud Spiwack
2014-02-24Removed some trailing whitespaces.Arnaud Spiwack
2014-02-24IStream: a concat_map primitive.Arnaud Spiwack
2014-02-24A view type for IStream.Arnaud Spiwack
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2014-02-04The constructor tactic now returns several successes.Pierre-Marie Pédrot
2014-02-02Fixing bug #3226.Pierre-Marie Pédrot
2014-01-31In Ltac's exact tactic: avoid checking the type of the term twice.Arnaud Spiwack
2014-01-28Fixing dependent inversion. Some exceptions were not caught by the tacticPierre-Marie Pédrot
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2014-01-17Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...Pierre-Marie Pédrot
2014-01-14Removing unused tactics in rewrite.Pierre-Marie Pédrot
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-04Code cleaning in Rewrite, may also result faster.Pierre-Marie Pédrot
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-24Simplifying the use of hypinfos in Rewrite.Pierre-Marie Pédrot
2013-12-23Rewrite.ml: removing direction flag from hypinfo.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-10 14:10:18 +0000