Optimize the clear tactic.

We do not check for presence of a variable in a global definition when we know
that this variable was not present in the section.

1 files changed, 12 insertions, 9 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4506fddb5..56671da80 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -472,10 +472,11 @@ let cleared = Store.field ()
 
 exception Depends of Id.t
 
-let rec check_and_clear_in_constr env evdref err ids c =
+let rec check_and_clear_in_constr env evdref err ids global c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
-     evars) *)
+     evars). [global] should be true iff there is some variable of [ids] which
+     is a section variable *)
   let check id' =
     if Id.Set.mem id' ids then
       raise (ClearDependencyError (id',err))
@@ -485,14 +486,14 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	  check id'; c
 
       | ( Const _ | Ind _ | Construct _ ) ->
-          let vars = Environ.vars_of_global env c in
-            Id.Set.iter check vars; c
+        let () = if global then Id.Set.iter check (Environ.vars_of_global env c) in
+        c
 
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
 	    let nc = whd_evar !evdref c in
-	      (check_and_clear_in_constr env evdref err ids nc)
+	      (check_and_clear_in_constr env evdref err ids global nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
@@ -527,7 +528,8 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	    let _nconcl =
 	      try
                 let nids = Id.Map.domain rids in
-                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
+                let global = Id.Set.exists is_section_variable nids in
+                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi)
 	      with ClearDependencyError (rid,err) ->
 		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
 
@@ -548,19 +550,20 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	    (* spiwack: /hacking session *)
               whd_evar !evdref c
 
-      | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
+      | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
 
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occurring in evi *)
+  let global = Id.Set.exists is_section_variable ids in
   let terms =
-    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
+    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in
   let nhyps =
     let open Context.Named.Declaration in
     let check_context decl =
       let err = OccurHypInSimpleClause (Some (get_id decl)) in
-      map_constr (check_and_clear_in_constr env evdref err ids) decl
+      map_constr (check_and_clear_in_constr env evdref err ids global) decl
     in
     let check_value vk = match force_lazy_val vk with
     | None -> vk