aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2014-04-27Rewriting [lapply] tactic in the new monad.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-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 tactic compatibility layer from Elim.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-04-20Adding a [map] primitive to the tactic monad. Hopefully this should bePierre-Marie Pédrot
2014-04-07Transfering the initial goals from the proofview to the proof object.Pierre-Marie Pédrot
2014-04-06Removing unused functions in Refiner.Pierre-Marie Pédrot
2014-04-06Actually using the [modify] primitive.Pierre-Marie Pédrot
2014-04-06Adding an [modify] function to the tactic monad. It allows to modifyPierre-Marie Pédrot
2014-04-01Evars introduced by Proofview refining are flagged as GoalEvar. For somePierre-Marie Pédrot
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 01:39:40 +0000