Fast path for implicit tactic solving.

We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.

6 files changed, 27 insertions, 21 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1223f6eb4b..7a9fc6657e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
@@ -341,10 +341,10 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-let constr_flags = {
+let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
@@ -353,7 +353,7 @@ let refine_tac ist simple with_classes c =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags =
-      { constr_flags with Pretyping.use_typeclasses = with_classes } in
+      { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index fcc2b86a91..f75ea70872 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -45,7 +45,7 @@ let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6ed96c1fb7..fe10f0c313 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   Proofview.NonLogical.run (db_constr (curr_debug ist) env c);
   (evd,c)
 
-let constr_flags = {
+let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  interp_gen kind ist false constr_flags env sigma c
+  interp_gen kind ist false (constr_flags ()) env sigma c
 
 let interp_constr = interp_constr_gen WithoutTypeConstraint
 
 let interp_type = interp_constr_gen IsType
 
-let open_constr_use_classes_flags = {
+let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
-let open_constr_no_classes_flags = {
+let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
@@ -679,11 +679,11 @@ let pure_open_constr_flags = {
   expand_evars = false }
 
 (* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
   let flags =
-    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
-    else open_constr_use_classes_flags in
-  interp_gen expected_type ist false flags
+    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
+    else open_constr_use_classes_flags () in
+  interp_gen expected_type ist false flags env sigma c
 
 let interp_pure_open_constr ist =
   interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b06ea43bdd..9995a9394a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -233,10 +233,10 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac
 
 let clear_implicit_tactic () = implicit_tactic := None
 
-let solve_by_implicit_tactic env sigma evk =
+let apply_implicit_tactic tac = (); fun env sigma evk ->
   let evi = Evd.find_undefined sigma evk in
-  match (!implicit_tactic, snd (evar_source evk sigma)) with
-  | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
+  match snd (evar_source evk sigma) with
+  | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
 	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
@@ -250,3 +250,9 @@ let solve_by_implicit_tactic env sigma evk =
         sigma, ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
+
+let solve_by_implicit_tactic () = match !implicit_tactic with
+| None -> None
+| Some tac -> Some (apply_implicit_tactic tac)
+
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7458109fa1..aad719db49 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
+val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr) option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1e8082f882..8b3442c05b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1146,7 +1146,7 @@ let run_delayed env sigma c =
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = Some solve_by_implicit_tactic;
+  Pretyping.use_hook = solve_by_implicit_tactic ();
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }