aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Added support for having one subgoal inheriting the name of its father in Ref...Gravatar Hugo Herbelin2014-10-09
* Removing Convert_concl and Convert_hyp from Logic.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Factored out IDE goal structure.Gravatar Carst Tankink2014-10-01
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Gravatar Pierre-Marie Pédrot2014-09-27
* Adding a tclNEWGOALS primitive.Gravatar Pierre-Marie Pédrot2014-09-26
* Fixing strange evarmap leak in goals.Gravatar Pierre-Marie Pédrot2014-09-18
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Gravatar Matthieu Sozeau2014-09-17
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
* Fix source of initial goal.Gravatar Hugo Herbelin2014-09-12
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Only using filtered hyps in Goal.enter.Gravatar Pierre-Marie Pédrot2014-09-04
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-09-04
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Fix: shelve_unifiable did not work modulo evar instantiation.Gravatar Arnaud Spiwack2014-09-04
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Using goal-tactics to interpret arguments to idtac.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Cleaning and documenting a bit the Proofview.Refine module.Gravatar Pierre-Marie Pédrot2014-08-28
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
* New primitive allowing to modify refine handles.Gravatar Pierre-Marie Pédrot2014-08-19
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 23:50:24 +0000