initial support for notation that specifies the precedence of term variables, that...

[helm.git] / helm / software / components / acic_content / acic2content.ml

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index b10464bdad1acd6133dd117709e9221f0be55b12..b1423c5ab8cd805670fe4817fcf538c05ebb4107 100644 (file)
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -427,7 +427,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
-                        CicEnvironment.get_obj CicUniv.empty_ugraph uri
+                        CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
                       in
                         match o with 
                           | Cic.InductiveDefinition (l,_,_,_) -> l 
@@ -612,7 +612,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-          (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+          (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
             match o with
                 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
@@ -780,7 +780,7 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-          (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+          (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
             match o with
                | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
                | _ -> assert false