rewritten instantiate code

[helm.git] / helm / software / components / ng_kernel / nCic2OCic.ml

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index d9edb1100c7d45340f97a907353decc2fc345c6d..1006d03c684e110e2ded288cd5915ff034436618 100644 (file)
--- a/helm/software/components/ng_kernel/nCic2OCic.ml
+++ b/helm/software/components/ng_kernel/nCic2OCic.ml
@@ -15,7 +15,7 @@ let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);;
 
 let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;;
 
-let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+let cprop = [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")];;
 
 let nn_2_on = function
   | "_" -> Cic.Anonymous
@@ -37,7 +37,7 @@ let convert_term uri n_fl t =
  | NCic.Sort (NCic.Type u) when
     (* BUG HERE: I should use NCicEnvironment.universe_eq, but I do not
        want to add this recursion between the modules *)
-    (*NCicEnvironment.universe_eq*) u=cprop -> Cic.Sort Cic.CProp 
+    (*NCicEnvironment.universe_eq*) u=cprop -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
  | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
  | NCic.Implicit _ -> assert false
  | NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) ->