aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2014-03-28Lighter interface for creating refining tactics.Pierre-Marie Pédrot
2014-03-27Removing tactic compatibility layer from Eqdecide.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 Inv.Pierre-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-07Potentially unused computation in Goal.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-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-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-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-25Tacinterp: fewer Proofview.Goal.enterl.Arnaud Spiwack
2014-02-24cbn understands ArgumentsPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2014-02-21More sharing in Logic, together with some code cleaning.Pierre-Marie Pédrot
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2014-02-10STM: fix valid_id coming from Qed errorsEnrico Tassi
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-02-02Fixing backtrace reporting.Pierre-Marie Pédrot
2014-01-31Typos in comment.Arnaud Spiwack
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2014-01-10Useless Array.of_listPierre-Marie Pédrot
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-06Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...Arnaud Spiwack
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-04Fix Admitted.Arnaud Spiwack
2013-12-04Proof_global: fix start_proof comment after the preceding commits.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
2013-11-30Fixing ltac constr variable handling in refine.Pierre-Marie Pédrot
2013-11-29Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notHugo Herbelin
2013-11-12Useless computation in Goal handle augmentation.ppedrot
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 13:06:25 +0000