From b0ffad7f20114875611132dfffb9517d6f5b9ff9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 Jun 2016 08:40:51 +0200
Subject: Small optimization in clear_body.

We do not check that an hypothesis is used in context declarations that
occur before it.
---
 tactics/tactics.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d4158d7872..c336bb434a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2026,16 +2026,18 @@ let clear_body ids =
     let env = push_named_context ctx base_env in
     let check =
       try
-        let check (env, sigma) decl =
+        let check (env, sigma, seen) 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
+            if not seen then sigma
+            else 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)
+          let seen = seen || List.mem_f Id.equal (get_id decl) ids in
+          (push_named decl env, sigma, seen)
         in
-        let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in
+        let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in
         let sigma =
           if List.exists (fun id -> occur_var env id concl) ids then
             check_is_type env sigma concl
-- 
cgit v1.2.3