X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=5fe5bc3dcc8f87e3023581188e76745c4e23e22d;hb=09d156a3f1ee9ebaccc9dc971734aa94509ca51a;hp=4d0708ae5cfd92169b7f3c6d6c77ea67d533d156;hpb=f88549d5f75107867c34e2300bd4199d4d6e80b2;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 4d0708ae5..5fe5bc3dc 100644
--- 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));;