aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
Commit message (Expand)AuthorAge
* 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
* 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
* Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Gravatar Pierre-Marie Pédrot2014-09-27
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-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
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* 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
* 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
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* Try to remove intermediate allocations when dealing with goal-specific tactics.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
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
* No reason a priori for using unfiltered env for printingGravatar herbelin2013-01-29
* Fixed synchronicity of filter with evar context in new_goal_with.Gravatar herbelin2013-01-29
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fixes bug #2654 (tactic instantiate failing to update existential variables).Gravatar aspiwack2012-01-06
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Porting Hendrik's 8.3 patch for proof tree visualization under proofGravatar herbelin2011-08-30
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Enlevé les trucs commités au mauvais endroitGravatar aspiwack2007-10-23
* Quelques structures de donnée plus les modules principaux (et Gravatar aspiwack2007-10-23