aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2011-10-18Fix bug #2227msozeau
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
2011-10-05When a pattern match, don't use the first matching term but anherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
2011-09-26Adding subst_term up to convherbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
2011-09-22Remove duplicated version of check_required_library.letouzey
2011-08-22Tactics.compute_scheme_signature: factorize the two almost-similar casesletouzey
2011-08-16Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)aspiwack
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-10Exported tactic intro_thenherbelin
2011-08-10Fix implementation of Hint Immediate used by typeclasses eautomsozeau
2011-07-29generic = on named_context replaced by named_context_equalpuech
2011-07-29Tactics: replace generic = on constr by destructorspuech
2011-07-29Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordpuech
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
2011-07-29Class_tactics: generic equality on named_context_val replaced by eq_named_con...puech
2011-07-29Eqschemes: generic equality on constr replaced by eq_constrpuech
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
2011-07-29Tactics: generic equality on named_declaration replaced by eq_named_declarationpuech
2011-07-29Hipattern: two generic equalities on constr spotted & rewrittenpuech
2011-07-18Fixed a "feature" of "inversion" and "dependent rewrite" revealed byherbelin
2011-07-16Changed name of internally defined "_sym" scheme to avoid confusion with Logi...herbelin
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...herbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-06-10Fixing the "buggy" first_name and prepare multi-induction.herbelin
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
2011-06-10Integrating onLastHypId into intro so that we can get the introductionherbelin
2011-06-07Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...msozeau
2011-05-26Fixing discriminate for identity.herbelin
2011-05-17Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)letouzey
2011-05-17More work on error handlingletouzey
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-04-28Revert r14078 "Partial backtrack on the support for open terms in destruct/in...gmelquio
2011-04-28Partial backtrack on the support for open terms in destruct/induction:gmelquio
2011-04-26Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:30:18 +0000