From afb33189adbdcd6f9b62a3c8718e9a514ddcffbe Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Dec 2001 12:00:39 +0000
Subject: [PATCH] Bug fixed: the strictly_positive condition was unnecessarily
 too tight.

---
 helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 6 ------
 1 file changed, 6 deletions(-)

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 *)
-- 
2.39.2