X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualParser.mly;h=3ca69d5c6d59ba9f0fd3701942f6c58a8f8ba97f;hb=b3bfd6b249600b15552c890306a635aee30c2a74;hp=f6f557947a0598509c1ce9c45f66fc0f79b99009;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index f6f557947..3ca69d5c6 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -184,20 +184,13 @@ expr2:
    { [], function interp ->
       let rec cic_real_of_real =
        function
-          0 ->
-           Cic.Const
-            (UriManager.uri_of_string
-              "cic:/Coq/Reals/Rdefinitions/R0.con",[])
-        | 1 ->
-           Cic.Const
-            (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con",[])
+          0 -> Cic.Const (HelmLibraryObjects.Reals.r0_URI, [])
+        | 1 -> Cic.Const (HelmLibraryObjects.Reals.r1_URI,[])
         | n ->
           Cic.Appl
            [ Cic.Const
-               (UriManager.uri_of_string
-                  "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
-             Cic.Const (UriManager.uri_of_string
-              "cic:/Coq/Reals/Rdefinitions/R1.con",[]);
+               (HelmLibraryObjects.Reals.rplus_URI,[]) ;
+             Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);
              cic_real_of_real (n - 1)
            ]
       in
@@ -208,14 +201,10 @@ expr2:
       let rec cic_int_of_int =
        function
           0 ->
-           Cic.MutConstruct
-            (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
-             0,1,[])
+           Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,1,[])
         | n ->
           Cic.Appl
-           [ Cic.MutConstruct
-              (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
-               0,2,[]) ;
+           [ Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,2,[]) ;
              cic_int_of_int (n - 1)
            ]
       in
@@ -227,9 +216,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string
-              "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -240,9 +227,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string
-              "cic:/Coq/Reals/Rdefinitions/Rminus.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Reals.rminus_URI,[]);
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -253,9 +238,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string
-              "cic:/Coq/Reals/Rdefinitions/Rmult.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Reals.rmult_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -266,9 +249,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string
-              "cic:/Coq/Reals/Rdefinitions/Rdiv.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Reals.rdiv_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -279,8 +260,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -291,8 +271,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Peano.minus_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -303,42 +282,11 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
-          (mk_expr1 interp) ;
-          (mk_expr2 interp)
-         ]
-   }
- | expr2 EQT expr2
-   { let dom1,mk_expr1 = $1 in
-     let dom2,mk_expr2 = $3 in
-     let dom3,mk_expr3 = mk_implicit () in
-      let dom = union dom1 (union dom2 dom3) in
-       dom, function interp ->
-        Cic.Appl
-         [Cic.MutInd
-           (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
-          (mk_expr3 interp) ;
+         [Cic.Const (HelmLibraryObjects.Peano.mult_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
    }
- | expr2 NEQT expr2
-   { let dom1,mk_expr1 = $1 in
-     let dom2,mk_expr2 = $3 in
-     let dom3,mk_expr3 = mk_implicit () in
-      let dom = union dom1 (union dom2 dom3) in
-       dom, function interp ->
-        Cic.Appl [
-         Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]);
-         Cic.Appl
-          [Cic.MutInd
-            (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
-           (mk_expr3 interp) ;
-           (mk_expr1 interp) ;
-           (mk_expr2 interp)
-          ]]
-   }
  | expr2 EQ expr2
    { let dom1,mk_expr1 = $1 in
      let dom2,mk_expr2 = $3 in
@@ -346,8 +294,7 @@ expr2:
       let dom = union dom1 (union dom2 dom3) in
        dom, function interp ->
         Cic.Appl
-         [Cic.MutInd
-           (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ;
+         [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI,0,[]) ;
           (mk_expr3 interp) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)