aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
tactic notations and ltac definitions (see bug report #2496). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14606 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
pattern; this fixes stupid causes of failure of destruct shown by compiling contrib Containers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14579 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
constructors as non relevant for injection. Also made injection failing in such situation. Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases (observed in the compilation of CoinductiveReals.LNP_Digit). The most probable explanation is that this loop was formerly protected by a failing rewrite which stopped failing after revision 14549 made second-order pattern-matching more powerful. Also suppressed dead code in Invfun.intros_with_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14573 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2227msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14572 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14524 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05When a pattern match, don't use the first matching term but anherbelin
instance of the initial pattern (this fixes compilation of CoRN after r14499). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14516 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
function but also restricting it to closed matching and consequently renaming it to subst_closed_term_occ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14498 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Adding subst_term up to convherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
resolution from Tacinterp to Pretyping (close to resolve_evars) so that final evar resolution can eventually be called from Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14490 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Remove duplicated version of check_required_library.letouzey
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14486 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-22Tactics.compute_scheme_signature: factorize the two almost-similar casesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14417 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-16Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14411 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Exported tactic intro_thenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14403 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Fix implementation of Hint Immediate used by typeclasses eautomsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14398 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29generic = on named_context replaced by named_context_equalpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14373 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: replace generic = on constr by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14368 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14367 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14341 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Class_tactics: generic equality on named_context_val replaced by ↵puech
eq_named_context_val git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14340 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Eqschemes: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14333 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14328 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14326 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14322 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14321 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on named_declaration replaced by eq_named_declarationpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14320 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Hipattern: two generic equalities on constr spotted & rewrittenpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14316 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-18Fixed a "feature" of "inversion" and "dependent rewrite" revealed byherbelin
the extension of "dependent rewrite" to "sig" type in r14279: in case of an equality "existT a p = x", no rewriting was done at all instead of substituting "x" as "inversion" normally does when an equality "x = t" is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14287 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Changed name of internally defined "_sym" scheme to avoid confusion with ↵herbelin
Logic.eq_sym that has specific implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14280 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> ↵herbelin
and <- when a variable is about to be substituted (subst_one rewrite the whole context at once, while multi_rewrite rewrites each hyp independently, what may break typing in case of dependencies). Also generalize "dependent rewrite" to "sig" (to be done: generalize it to eq_dep, eq_dep1, and any dependent tuple). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14279 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14200 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Moved allow_K to a unification flagherbelin
- seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Fixing another bug with "_" intro pattern.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14185 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Fixing the "buggy" first_name and prepare multi-induction.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14184 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
application to "destruct t as (_,H)" in the dependent case, and so on). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14183 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Integrating onLastHypId into intro so that we can get the introductionherbelin
name even when the hyp has not been introduced at the top of the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14182 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity ↵msozeau
proofs create unsolved evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14167 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-26Fixing discriminate for identity.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14157 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-17Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-17More work on error handlingletouzey
Anomalies are now meant to be the exceptions that are *not* catched and handled by the new Errors.handle_stack. Three variants of [Errors.print] allow to customize how anomalies are treated. In particular, [Errors.print_no_anomaly] is used for the Fail command, instead of a classification function Cerrors.is_user_error which wasn't customizable. No more AnomalyOnError, its only occurrence is now a regular anomaly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14133 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 02:14:08 +0000