X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=f9755474c0a59cdd418665328ca663f7d542fbb1;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=8e592e61d842322d4173bc0e0b6dd6420a50abdc;hpb=17f33fa8cb65de1f3edcba6ac750bbdb4d061117;p=helm.git

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 8e592e61d..f9755474c 100644
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -49,11 +49,11 @@ let warn s =
 *)
 
 let equality_is_a_congruence_A =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
 let equality_is_a_congruence_x =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
 let equality_is_a_congruence_y =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
 
 let apolynomial_uri =
   uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
@@ -125,20 +125,6 @@ let cic_is_const ?(uri: uri option = None) term =
   *)
 let uri_of_proof ~proof:(uri, _, _, _) = uri
 
-  (**
-    @param metano meta list index
-    @param metasenv meta list (environment)
-    @raise Failure if metano is not found in metasenv
-    @return conjecture corresponding to metano in metasenv
-  *)
-let conj_of_metano metano =
-  try
-    List.find (function (m, _, _) -> m = metano)
-  with Not_found ->
-    failwith (
-      "Ring.conj_of_metano: " ^
-      (string_of_int metano) ^ " no such meta")
-
   (**
     @param status current proof engine status
     @raise Failure if proof is None
@@ -153,7 +139,7 @@ let metasenv_of_status ~status:((_,m,_,_), _) = m
   *)
 let context_of_status ~status:(proof, goal as status) =
   let metasenv = metasenv_of_status ~status:status in
-  let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
+  let _, context, _ = CicUtil.lookup_meta goal metasenv in
    context
 
 (** CIC TERM CONSTRUCTORS *)
@@ -204,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
@@ -448,7 +434,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) =
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in
-    let (_, context, _) = conj_of_metano goal metasenv in
+    let (_, context, _) = CicUtil.lookup_meta goal metasenv in
      let proof',goal' = aux count context status in
       assert (goal = goal') ;
       proof',[goal']
@@ -461,10 +447,10 @@ 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) = conj_of_metano goal metasenv in
+  let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
   match (build_segments ~terms:[t1; t2]) with
   | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
@@ -487,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
@@ -525,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