is_small did not use the environment. Hence the List.nth exception. Fixed.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index c86a27ad04e89c3424ebff3b5c7ed8f8cd6be9e6..5c3dc08f1dc33c61cec2e09e34e8f5ef86ed51f5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -905,17 +905,7 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (itl,_,_) ->
             let (_,_,_,cl) = List.nth itl i in
-             (* is a small inductive type? *)
-             (*CSC: ottimizzare calcolando staticamente *)
-             let rec is_small =
-              function
-                 C.Prod (_,so,de) ->
-                  let s = type_of so in
-                   (s = C.Sort C.Prop || s = C.Sort C.Set) &&
-                   is_small de
-               | _ -> true (*CSC: we trust the type-checker *)
-             in
-              List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
+             List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
          | _ ->
            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
        )
@@ -949,16 +939,7 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,_) ->
                   let (_,_,_,cl) = List.nth itl i in
-                   (* is a small inductive type? *)
-                   let rec is_small =
-                    function
-                       C.Prod (_,so,de) ->
-                        let s = type_of so in
-                         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
-                         is_small de
-                     | _ -> true (*CSC: we trust the type-checker *)
-                   in
-                    List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
+                   List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
                | _ ->
                  raise (WrongUriToMutualInductiveDefinitions
                   (U.string_of_uri uri))
@@ -992,7 +973,8 @@ and type_of_branch argsno need_dummy outtype term constype =
   | _ -> raise (Impossible 20)
        
  
-and type_of t =
+(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
+and type_of_aux' env t =
  let rec type_of_aux env =
   let module C = Cic in
   let module R = CicReduction in
@@ -1225,7 +1207,24 @@ and type_of t =
       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
     )
  in
-  type_of_aux [] t
+  type_of_aux env t
+
+(* is a small constructor? *)
+(*CSC: ottimizzare calcolando staticamente *)
+and is_small c =
+ let rec is_small_aux env c =
+  let module C = Cic in
+   match CicReduction.whd c with
+      C.Prod (_,so,de) ->
+       let s = type_of_aux' env so in
+        (s = C.Sort C.Prop || s = C.Sort C.Set) &&
+        is_small_aux (so::env) de
+    | _ -> true (*CSC: we trust the type-checker *)
+ in
+  is_small_aux [] c
+
+and type_of t =
+ type_of_aux' [] t
 ;;
 
 let typecheck uri =