Huge commit with several changes:

[helm.git] / helm / software / components / cic_proof_checking / cicPp.ml

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 1686cd3572ab57d09a255d9a47f5c6409db367bb..97213404e7244a0b8c082b68b44f1d12bf14d53c 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -114,7 +114,7 @@ let rec pp t l =
          | C.Set   -> "Set"
          | C.Type _ -> "Type"
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
-        | C.CProp -> "CProp" 
+        | C.CProp _ -> "CProp" 
        )
     | C.Implicit (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
@@ -347,7 +347,7 @@ let ppsort = function
   | Cic.Prop -> "Prop"
   | Cic.Set -> "Set"
   | Cic.Type _ -> "Type"
-  | Cic.CProp -> "CProp"
+  | Cic.CProp _ -> "CProp"
 
 
 (* MATITA NAMING CONVENTION *)
@@ -412,7 +412,7 @@ let rec check_rec ctx string_name =
     | Cic.Cast (te,ty) -> check_rec ctx string_name te
     | Cic.Prod (name,so,dest) -> 
        let l_string_name = check_rec ctx string_name so in
-       check_rec (name::ctx) string_name dest
+       check_rec (name::ctx) l_string_name dest
     | Cic.Lambda (name,so,dest) -> 
         let string_name =
           match name with