From 86da26360d2136e9579beeb59b192ccfb0e67c18 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 Jun 2016 16:41:05 +0200
Subject: Optimize the clear tactic.

We do not allocate a closure in the main loop, and do so only when needed.
---
 engine/evarutil.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 56671da804..df1424e1c6 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -477,16 +477,18 @@ let rec check_and_clear_in_constr env evdref err ids global c =
      (ie the hypotheses ids have been removed from the contexts of
      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))
-  in
     match kind_of_term c with
       | Var id' ->
-	  check id'; c
+      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
 
       | ( Const _ | Ind _ | Construct _ ) ->
-        let () = if global then Id.Set.iter check (Environ.vars_of_global env c) in
+        let () = if global then
+          let check id' =
+            if Id.Set.mem id' ids then
+              raise (ClearDependencyError (id',err))
+          in
+          Id.Set.iter check (Environ.vars_of_global env c)
+        in
         c
 
       | Evar (evk,l as ev) ->
-- 
cgit v1.2.3