aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
AgeCommit message (Expand)Author
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
2014-09-26Adding a tclNEWGOALS primitive.Pierre-Marie Pédrot
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-15Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Arnaud Spiwack
2014-09-12While we don't have a clean alternative to Clenvtac, add a primitiveMatthieu Sozeau
2014-09-12Add syntax [id]: to apply tactic to goal named id.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12No plural for only one non existing focused goal.Hugo Herbelin
2014-09-12Fix source of initial goal.Hugo Herbelin
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-08Add a tactic [revgoals] to reverse the list of focused goals.Arnaud Spiwack
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
2014-09-04Ensuring the invariant that hypotheses and named context of the environment ofPierre-Marie Pédrot
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Pierre-Marie Pédrot
2014-09-04Using goal-tactics to interpret arguments to idtac.Pierre-Marie Pédrot
2014-09-04Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Pierre-Marie Pédrot
2014-09-03Putting back normalized goals when entering them.Pierre-Marie Pédrot
2014-08-28Simplification of the tclCHECKINTERRUPT tactic.Pierre-Marie Pédrot
2014-08-21Removing unused parts of the Goal.sensitive monad.Pierre-Marie Pédrot
2014-08-19New primitive allowing to modify refine handles.Pierre-Marie Pédrot
2014-08-07Hypotheses in [Proofview.Goal.enter] were not normalised.Arnaud Spiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:45:14 +0000