X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=72699f7e3cb2b584da6617a278a1b1f611945abd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ff80809831a167aeb9fe94577ea9141360659051;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index ff8080983..72699f7e3 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -345,7 +345,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  let sort = 
                    (try
                      Hashtbl.find ids_to_inner_sorts idr 
-                    with Not_found -> `Type) in 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
                  if sort = `Prop then 
                     K.Premise 
                       { K.premise_id = gen_id premise_prefix seed;
@@ -358,7 +358,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  let sort = 
                    (try
                      Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> `Type) in 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
                  if sort = `Prop then 
                     K.Lemma 
                       { K.lemma_id = gen_id lemma_prefix seed;
@@ -370,7 +370,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  let sort = 
                    (try
                      Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> `Type) in 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
@@ -731,7 +731,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   let idarg = get_id arg in
                   let sortarg = 
                     (try (Hashtbl.find ids_to_inner_sorts idarg)
-                     with Not_found -> `Type) in
+                     with Not_found -> `Type (CicUniv.fresh())) in
                   let hdarg = 
                     if sortarg = `Prop then
                       let (co,bo) = 
@@ -816,7 +816,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   else 
                     let aid = get_id a in
                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
-                      with Not_found -> `Type) in
+                      with Not_found -> `Type (CicUniv.fresh())) in
                     if asort = `Prop then
                       K.ArgProof (aux a)
                     else K.Term a in