CProp hierarchy is there!

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

diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
index 1cb86b35abfad49738f4d79f8fb8c2c7490e3b8a..daa0e5432a43cf1d12e6daa1e33740fe70fb0564 100755 (executable)
--- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
+++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
@@ -30,7 +30,7 @@ let debug_print = fun _ -> ()
 let rec higher_name arity =
   function 
       Cic.Sort Cic.Prop
-    | Cic.Sort Cic.CProp -> 
+    | Cic.Sort (Cic.CProp _) -> 
        if arity = 0 then "A" (* propositions *)
        else if arity = 1 then "P" (* predicates *)
        else "R" (*relations *)
@@ -87,7 +87,7 @@ let mk_fresh_name ~subst metasenv context name ~typ =
         in 
          (match ty with
              C.Sort C.Prop
-           | C.Sort C.CProp -> "H"
+           | C.Sort (C.CProp _) -> "H"
            | _ -> guess_a_name context typ
          )
         with CicTypeChecker.TypeCheckerFailure _ -> "H"