aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2014-10-16Expose Proofview.Refine.with_type in the API.Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-16Move the handling of the principal evar from refine to evd.Arnaud Spiwack
2014-10-16Move the handling a new evars from the [Proofview.Refine] module to [Evd].Arnaud Spiwack
2014-10-16Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Arnaud Spiwack
2014-10-16Proofview: small optimisation/simplification.Arnaud Spiwack
2014-10-13Add support for deactivating type class inference from induction/destruct.Hugo Herbelin
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-10-13Naming main goal "Main"Hugo Herbelin
2014-10-09Added support for having one subgoal inheriting the name of its father in Ref...Hugo Herbelin
2014-10-09Removing Convert_concl and Convert_hyp from Logic.Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-06Make tclEFFECTS also update the env in the proof monadEnrico Tassi
2014-10-04A few Global.env removed.Hugo Herbelin
2014-10-01Factored out IDE goal structure.Carst Tankink
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
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-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Matthieu Sozeau
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
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-12Use evar name to print goal.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo 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-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-10Fixing localisation of tactic errors (my mistake in himsg.ml essentially).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-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
2014-09-04Only using filtered hyps in Goal.enter.Pierre-Marie Pédrot
2014-09-04Ensuring the invariant that hypotheses and named context of the environment ofPierre-Marie Pédrot
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Fix: shelve_unifiable did not work modulo evar instantiation.Arnaud Spiwack
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-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 11:29:51 +0000