Porting URIs to V8.0.

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index 83f2d36479015f3d0626c6959a9b3a640a451c2b..3ff0163d2c6880b4520af7c8698e5c66ce092a4b 100644 (file)
--- a/helm/ocaml/cic/helmLibraryObjects.ml
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -80,15 +80,6 @@ module Logic =
     let absurd_URI = uri "cic:/Coq/Init/Logic/absurd.con"
   end
 
-module Logic_Type =
-  struct
-    let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
-    let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
-
-    let refl_eqt = mutconstruct eqt_URI 0 1
-    let sym_eqt = const sym_eqt_URI
-  end
-
 module Datatypes =
   struct
     let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"

diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml
index 51faaa6acc06a91e6cc1d400e661b92217c203a1..324501eb31055db58aab1d8f4f70a1dc4db440d2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/arit_notation.ml
+++ b/helm/ocaml/cic_disambiguation/arit_notation.ml
@@ -120,16 +120,3 @@ let _ =
           Cic.Appl [
             Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
               Cic.Implicit (Some `Type); t1; t2 ] ]));
-  DisambiguateChoices.add_symbol_choice "neq"
-    ("not equal to (sort Type)",
-      (fun env _ args ->
-        let t1, t2 =
-          match args with
-          | [t1; t2] -> t1, t2
-          | _ -> raise DisambiguateChoices.Invalid_choice
-        in
-        Cic.Appl [ const HelmLibraryObjects.Logic.not_URI;
-          Cic.Appl [
-            Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []);
-              Cic.Implicit (Some `Type); t1; t2 ] ]));
-

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index 885cc214058e43be72c58595497b6f35e8780022..f622ce034e8312b59609807cb6c88b9a7d34f0a9 100644 (file)
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -74,7 +74,7 @@ let _ =
          | _ -> raise DisambiguateChoices.Invalid_choice
        in
        Cic.Appl [
-         Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []);
+         Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
            Cic.Implicit (Some `Type); t1; t2
        ]));
   DisambiguateChoices.add_binary_op "and" "logical and"

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)::_)) ->

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index bd9c1513661ba61d6abc8561cbb1ced948e7594e..fb5caa302cc85f59fb4292f2f36b94f7987f313f 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -190,7 +190,7 @@ exception GoalUnringable
   *)
 let ringable =
   let is_equality = function
-    | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true
+    | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
     | _ -> false
   in
   let is_real = function
@@ -447,7 +447,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) =
   *)
 let ring_tac ~status:((proof, goal) as status) =
   warn "in Ring tactic";
-  let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in
+  let eqt = mkMutInd (Logic.eq_URI, 0) [] in
   let r = Reals.r in
   let metasenv = metasenv_of_status ~status in
   let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
@@ -473,7 +473,7 @@ let ring_tac ~status:((proof, goal) as status) =
             "exact sym_eqt su t1 ...", exact_tac
             ~term:(
               Cic.Appl
-               [mkConst Logic_Type.sym_eqt_URI
+               [mkConst Logic.sym_eq_URI
                  [equality_is_a_congruence_A, Reals.r;
                   equality_is_a_congruence_x, t1'' ;
                   equality_is_a_congruence_y, t1
@@ -511,7 +511,7 @@ let ring_tac ~status:((proof, goal) as status) =
                       exact_tac
                        ~term:(
                          Cic.Appl
-                          [mkConst Logic_Type.sym_eqt_URI
+                          [mkConst Logic.sym_eq_URI
                             [equality_is_a_congruence_A, Reals.r;
                              equality_is_a_congruence_x, t2'' ;
                              equality_is_a_congruence_y, t2