ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 6678d509cbcb9ad15f33c7e5e1f0b64be3d6f2b4..af98ff0efc72b53acfd7d7e8b225e45272a166f4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1308,18 +1308,18 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
            let itl_len = List.length itl in
            let (name,_,ty,cl) = List.nth itl i in
            let cl_len = List.length cl in
-            if (itl_len = 1 && cl_len <= 1) then
+            if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
              let non_informative,ugraph =
               if cl_len = 0 then true,ugraph
               else
                is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
                 paramsno (snd (List.nth cl 0)) ugraph
              in
-              (* is a singleton or empty non recursive and non informative
+              (* is it a singleton or empty non recursive and non informative
                  definition? *)
               non_informative, ugraph
             else
-             false,ugraph
+              false,ugraph
          | _ ->
              raise (TypeCheckerFailure 
                     (lazy ("Unknown mutual inductive definition:" ^