Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 49e2e23ad11e738442faa10d8dca38c597ba937a..56459d197278ac902d9e731f7b45647dfead2061 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -368,11 +368,14 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                     with Not_found -> "Type") in 
                  if sort ="Prop" then 
                     let inductive_types =
-                      (match CicEnvironment.get_obj uri with
-                         Cic.Constant _ -> assert false
-                       | Cic.Variable _ -> assert false
-                       | Cic.CurrentProof _ -> assert false
-                       | Cic.InductiveDefinition (l,_,_) -> l 
+                      (let o,_ = 
+                        CicEnvironment.get_obj uri CicUniv.empty_ugraph 
+                      in
+                        match o with 
+                             Cic.Constant _ -> assert false
+                          | Cic.Variable _ -> assert false
+                          | Cic.CurrentProof _ -> assert false
+                          | Cic.InductiveDefinition (l,_,_) -> l 
                       ) in
                     let (_,_,_,constructors) = 
                       List.nth inductive_types tyno in 
@@ -538,12 +541,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-           (match CicEnvironment.get_obj uri with
-               Cic.Constant _ -> assert false
-             | Cic.Variable _ -> assert false
-             | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> l,n 
-           ) in
+          (let o, _ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+            match o with
+                Cic.Constant _ -> assert false
+               | Cic.Variable _ -> assert false
+               | Cic.CurrentProof _ -> assert false
+               | Cic.InductiveDefinition (l,_,n) -> l,n 
+          ) in
         let (_,_,_,constructors) = List.nth inductive_types typeno in
         let name_and_arities = 
           let rec count_prods =
@@ -686,12 +690,13 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-           (match CicEnvironment.get_obj ind_uri with
-               Cic.Constant _ -> assert false
-             | Cic.Variable _ -> assert false
-             | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> (l,n) 
-           ) in
+          (let o,_ = CicEnvironment.get_obj ind_uri CicUniv.empty_ugraph in
+            match o with
+                Cic.Constant _ -> assert false
+               | Cic.Variable _ -> assert false
+               | Cic.CurrentProof _ -> assert false
+               | Cic.InductiveDefinition (l,_,n) -> (l,n) 
+          ) in
         let rec split n l =
           if n = 0 then ([],l) else
           let p,a = split (n-1) (List.tl l) in