Fix bug #4707: clearbody much slower in 8.5pl1.

We only retype hypotheses and conclusion when they do depend on the cleared
identifier. This saves a lot of time.

1 files changed, 33 insertions, 23 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 28aed8a10e..63d3c694ea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1789,17 +1789,17 @@ let on_the_bodies = function
 | [id] -> str " depends on the body of " ++ pr_id id
 | l -> str " depends on the bodies of " ++ pr_sequence pr_id l
 
-let check_is_type env ty msg =
-  Proofview.tclEVARMAP >>= fun sigma ->
+exception DependsOnBody of Id.t option
+
+let check_is_type env sigma ty =
   let evdref = ref sigma in
   try
     let _ = Typing.sort_of env evdref ty in
-    Proofview.Unsafe.tclEVARS !evdref
+    !evdref
   with e when Errors.noncritical e ->
-    msg e
+    raise (DependsOnBody None)
 
-let check_decl env (_, c, ty) msg =
-  Proofview.tclEVARMAP >>= fun sigma ->
+let check_decl env sigma (id, c, ty) =
   let evdref = ref sigma in
   try
     let _ = Typing.sort_of env evdref ty in
@@ -1807,14 +1807,15 @@ let check_decl env (_, c, ty) msg =
     | None -> ()
     | Some c -> Typing.check env evdref c ty
     in
-    Proofview.Unsafe.tclEVARS !evdref
+    !evdref
   with e when Errors.noncritical e ->
-    msg e
+    raise (DependsOnBody (Some id))
 
 let clear_body ids =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let sigma = Proofview.Goal.sigma gl in
     let ctx = named_context env in
     let map (id, body, t as decl) = match body with
     | None ->
@@ -1828,23 +1829,32 @@ let clear_body ids =
     let ctx = List.map map ctx in
     let base_env = reset_context env in
     let env = push_named_context ctx base_env in
-    let check_hyps =
-      let check env (id, _, _ as decl) =
-        let msg _ = Tacticals.New.tclZEROMSG
-          (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids)
+    let check =
+      try
+        let check (env, sigma) decl =
+          (** Do no recheck hypotheses that do not depend *)
+          let sigma =
+            if List.exists (fun id -> occur_var_in_decl env id decl) ids then
+              check_decl env sigma decl
+            else sigma
+          in
+          (push_named decl env, sigma)
         in
-        check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env)
-      in
-      let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in
-      Proofview.tclIGNORE checks
-    in
-    let check_concl =
-      let msg _ = Tacticals.New.tclZEROMSG
-        (str "Conclusion" ++ on_the_bodies ids)
-      in
-      check_is_type env concl msg
+        let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in
+        let sigma =
+          if List.exists (fun id -> occur_var env id concl) ids then
+            check_is_type env sigma concl
+          else sigma
+        in
+        Proofview.Unsafe.tclEVARS sigma
+      with DependsOnBody where ->
+        let msg = match where with
+        | None -> str "Conclusion" ++ on_the_bodies ids
+        | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids
+        in
+        Tacticals.New.tclZEROMSG msg
     in
-    check_hyps <*> check_concl <*>
+    check <*>
     Proofview.Refine.refine ~unsafe:true begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
     end