From 5168a1b2383c34c40a4ec310ff4e4d990794df2e Mon Sep 17 00:00:00 2001
From: jforest
Date: Fri, 6 Jul 2007 19:55:53 +0000
Subject: minor bug correction (continuing r 9943)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9956 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/recdef/recdef.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 213ec18a1c..afbe1c933d 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1237,7 +1237,7 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		  [cont_tac pmax' le_proofs';
 		   h_intros [heq;heq2];
 		   observe_tac "rewriteRL" (tclTRY (rewriteLR (mkVar heq2)));
-		   tclTHENS
+		   tclTRY (tclTHENS
 		     ( fun g -> 
 			 let t_eq = compute_renamed_type g (mkVar heq) in 
 			 let k_id,def_id = 
@@ -1259,7 +1259,7 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		     [tclIDTAC;
 		      tclTHENLIST
 			[apply (delayed_force le_lt_n_Sm);
-			 compute_le_proofs le_proofs']]])
+			 compute_le_proofs le_proofs']])])
 	     functional termine f p heq1 new_pmax
 	     (p'::bounds)((mkVar pmax)::le_proofs) eqs
              (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args]
-- 
cgit v1.2.3