aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2011-11-18Fix parsing of :>> and backtrack correctly on the cache of hints for local co...msozeau
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Merge fix for bug #2604.msozeau
2011-11-17Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-17Was missing a potential application of subtypingmsozeau
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
2011-11-04Auto: removal of ?use_core_db obsolete now that we have nocoreletouzey
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-26Auto: avoid storing clausenv (and hence env, evar_map, universes) in voletouzey
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 11:12:20 +0000