aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
| | | | | | | | | | | 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
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
| | | | | | | | | | 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
* A few comments and a dev file to summarize issues with unificationGravatar herbelin2011-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14200 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
| | | | | | | | | 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
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | 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
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
| | | | | | | | - 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
* Fixing another bug with "_" intro pattern.Gravatar herbelin2011-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing the "buggy" first_name and prepare multi-induction.Gravatar herbelin2011-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made use of "_" in repeated use of intros_patterns work (withGravatar herbelin2011-06-10
| | | | | | 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
* Integrating onLastHypId into intro so that we can get the introductionGravatar herbelin2011-06-10
| | | | | | | 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
* Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity ↵Gravatar msozeau2011-06-07
| | | | | | proofs create unsolved evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing discriminate for identity.Gravatar herbelin2011-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)Gravatar letouzey2011-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 85f007b7-540e-0410-9357-904b9bb8a0f7
* More work on error handlingGravatar letouzey2011-05-17
| | | | | | | | | | | | | | 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
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
| | | | | | | | | 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
* Revert r14078 "Partial backtrack on the support for open terms in ↵Gravatar gmelquio2011-04-28
| | | | | | | | 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
* Partial backtrack on the support for open terms in destruct/induction:Gravatar gmelquio2011-04-28
| | | | | | | | | 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
* Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).Gravatar herbelin2011-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
| | | | | | (backport from trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug of destruct which was sometimes forgetting local definitions ↵Gravatar herbelin2011-04-24
| | | | | | behind it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Don't force progress on instance applications, there is always progress when ↵Gravatar msozeau2011-04-20
| | | | | | refining dependent instances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14031 85f007b7-540e-0410-9357-904b9bb8a0f7
* This is used in the rippling plugin. This also allows fixing bug #2188.Gravatar msozeau2011-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* More informative anomaly.Gravatar herbelin2011-04-14
| | | | | | 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
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
| | | | | | | | | | | 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
* Put dependent subgoals first so as to allow backtracking on them, might ↵Gravatar msozeau2011-04-13
| | | | | | change resolution time quite a bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13997 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
| | | | | | | - 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
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - 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
* - Improve unification (beta-reduction, and same heuristic as evarconv for ↵Gravatar msozeau2011-04-13
| | | | | | reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
| | | | | | - 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
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Tom Prince's patch for build_constant_by_tactic not able toGravatar herbelin2011-04-08
| | | | | | 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
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
| | | | | | | | | | | | | | 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
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
| | | | | | | | | | | | | | | | 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
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
| | | | | | | 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
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
| | | | | | | - Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
| | | | | | | in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix declarations of [Add Setoid/Morphism...] in sections to not exportGravatar msozeau2011-03-08
| | | | | | | by default (bug introduced in r13842). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing injection bug #2493 (regression introduced by fixing injectionGravatar herbelin2011-03-05
| | | | | | bug #2255 from 8.2pl2: use of unification might support cumulativity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13873 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Allow to set a particular transparent_state for the local hintGravatar msozeau2011-03-04
| | | | | | | | database - Fix [specialize] to properly resolve typeclass constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13868 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Allow rewriting under abitrary products, not just those in Prop.Gravatar msozeau2011-02-28
| | | | | | | | | - New [fold] rewrite strategy to do folding of terms up-to unification and under binders (might leave uninstantiated existentials). This does not build a proof, only a cast. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13864 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
| | | | | | | | | were all declared as global). - Add possibility to remove hints (Resolve or Immediate only) based on the name of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to clarify a bit Class_tactics (comments, refactoring,...)Gravatar letouzey2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13832 85f007b7-540e-0410-9357-904b9bb8a0f7
* An generic imperative union-find, used for deps of evars in Class_tacticsGravatar letouzey2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change Evd.fold to a faster version that simply removes unneeded evars.Gravatar msozeau2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13830 85f007b7-540e-0410-9357-904b9bb8a0f7
* - proper printing of setoid_rewrite tactic applicationsGravatar msozeau2011-02-10
| | | | | | | | | - keep a list of names to avoid when going under lambdas so as not to clash with bound ltac variables (fixes Random contrib). - remove unused argument of strategies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13819 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename subst_raw_with_bindings to subst_glob_with_bindings and exportGravatar msozeau2011-02-10
| | | | | | | it, properly apply substitution to setoid_rewrite arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13818 85f007b7-540e-0410-9357-904b9bb8a0f7
* One more fix for setoid_rewrite: completely reinterpret the given lemmasGravatar msozeau2011-02-09
| | | | | | | | in the current goal, generating fresh evars and metas for unification (fixes contrib ATBR). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of existential variables when multiple differentGravatar msozeau2011-02-08
| | | | | | | | | instances of the lemma are rewritten at once. Cleanup dead code and put the problematic cases in the test-suite. Also fix some test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13813 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 06:16:58 +0000