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 42faf7e6ab6f2708672074802b9a79882b8ee36d..464aa7c2a539da78633a935b1719fc36ba64a751 100644 (file)
--- 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