From 8cfe40dbc02156228a529c01190c50d825495013 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 22 Mar 2017 19:06:54 +0100
Subject: Ensuring static invariants about handling of pending evars in
 Pretyping.

All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
---
 tactics/tactics.ml  | 16 ++++++----------
 tactics/tactics.mli |  2 +-
 2 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 84d09d8330..1e8082f882 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1154,10 +1154,9 @@ let tactic_infer_flags with_evar = {
 let onOpenInductionArg env sigma tac = function
   | clear_flag,ElimOnConstr f ->
       let (cbl, sigma') = run_delayed env sigma f in
-      let pending = (sigma,sigma') in
       Tacticals.New.tclTHEN
         (Proofview.Unsafe.tclEVARS sigma')
-        (tac clear_flag (pending,cbl))
+        (tac clear_flag (sigma,cbl))
   | clear_flag,ElimOnAnonHyp n ->
       Tacticals.New.tclTHEN
         (intros_until_n n)
@@ -1165,8 +1164,7 @@ let onOpenInductionArg env sigma tac = function
            (fun c ->
              Proofview.Goal.enter { enter = begin fun gl ->
              let sigma = Tacmach.New.project gl in
-             let pending = (sigma,sigma) in
-             tac clear_flag (pending,(c,NoBindings))
+             tac clear_flag (sigma,(c,NoBindings))
              end }))
   | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
@@ -1174,8 +1172,7 @@ let onOpenInductionArg env sigma tac = function
         (try_intros_until_id_check id)
         (Proofview.Goal.enter { enter = begin fun gl ->
          let sigma = Tacmach.New.project gl in
-         let pending = (sigma,sigma) in
-         tac clear_flag (pending,(mkVar id,NoBindings))
+         tac clear_flag (sigma,(mkVar id,NoBindings))
         end })
 
 let onInductionArg tac = function
@@ -1198,10 +1195,9 @@ let map_destruction_arg f sigma = function
 
 let finish_delayed_evar_resolution with_evars env sigma f =
   let ((c, lbind), sigma') = run_delayed env sigma f in
-  let pending = (sigma,sigma') in
   let sigma' = Sigma.Unsafe.of_evar_map sigma' in
   let flags = tactic_infer_flags with_evars in
-  let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in
+  let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in
   (Sigma.to_evar_map sigma', (c, lbind))
 
 let with_no_bindings (c, lbind) =
@@ -4525,11 +4521,11 @@ let induction_destruct isrec with_evars (lc,elim) =
 
 let induction ev clr c l e =
   induction_gen clr true ev e 
-    (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None
+    ((Evd.empty,(c,NoBindings)),(None,l)) None
 
 let destruct ev clr c l e =
   induction_gen clr false ev e
-    (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None
+    ((Evd.empty,(c,NoBindings)),(None,l)) None
 
 (* The registered tactic, which calls the default elimination
  * if no elimination constant is provided. *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7acfb62864..354ac50b43 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -385,7 +385,7 @@ val letin_tac : (bool * intro_pattern_naming) option ->
 (** Common entry point for user-level "set", "pose" and "remember" *)
 
 val letin_pat_tac : (bool * intro_pattern_naming) option ->
-  Name.t -> pending_constr -> clause -> unit Proofview.tactic
+  Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic
 
 (** {6 Generalize tactics. } *)
 
-- 
cgit v1.2.3


From f9526a2bcd05174b7adfe56b7375f0306a2a1e6d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Mar 2017 08:38:00 +0100
Subject: 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.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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 }
 
-- 
cgit v1.2.3