From 8d4d4ff40606138ea72668cf46a95c776d2f1b7c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 May 2008 11:51:14 +0000 Subject: [PATCH] ref sync check fixed controlling fix/cofix coherence --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2