From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 29 May 2008 11:51:14 +0000 (+0000)
Subject: ref sync check fixed controlling fix/cofix coherence
X-Git-Tag: make_still_working~5108
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d4d4ff40606138ea72668cf46a95c776d2f1b7c;p=helm.git

ref sync check fixed controlling fix/cofix coherence
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 42faf7e6a..464aa7c2a 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1020,10 +1020,10 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
       let _,_,_,cl = List.nth tl i in 
       let _,_,arity = List.nth cl (j-1) in 
       arity
-  | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,Ref.CoFix i) ->
+  | (_,_,_,_,C.Fixpoint (false,fl,_)), Ref.Ref (_,Ref.CoFix i) ->
       let _,_,_,arity,_ = List.nth fl i in
       arity
-  | (_,h1,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,Ref.Fix (i,recno2,h2)) ->
+  | (_,h1,_,_,C.Fixpoint (true,fl,_)), Ref.Ref (_,Ref.Fix (i,recno2,h2)) ->
       let _,_,recno1,arity,_ = List.nth fl i in
       if h1 <> h2 || recno1 <> recno2 then error ();
       arity