From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Dec 2001 12:00:39 +0000 (+0000)
Subject: Bug fixed: the strictly_positive condition was unnecessarily too tight.
X-Git-Tag: mlminidom_0_2_2~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afb33189adbdcd6f9b62a3c8718e9a514ddcffbe;p=helm.git

Bug fixed: the strictly_positive condition was unnecessarily too tight.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 569e44674..6529fede1 100644
--- 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 *)