aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
AgeCommit message (Expand)Author
2014-04-07Transfering the initial goals from the proofview to the proof object.Pierre-Marie Pédrot
2014-04-06Actually using the [modify] primitive.Pierre-Marie Pédrot
2014-04-01Evars introduced by Proofview refining are flagged as GoalEvar. For somePierre-Marie Pédrot
2014-03-28Lighter interface for creating refining tactics.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
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-25Tacinterp: fewer Proofview.Goal.enterl.Arnaud Spiwack
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
2013-11-05Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same timeppedrot
2013-11-04Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...aspiwack
2013-11-04Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...aspiwack
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
2013-11-02A try/with was catching every exception.aspiwack
2013-11-02Update comments.aspiwack
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02A tactic shelve_unifiable.aspiwack
2013-11-02Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ...aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02Adds an experimental exactly_once tactical.aspiwack
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
2013-11-02A dedicated view type for Proofview_gen.split.aspiwack
2013-11-02Adds a tactical once.aspiwack
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Try to remove intermediate allocations when dealing with goal-specific tactics.aspiwack
2013-11-02Various rewriting, mostly for speed purposes.aspiwack
2013-11-02Makes the Ltac debugger usable again.aspiwack
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Cleanup of comments.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Bases tactics on an IO monad.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Uses Proofview.tclEXTEND more sparingly.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-06-06Fixing bug #3030.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:16:07 +0000