]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/freshNamesGenerator.ml
rebuilt against ocaml 3.08.3
[helm.git] / helm / ocaml / cic_unification / freshNamesGenerator.ml
index 3bdde5b593426125143aa874e904feb1069d1e4b..fbb90552aa9e4293792743a3329e248c9b24ae90 100644 (file)
@@ -34,7 +34,10 @@ let mk_fresh_name ~subst metasenv context name ~typ =
       C.Anonymous ->
        (*CSC: great space for improvements here *)
        (try
-         (match CicTypeChecker.type_of_aux' ~subst metasenv context typ with
+        let ty,_ = 
+          CicTypeChecker.type_of_aux' ~subst metasenv context typ 
+            CicUniv.empty_ugraph in 
+         (match ty with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"