aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2012-03-02Noise for nothingpboutill
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-12-14Some extra universe refreshing seems needed in abstract_generalizeherbelin
2011-12-12Proof using ...gareuselesinge
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
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-08-22Tactics.compute_scheme_signature: factorize the two almost-similar casesletouzey
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-10Exported tactic intro_thenherbelin
2011-07-29Tactics: replace generic = on constr by destructorspuech
2011-07-29Tactics: 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 constr replaced by eq_constrpuech
2011-07-29Tactics: generic equality on named_declaration replaced by eq_named_declarationpuech
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...herbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
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-04-26Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).herbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions behi...herbelin
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-04-13- Remove create_evar_defsmsozeau
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-04- Allow to set a particular transparent_state for the local hintmsozeau
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-09-24Solving bug #2212 (unification under tuples now not allowed forherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-30Fix generalize_eqs tactic to not consider defined variables as being generali...msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-13Made intros_until and onInductionArg a bit stricter and robustherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:01:02 +0000