Bug fixed: the strictly_positive condition was unnecessarily too tight.

[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 569e4467455f3e112b47297c5fe807b4d9472859..6529fede1789e1e62ac821a10bd62e481ff506b4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -285,12 +285,6 @@ and strictly_positive n nn te =
             i &&
              weakly_positive (n+1) (nn+1) uri x
           ) cl' true
-   | C.MutInd (uri,_,i) ->
-      (match CicEnvironment.get_obj uri with
-          C.InductiveDefinition (tl,_,_) ->
-           List.length tl = 1
-        | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
-      )
    | t -> does_not_occur n nn t
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)