More uris ported to V8.0.

diff --git a/helm/ocaml/cic_transformations/contentTable.ml b/helm/ocaml/cic_transformations/contentTable.ml
index 7950ce2846e6116c16e0881a8d8e760bc2eb592c..c41a8386aafb7008988f74bc05ce95c3b879334f 100644 (file)
--- a/helm/ocaml/cic_transformations/contentTable.ml
+++ b/helm/ocaml/cic_transformations/contentTable.ml
@@ -14,44 +14,32 @@ let add_symbol uri mnemonic =
 ;;
 
 (* eq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" 
-  (fun aid sid args ast_of_acic ->
-    idref aid (CicAst.Appl
-      (idref sid (CicAst.Symbol ("eq", 0)) ::
-        List.map ast_of_acic (List.tl args)))) ;;
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" 
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
   (fun aid sid args ast_of_acic ->
     idref aid (CicAst.Appl
       (idref sid (CicAst.Symbol ("eq", 0)) ::
         List.map ast_of_acic (List.tl args)))) ;;
 
 (* and *)
-add_symbol "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" "and" ;;
+add_symbol HelmLibraryObjects.Logic.and_XURI "and" ;;
 
 (* or *)
-add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;;
+add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;;
 
 (* iff *)
-add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;;
+add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;;
 
 (* not *)
-add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;;
+add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;;
 
 (* Rinv *)
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;;
+add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;;
 
 (* Ropp *)
-add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "opp" ;;
+add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;;
 
 (* exists *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" 
-  (fun aid sid args ast_of_acic ->
-   match (List.tl args) with
-     [Cic.ALambda (_,n,s,t)] ->
-       idref aid
-        (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
-  | _ -> raise Not_found);;
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" 
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
   (fun aid sid args ast_of_acic ->
    match (List.tl args) with
      [Cic.ALambda (_,n,s,t)] ->
@@ -60,30 +48,29 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
   | _ -> raise Not_found);;
 
 (* leq *) 
-add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;;
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;;
+add_symbol HelmLibraryObjects.Peano.le_XURI "leq" ;;
+add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;;
 
 (* lt *)
-add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;;
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;;
+add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;;
+add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;;
 
 (* geq *)
-add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;;
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;;
+add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;;
+add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;;
 
 (* gt *)
-add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;;
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;;
+add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;;
+add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;;
 
 (* plus *)
-add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;;
-add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "plus" ;;
+add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;;
+add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;;
 
-let rplus_uri =
-  UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
-let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
+let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;;
+let r1_uri = HelmLibraryObjects.Reals.r1_URI;;
 
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
   (fun aid sid args ast_of_acic ->
     let appl () =
       idref aid (CicAst.Appl 
@@ -104,19 +91,19 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
 ;;
 
 (* zero and one *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
   (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" 
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
   (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
 
 (* times *) 
-add_symbol "cic:/Coq/Init/Peano/mult.con" "times" ;;
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rmult.con" "times" ;;
+add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;;
+add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;;
 
 (* minus *)
-add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;;
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;;
+add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;;
+add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;;
 
 (* div *)
-add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;;
+add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;;