From 0daf358a71aff4aded2b822fc18b7a8b49cdbd04 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:29:53 +0000
Subject: Extract_env: generic = on prec_declaration replaced by
 prec_declaration_equal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14369 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/extract_env.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 62473855aa..73062328b1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -137,6 +137,11 @@ let check_fix env cb i =
 	  | _ -> raise Impossible)
     | Undef _ | OpaqueDef _ -> raise Impossible
 
+let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
+  na1 = na2 &&
+  array_equal eq_constr ca1 ca2 &&
+  array_equal eq_constr ta1 ta2
+
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
   let n = Array.length (let fi,_,_ = recd in fi) in
@@ -149,7 +154,8 @@ let factor_fix env l cb msb =
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
-	       if check <> check_fix env cb' (j+1) then raise Impossible;
+	       let check' = check_fix env cb' (j+1) in
+	       if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
     labels, recd, msb''
-- 
cgit v1.2.3