ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 4d0708ae5cfd92169b7f3c6d6c77ea67d533d156..65216f5d6a1677ce8f943150601fce54184e720d 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -232,48 +232,48 @@ Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
 
 (* zero and one *)
 
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
   (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
 
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
   (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
 
 (* times *) 
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "times",
-          None, Some "cic:/Coq/Init/Peano/mult.con"))
+          None, Some HelmLibraryObjects.Peano.mult_SURI))
      :: List.map acic2cexpr args));;
 
 
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "times",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
+          None, Some HelmLibraryObjects.Reals.rmult_SURI))
      :: List.map acic2cexpr args));;
 (* minus *)
-Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "minus",
-          None, Some "cic:/Coq/Arith/Minus/mult.con"))
+          None, Some HelmLibraryObjects.Peano.minus_SURI))
      :: List.map acic2cexpr args));;
 
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "minus",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
+          None, Some HelmLibraryObjects.Reals.rminus_SURI))
      :: List.map acic2cexpr args));;
 
 (* div *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "div",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
+          None, Some HelmLibraryObjects.Reals.rdiv_SURI))
      :: List.map acic2cexpr args));;
 
 
@@ -286,17 +286,18 @@ let string_of_sort =
   function 
     Cic.Prop  -> "Prop"
   | Cic.Set   -> "Set"
-  | Cic.Type  -> "Type"
+  | Cic.Type _ -> "Type" (* TASSI *)
   | Cic.CProp -> "Type"
 ;;
 
 let get_constructors uri i =
   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 i in
    constructors
@@ -370,7 +371,8 @@ let acic2cexpr ids_to_inner_sorts t =
           make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
         let inductive_types = 
-          (match CicEnvironment.get_obj uri with
+          (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
@@ -398,7 +400,8 @@ let acic2cexpr ids_to_inner_sorts t =
             make_subst subst, Some (UriManager.string_of_uri uri)))
     | C.AMutInd (id,uri,i,subst) ->
         let inductive_types = 
-          (match CicEnvironment.get_obj uri with
+          (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