aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Revert r14078 "Partial backtrack on the support for open terms in ↵gmelquio
destruct/induction:" While this is needed for supporting destruct with typeclasses on 8.4, it was not my intent to commit it yet (as a better fix might be in the work), so reverting it for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14079 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Partial backtrack on the support for open terms in destruct/induction:gmelquio
use type classes to possibly solve evars before trying to unify the term (or the dependencies of its type) agains a subterm of the current goal. This solves compatibility bug #2222. Mixing unification and type classes is left for future work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14078 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14067 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
(backport from trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14061 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions ↵herbelin
behind it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14053 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Don't force progress on instance applications, there is always progress when ↵msozeau
refining dependent instances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14031 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20This is used in the rippling plugin. This also allows fixing bug #2188.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14030 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-18Add a flag to control betaiota reduction during unification to maintain ↵msozeau
backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14More informative anomaly.herbelin
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14002 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Put dependent subgoals first so as to allow backtracking on them, might ↵msozeau
change resolution time quite a bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13997 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Make typeclass transparency information directly availablemsozeau
- Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Remove create_evar_defsmsozeau
- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Improve unification (beta-reduction, and same heuristic as evarconv for ↵msozeau
reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
- Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Add [Polymorphic] flag for defsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
use a lemma name chosen by the caller (here tclABSTRACT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13972 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
Note: even if this new tactical can be quite handy during the development phase, (for instance to bound the time allocated to some search tactics), please be aware of its main drawback: with it, scripts are no longer machine-independant, something that works on a quick machine may fail on a slow one. The converse is even possible if you combine this "timeout" with other tactic combinators. We strongly advise to not leave any "timeout" in the final version of a development. In addition, this feature won't probably work on native win32, since Unix.alarm isn't implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
in preparation for adding forward reasoning to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 01:29:12 +0000