From 67fe536720c5ef5bb509249b9a30cbc6f2cebd92 Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 26 Feb 2004 13:35:24 +0000
Subject: Keep structure information for Fixpoint declaration and Fix terms

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

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e28065afd8..fa1faf9cf3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1009,7 +1009,7 @@ let rec check_same_type ty1 ty2 =
   match ty1, ty2 with
   | CRef r1, CRef r2 -> check_same_ref r1 r2
   | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
-      List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) ->
+      List.iter2 (fun (id1,i1,_,a1,b1) (id2,i2,_,a2,b2) ->
         if id1<>id2 || i1<>i2 then failwith "not same fix";
         check_same_type a1 a2;
         check_same_type b1 b2)
@@ -1508,7 +1508,7 @@ let rec extern inctx scopes vars r =
 	 | RFix (nv,n) ->
 	     let listdecl = 
 	       Array.mapi (fun i fi ->
-		 (fi,nv.(i),extern_type scopes vars tyv.(i),
+		 (fi,nv.(i), None, extern_type scopes vars tyv.(i),
                   extern false scopes vars' bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
-- 
cgit v1.2.3