aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Removing redundant entry int_nelist and removing extra space whenGravatar herbelin2012-03-18
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Revise API of understand_ltac to be parameterized by a flag for resolution of...Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Use a heuristic to not simplify equality hypotheses remaining after dependent...Gravatar msozeau2012-02-20
* In [reflexivity], [symmetry] etc, use the type found by looking at the relati...Gravatar msozeau2012-02-14
* A "Grab Existential Variables" to transform the unresolved evars at the end o...Gravatar aspiwack2012-02-07
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Added an pattern / occurence syntax for vm_compute.Gravatar ppedrot2012-01-30
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* Fix bug #2483: anomaly raised due to wrong handling of the evars state.Gravatar msozeau2012-01-23
* Breakpoints in Ltac debugger: new command "r foo" to jump to the nextGravatar herbelin2012-01-20
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
* Improving pretty-printing of Ltac functions.Gravatar herbelin2011-12-17
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
* Some extra universe refreshing seems needed in abstract_generalizeGravatar herbelin2011-12-14
* Proof using ...Gravatar gareuselesinge2011-12-12
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Fix parsing of :>> and backtrack correctly on the cache of hints for local co...Gravatar msozeau2011-11-18
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Merge fix for bug #2604.Gravatar msozeau2011-11-17
* Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...Gravatar msozeau2011-11-17
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Was missing a potential application of subtypingGravatar msozeau2011-11-17
* Fixing tactic remember not correctly checking preservation of typingGravatar herbelin2011-11-06
* Auto: removal of ?use_core_db obsolete now that we have nocoreGravatar letouzey2011-11-04
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Auto: avoid storing clausenv (and hence env, evar_map, universes) in voGravatar letouzey2011-10-26
* Applying Tom Prince's patch to support parametric "constructor n" inGravatar herbelin2011-10-25
* Use full conversion for checking type of holes in destruct over aGravatar herbelin2011-10-22
* Fixing Equality.injectable which did not detect an equality withoutGravatar herbelin2011-10-22
* Fix bug #2473 due to wrong folding of the evar environmentGravatar msozeau2011-10-18
* Fix bug #2227Gravatar msozeau2011-10-18
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* A new tactic is_var to check whether a term is a goal/section variableGravatar letouzey2011-10-07
* When a pattern match, don't use the first matching term but anGravatar herbelin2011-10-05
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
* Adding subst_term up to convGravatar herbelin2011-09-26
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
* auto with nocore : disable the use of the core database (wish #2188)Gravatar letouzey2011-09-23