aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Remove duplicated version of check_required_library.Gravatar letouzey2011-09-22
* Tactics.compute_scheme_signature: factorize the two almost-similar casesGravatar letouzey2011-08-22
* Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)Gravatar aspiwack2011-08-16
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Exported tactic intro_thenGravatar herbelin2011-08-10
* Fix implementation of Hint Immediate used by typeclasses eautoGravatar msozeau2011-08-10
* generic = on named_context replaced by named_context_equalGravatar puech2011-07-29
* Tactics: replace generic = on constr by destructorsGravatar puech2011-07-29
* Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordGravatar puech2011-07-29
* Tactics: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Class_tactics: generic equality on named_context_val replaced by eq_named_con...Gravatar puech2011-07-29
* Eqschemes: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Equality: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Tactics: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Equality: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Tactics: generic equality on constr replaced by eq_constrGravatar puech2011-07-29