aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
Commit message (Expand)AuthorAge
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove [advance] from the API.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Make [Goal.goal] be exactly [Evar.t].Gravatar Arnaud Spiwack2014-10-16
* Goal: remove dead code.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Gravatar Arnaud Spiwack2014-10-16
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* 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
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
* 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
* Fix: shelve_unifiable did not work modulo evar instantiation.Gravatar Arnaud Spiwack2014-09-04
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
* 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
* Goal: API to get the solution of a goalGravatar Enrico Tassi2014-08-05
* Tentative optimization not to nf_evar too often in the compatibilityGravatar Pierre-Marie Pédrot2014-06-17
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Potentially unused computation in Goal.Gravatar Pierre-Marie Pédrot2014-03-07
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Useless Array.of_listGravatar Pierre-Marie Pédrot2014-01-10
* Exporting the full pretyper options in Goal.constr_of_raw.Gravatar Pierre-Marie Pédrot2014-01-10
* Fixing ltac constr variable handling in refine.Gravatar Pierre-Marie Pédrot2013-11-30
* Useless computation in Goal handle augmentation.Gravatar ppedrot2013-11-12
* Partial applications in Goal.Gravatar ppedrot2013-11-09
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
* Add primitives in Goal.V82 to access the goal in nf_evar'd form.Gravatar aspiwack2013-11-02
* A tactic shelve_unifiable.Gravatar aspiwack2013-11-02
* Normalise goals with respect to evars in the new tactics.Gravatar aspiwack2013-11-02
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* A better version of Goal.advance.Gravatar aspiwack2013-11-02
* More optimisations of partial applications.Gravatar aspiwack2013-11-02
* Try to remove intermediate allocations when dealing with goal-specific tactics.Gravatar aspiwack2013-11-02
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Removing dubious use of evarmap manipulating functions in printingGravatar ppedrot2013-10-05
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
* State Transaction MachineGravatar gareuselesinge2013-08-08
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 03:45:13 +0000