X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=9e91eeb07fad9f5f58a20bd3b94c873660397cff;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;hp=4a349e54c4a6976ede342383052f034dcbf124d1;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 4a349e54c..9e91eeb07 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -23,6 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
+open HelmLibraryObjects
 
 let rec injection_tac ~term ~status:((proof, goal) as status) = 
   let module C = Cic in
@@ -34,8 +35,8 @@ let rec injection_tac ~term ~status:((proof, goal) as status) =
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in  
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
-             or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+             when (U.eq equri Logic.eq_URI)
+             or (U.eq equri Logic_Type.eqt_URI) -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
@@ -86,8 +87,8 @@ and injection1_tac ~term ~i ~status:((proof, goal) as status) =
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
       match termty with (* an equality *)
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-            when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
-            or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+            when (U.eq equri Logic.eq_URI) or
+            (U.eq equri Logic_Type.eqt_URI) -> (
           match tty with (* some inductive type *)
              (C.MutInd (turi,typeno,exp_named_subst))
            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -210,8 +211,7 @@ let discriminate'_tac ~term ~status:((proof, goal) as status) =
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
-          when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) 
-            or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+          when (U.eq equri Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -275,8 +275,8 @@ prerr_endline ("XXXX nth funzionano ") ;
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
-                                     else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
+                                     then (C.MutInd(Logic.false_URI,0,[]))
+                                     else (C.MutInd(Logic.true_URI,0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -285,7 +285,7 @@ prerr_endline ("XXXX nth funzionano ") ;
 
                     let (proof',goals') = 
                      EliminationTactics.elim_type_tac 
-                      ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ) 
+                      ~term:(C.MutInd(Logic.false_URI,0,[]))
                       ~status 
                     in
                      (match goals' with