Porting URIs to V8.0.

[helm.git] / helm / ocaml / tactics / discriminationTactics.ml

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 15d7968d34c5476e5192fa4c085c4d544bccc59f..5523c137ce80c3f539b632ef41580a60e9b690f5 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -35,8 +35,7 @@ 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 Logic.eq_URI)
-             or (U.eq equri Logic_Type.eqt_URI) -> (
+             when (U.eq equri Logic.eq_URI) -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
@@ -87,8 +86,7 @@ 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 Logic.eq_URI) or
-            (U.eq equri Logic_Type.eqt_URI) -> (
+            when (U.eq equri Logic.eq_URI) -> (
           match tty with (* some inductive type *)
              (C.MutInd (turi,typeno,exp_named_subst))
            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -211,7 +209,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 Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> (
+          when (U.eq equri Logic.eq_URI) -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->