aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-20Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicherbelin
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-18Removing redundant entry int_nelist and removing extra space whenherbelin
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution of...msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-02Noise for nothingpboutill
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-02-14In [reflexivity], [symmetry] etc, use the type found by looking at the relati...msozeau
2012-02-07A "Grab Existential Variables" to transform the unresolved evars at the end o...aspiwack
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2012-01-23Fix bug #2483: anomaly raised due to wrong handling of the evars state.msozeau
2012-01-20Breakpoints in Ltac debugger: new command "r foo" to jump to the nextherbelin
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-12-17Improving pretty-printing of Ltac functions.herbelin
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:15:42 +0000