aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-07 15:15:04 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-07 15:15:04 +0000
commit4a1077f9d1ee00632ec72a4089013194f558cacd (patch)
tree0e38a7ea9d0f9f8b9cd18873f404482f0e98d446 /tactics/auto.mli
parent69e52c438714e01fbaefc05b61f47a5ae95a7205 (diff)
Fixes in typeclasses resolution. Avoid reducing instances types before
making the auto apply entry. Makes indexing better and avoid polution of [auto with *] with many abstract lemmas comming from [typeclass_instances]. Quite a nice speedup again, even Field_theory has dropped to 58s from 70s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.mli')
-rw-r--r--tactics/auto.mli10
1 files changed, 6 insertions, 4 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 3efcc6281..b35f98ec1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -95,11 +95,13 @@ val make_exact_entry : int option -> constr * constr -> global_reference * pri_a
(* [make_apply_entry (eapply,verbose) pri (c,cty)].
[eapply] is true if this hint will be used only with EApply;
+ [hnf] should be true if we should expand the head of cty before searching for
+ products;
[c] is the term given as an exact proof to solve the goal;
- [cty] is the type of [hc]. *)
-
+ [cty] is the type of [c]. *)
+
val make_apply_entry :
- env -> evar_map -> bool * bool -> int option -> constr * constr
+ env -> evar_map -> bool * bool * bool -> int option -> constr * constr
-> global_reference * pri_auto_tactic
(* A constr which is Hint'ed will be:
@@ -110,7 +112,7 @@ val make_apply_entry :
has missing arguments. *)
val make_resolves :
- env -> evar_map -> bool * bool -> int option -> constr ->
+ env -> evar_map -> bool * bool * bool -> int option -> constr ->
(global_reference * pri_auto_tactic) list
(* [make_resolve_hyp hname htyp].