aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
AgeCommit message (Expand)Author
2014-08-05Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Arnaud Spiwack
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
2014-08-01Add primtive [num_goal] to Proofview.Arnaud Spiwack
2014-07-28Adding a tclBREAK primitive to the tactic monad.Pierre-Marie Pédrot
2014-07-25Add a tactic [swap i j] to swap the position of goals [i] and [j].Arnaud Spiwack
2014-07-25Adds a cycle tactic to reorder goals in a loop.Arnaud Spiwack
2014-07-24A handful of useful primitives in Proofview.Refine.Arnaud Spiwack
2014-07-24Adding a tail-rec tclONCE.Pierre-Marie Pédrot
2014-07-23Proof_global.start_dependent_proof: properly threads the sigma through the te...Arnaud Spiwack
2014-07-14Adding a delay to tclTIME.Pierre-Marie Pédrot
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-10check_for_interrupt: better (but slower) in threading modeEnrico Tassi
2014-07-08Exporting Proof.split in proofview.Pierre-Marie Pédrot
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-06-19Adding a raw_goals primitive for Tacinterp.Pierre-Marie Pédrot
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-03The tactic interpreter now uses a new type of tactics, throughPierre-Marie Pédrot
2014-05-24Revert "Chasing the goal entering backward while interpreting tactics. This r...Pierre-Marie Pédrot
2014-05-24Chasing the goal entering backward while interpreting tactics. This requiredPierre-Marie Pédrot
2014-05-08- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Matthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Fixing various backtrace recordings.Pierre-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 10:55:43 +0000