X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=590b482c716db80b74b83429aa4808fbb804aa38;hb=fafa203bb8521f516a0e87ef28d2cedccb72f795;hp=901540b6f63685eb69c635ab15fe9a247e3b87b0;hpb=25ec5b95fe67bbdee888a8268b3772a394cd74a5;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 901540b6f..590b482c7 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-open HelmLibraryObjects
-
 let debug_print = fun _ -> ()
 
 let rec injection_tac ~term =
@@ -41,7 +39,7 @@ let rec injection_tac ~term =
     ProofEngineTypes.apply_tactic
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri Logic.eq_URI) -> (
+             when LibraryObjects.is_eq_URI equri -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
@@ -97,7 +95,7 @@ and injection1_tac ~term ~i =
      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      match termty with (* an equality *)
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri Logic.eq_URI) -> (
+             when LibraryObjects.is_eq_URI equri -> (
            match tty with (* some inductive type *)
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -219,7 +217,7 @@ let discriminate'_tac ~term =
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
-          when (U.eq equri Logic.eq_URI) -> (
+          when LibraryObjects.is_eq_URI equri -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -278,8 +276,8 @@ let discriminate'_tac ~term =
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd(Logic.false_URI,0,[]))
-                                     else (C.MutInd(Logic.true_URI,0,[]))
+                                     then (C.MutInd(LibraryObjects.false_URI (),0,[]))
+                                     else (C.MutInd(LibraryObjects.true_URI (),0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -289,7 +287,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
 		     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(Logic.false_URI,0,[])))
+                       (C.MutInd(LibraryObjects.false_URI (),0,[])))
                       status 
                     in
                      (match goals' with