aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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
2010-12-13Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13709 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Add tactic has_evar (#2433)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13664 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Add tactic is_evar (Closes: #2433)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13663 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0"). Would be simpler if make_apply_entry supported lemmas containing evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13597 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31Slight code cleaning in auto.ml (made code of make_exact_entry andherbelin
make_apply_entry more similar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13594 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-27correction of bug #2414 (report of r 13586)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13587 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-23Automatically translate hints of the form "c _ ... _" into "c". Besidesherbelin
being convenient, it improves compatibility when moving more implicit arguments to maximal status. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13574 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-04Two [Evd.fold] turned into [Evd.fold_undefined].aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13491 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained with Tacinterp.eval_tactic. Rationale: these declare parsing rules, and eval_tactic is a semantic action, and therefore should be done in the rule body instead. Moreover, having the glob_tactic_expr and its evaluation captured by these rules was quite confusing IMHO. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Remove some occurrences of "open Termops"glondu
Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
These functions are applied much more often without labels than with them (the alternate of adding the label wherever relevant changes 124 lines instead of 41). Moreover, this is more consistent with the Term module and there is no ambiguity in argument types. This commit goes towards elimination of occurrences of OCaml warning 6. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-27Fix bug in implementation of setoid rewriting under cases andmsozeau
abstractions (reported by Pierre Courtieu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13466 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Solving bug #2212 (unification under tuples now not allowed forherbelin
flexible types what seems a reasonable strategy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13464 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:02:20 +0000