Bug fixed in check_sort_elimination in the case (not tested so far)

dummy = false, Prop vs Type.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 1db82a99fb48eeddcf63adb96c4a31575e2ca5e6..43805cf8b24f1dc692277d2ea738db580ad446b4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1299,21 +1299,19 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
         false,ugraph1
        else
          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
-           C.Sort C.Prop -> true,ugraph1
-         | (C.Sort C.Set | C.Sort C.CProp) ->
-             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-              match o with
-               C.InductiveDefinition (itl,_,_,_) ->
-                   let (_,_,_,cl) = List.nth itl i in
-                   (* is a singleton definition? *)
-                   List.length cl = 1,ugraph1
-             | _ ->
-                 raise (TypeCheckerFailure
-                         ("Unknown mutual inductive definition:" ^
-                          UriManager.string_of_uri uri))
-             )
-         | _ -> false,ugraph1
-         )
+              C.Sort C.Prop -> true,ugraph1
+           | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
+               (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 match o with
+                    C.InductiveDefinition (itl,_,_,_) ->
+                     let (_,_,_,cl) = List.nth itl i in
+                     (* is a singleton definition or the empty proposition? *)
+                     (List.length cl = 1 || List.length cl = 0),ugraph1
+                  | _ ->
+                   raise (TypeCheckerFailure
+                    ("Unknown mutual inductive definition:" ^
+                       UriManager.string_of_uri uri)))
+           | _ -> false,ugraph1)
    | ((C.Sort C.Set, C.Prod (name,so,ta)) 
    | (C.Sort C.CProp, C.Prod (name,so,ta)))
      when not need_dummy ->