- too strict check on left parameters of constructors in guarded by constructors...

- the cases Fixpont and CoFixpoint in guarded by constructors are useless code in the
  new kernel since:
    o  recursive/corecursive objects are now closed terms
    o  we do not allow (yet?) to pass co-recursive functions around
    o  we do check that the arguments of the application of a fix/cofix do not
       contain the function we are checking for GBC

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 17380336797d23b58f8a012794e6cd46232c169e..56119fce7c3ead8eed15d7521b2adf1b1ae48890 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -947,7 +947,6 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
          (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args))))
       in
       let left, args = HExtlib.split_nth paramsno tl in
-      List.for_all (does_not_occur ~subst context n nn) left &&
       analyse_instantiated_type rec_params args
    | C.Appl ((C.Match (_,out,te,pl))::_) 
    | C.Match (_,out,te,pl) as t ->
@@ -956,6 +955,9 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
        does_not_occur ~subst context n nn out &&
        does_not_occur ~subst context n nn te &&
        List.for_all (aux context n nn h) pl
+(* IMPOSSIBLE unsless we allow to pass cofix to other fix/cofix as we do for 
+   higher order fix in g_b_destructors.
+
    | C.Const (Ref.Ref (u,(Ref.Fix _| Ref.CoFix _)) as ref)
    | C.Appl(C.Const (Ref.Ref(u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t ->
       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
@@ -967,6 +969,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
        (fun (_,_,_,_,bo) ->
           aux (context@tys) n nn h (debruijn u len context bo))
        fl
+*)
    | C.Const _
    | C.Appl _ as t -> does_not_occur ~subst context n nn t
  in