From ad1c7b1866c7b6ec29d72d99783bfa4281756b44 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 10 Apr 2002 11:48:37 +0000
Subject: Simplification des Clear internes dégénérés (sans hypothèses à
 effacer)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2626 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacmach.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a2f5478df9..115367cd79 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -230,11 +230,11 @@ let convert_concl c gl =
 let convert_hyp d gl =
   refiner (Prim (Convert_hyp d)) gl
 
-let thin ids gl = 
-  refiner (Prim (Thin ids)) gl
+let thin ids gl =
+  if ids = [] then tclIDTAC gl else refiner (Prim (Thin ids)) gl
 
-let thin_body ids gl = 
-  refiner (Prim (ThinBody ids)) gl
+let thin_body ids gl =
+  if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
 
 let move_hyp with_dep id1 id2 gl = 
   refiner (Prim (Move (with_dep,id1,id2))) gl
-- 
cgit v1.2.3