sort CProp added

[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 62dc951aaa54deb58cc3fe0dc36dfa5e142a4fac..7521f0f90b0456ca0ec8c0bf4c4e9a2d18922c25 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1185,6 +1185,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Prop, C.Sort C.Set)
+   | (C.Sort C.Prop, C.Sort C.CProp)
    | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
        (match CicEnvironment.get_obj uri with
@@ -1198,8 +1199,13 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
               (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
        )
    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
-   | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
+   | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
+   | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
+      when need_dummy ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (itl,_,paramsno) ->
             let tys =
@@ -1220,7 +1226,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         res &&
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop -> true
-          | C.Sort C.Set ->
+          | (C.Sort C.Set | C.Sort C.CProp) ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,_) ->
                   let (_,_,_,cl) = List.nth itl i in
@@ -1233,13 +1239,15 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
              )
           | _ -> false
         )
-   | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
+   | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
+      when not need_dummy ->
        let res = CicReduction.are_convertible context so ind
        in
         res &&
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop
           | C.Sort C.Set  -> true
+         | C.Sort C.CProp -> true
           | C.Sort C.Type ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,paramsno) ->
@@ -1647,7 +1655,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->
@@ -1728,7 +1736,7 @@ and is_small context paramsno c =
       C.Prod (n,so,de) ->
        (*CSC: [] is an empty metasenv. Is it correct? *)
        let s = type_of_aux' [] context so in
-        (s = C.Sort C.Prop || s = C.Sort C.Set) &&
+        (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
         is_small_aux ((Some (n,(C.Decl so)))::context) de
     | _ -> true (*CSC: we trust the type-checker *)
  in