aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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
2011-03-11- Better error messages taking unif. constraints into account.msozeau
- 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
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08Fix declarations of [Add Setoid/Morphism...] in sections to not exportmsozeau
by default (bug introduced in r13842). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13898 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Fixing injection bug #2493 (regression introduced by fixing injectionherbelin
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
2011-03-04- Allow to set a particular transparent_state for the local hintmsozeau
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
2011-02-28- Allow rewriting under abitrary products, not just those in Prop.msozeau
- 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
2011-02-17- Use transparency information all the way through unification andmsozeau
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
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
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
2011-02-11Try to clarify a bit Class_tactics (comments, refactoring,...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13832 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11An generic imperative union-find, used for deps of evars in Class_tacticsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13831 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11Change Evd.fold to a faster version that simply removes unneeded evars.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13830 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-10- proper printing of setoid_rewrite tactic applicationsmsozeau
- 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
2011-02-10Rename subst_raw_with_bindings to subst_glob_with_bindings and exportmsozeau
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
2011-02-09One more fix for setoid_rewrite: completely reinterpret the given lemmasmsozeau
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
2011-02-08Correct handling of existential variables when multiple differentmsozeau
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
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
new proof engine. Correct treatment of the evar set: the tactic incrementally extends (and potentially refines) the existing sigma and the internally generated typeclasses constraints are removed from it at the end as they are always solved. This avoids tricky and costly evar_map manipulations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13812 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-03Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)letouzey
After r13717, we concentrate on undefined evars. But doing so too naively was breaking Class_tactics.split_evars, since defined evars may point to undefined ones. We should not ignore them, but rather traverse them, which is now done by functions Evarutil.undefined_evars_of_* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13809 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Add [Typeclasses Debug] option that respects backtracking, solvemsozeau
regression in typeclass resolution not generating the proper subgoals (may break some contribs). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13787 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-27Rename the "raw" argument extension into "glob"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13761 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
Rationale: the expansion ignores the TYPED clause when {RAW,GLOB}_TYPED are given. Indeed, in this case, the final type is a consequence of either "INTERPRETED BY" (if given), or the default one based on GLOB_TYPED. This avoids the pitfall of the "raw" argument extension, where the TYPED clause was unused and totally misleading. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13760 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24More {raw => glob} changes for consistencyglondu
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24tactics/eqdecide.ml4: avoid a useless argument in decideEqualityglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13753 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Remove the two-argument variant of "decide equality"glondu
This variant was ignoring its second argument, and didn't exactly respect its documented specification. This is fixed by removing the variant altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13746 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Rename rawterm.ml into glob_term.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-15Evar-related speed-up and clarifications in Class_tactics and Rewriteletouzey
Some functions are restricted to consider only undefined evars, and some Evd.fold are replaced by Evd.fold_undefined. I'm less sure about the modifications in rewrite.ml4, but in pratice they seem to work well on the stdlib. I was planning to say assert false for Not_found in Rewrite.evd_of_existentials but some file of the stdlib doesn't like that (to be checked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13717 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-15Misc improvements about evar_mapletouzey
- A Evd.defined_evars to keep only this part of the evar_map - One Evd.fold less in Typeclasses.mark_unresolvables - We check that only undefined evar_map could be set unresolvable - A duplicated function in himsg.ml TODO: some calls to Evd.fold(_undefined) would be faster if written as Map.map or Map.mapi. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:28:03 +0000