aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
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
2010-06-09Relaxed the freshness constraint in "intro H" (with "H" explicit):herbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-20Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)herbelin
2010-04-14Removing redundant internal variants of apply tactic and simplification of ML...herbelin
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 00:28:33 +0000