Comestic changes.

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index ab7bde56f8dfa4049ca0989ccb55e64d3ac7eada..298a87f3c8df8361fc4bcaee9f9cbaa5dc12c5d9 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -28,8 +28,6 @@ open PrimitiveTactics
 open ProofEngineTypes
 open UriManager
 
-open HelmLibraryObjects
-
 (** DEBUGGING *)
 
   (** perform debugging output? *)
@@ -192,11 +190,11 @@ exception GoalUnringable
   *)
 let ringable =
   let is_equality = function
-    | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
+    | Cic.MutInd (uri, 0, []) when (eq uri HelmLibraryObjects.Logic.eq_URI) -> true
     | _ -> false
   in
   let is_real = function
-    | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
+    | Cic.Const (uri, _) when (eq uri HelmLibraryObjects.Reals.r_URI) -> true
     | _ -> false
   in
   function
@@ -254,7 +252,7 @@ let path_of_int n =
     @return a cic term representing the variable map containing vars variables
   *)
 let btree_of_array ~vars =
-  let r = Reals.r in
+  let r = HelmLibraryObjects.Reals.r in
   let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
   let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
   let size = Array.length vars in
@@ -287,17 +285,17 @@ let abstract_poly ~terms =
   let rec aux = function  (* TODO not tail recursive *)
     (* "bop" -> binary operator | "uop" -> unary operator *)
     | Cic.Appl (bop::t1::t2::[])
-      when (cic_is_const ~uri:(Some Reals.rplus_URI) bop) -> (* +. *)
+      when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rplus_URI) bop) -> (* +. *)
         Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
     | Cic.Appl (bop::t1::t2::[])
-      when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *)
+      when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rmult_URI) bop) -> (* *. *)
         Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
     | Cic.Appl (uop::t::[])
-      when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *)
+      when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.ropp_URI) uop) -> (* ~-. *)
         Cic.Appl [mkCtor apopp_uri []; aux t]
-    | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *)
+    | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r0_URI) t) -> (* 0. *)
         mkCtor ap0_uri []
-    | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *)
+    | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r1_URI) t) -> (* 1. *)
         mkCtor ap1_uri []
     | t ->  (* variable *)
       try
@@ -328,20 +326,20 @@ let abstract_poly ~terms =
   *)
 let build_segments ~terms =
   let theory_args_subst varmap =
-   [abstract_rings_A_uri, Reals.r ;
-    abstract_rings_Aplus_uri, Reals.rplus ;
-    abstract_rings_Amult_uri, Reals.rmult ;
-    abstract_rings_Aone_uri, Reals.r1 ;
-    abstract_rings_Azero_uri, Reals.r0 ;
-    abstract_rings_Aopp_uri, Reals.ropp ;
+   [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
+    abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
+    abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
+    abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
+    abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
+    abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
     abstract_rings_vm_uri, varmap] in
   let theory_args_subst' eq varmap t =
-   [abstract_rings_A_uri, Reals.r ;
-    abstract_rings_Aplus_uri, Reals.rplus ;
-    abstract_rings_Amult_uri, Reals.rmult ;
-    abstract_rings_Aone_uri, Reals.r1 ;
-    abstract_rings_Azero_uri, Reals.r0 ;
-    abstract_rings_Aopp_uri, Reals.ropp ;
+   [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
+    abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
+    abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
+    abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
+    abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
+    abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
     abstract_rings_Aeq_uri, eq ;
     abstract_rings_vm_uri, varmap ;
     abstract_rings_T_uri, t] in
@@ -353,8 +351,8 @@ let build_segments ~terms =
   let apolynomial_normalize_ok eq varmap t =
    mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
   let lxy_false =   (** Cic funcion "fun (x,y):R -> false" *)
-    Cic.Lambda (Cic.Anonymous, Reals.r,
-      Cic.Lambda (Cic.Anonymous, Reals.r, Datatypes.falseb))
+    Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r,
+      Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r, HelmLibraryObjects.Datatypes.falseb))
   in
   let (aterms, varmap) = abstract_poly ~terms in  (* abstract polys *)
   List.map    (* build ring segments *)
@@ -362,7 +360,7 @@ let build_segments ~terms =
      Cic.Appl [interp_ap varmap ; t],
      Cic.Appl (
        [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
-     Cic.Appl [apolynomial_normalize_ok lxy_false varmap Reals.rtheory ; t]
+     Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t]
    ) aterms
 
 
@@ -466,8 +464,8 @@ let purge_hyps_tac ~count =
 let ring_tac status =
   let (proof, goal) = status in
   warn "in Ring tactic";
-  let eqt = mkMutInd (Logic.eq_URI, 0) [] in
-  let r = Reals.r in
+  let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in
+  let r = HelmLibraryObjects.Reals.r in
   let metasenv = metasenv_of_status status in
   let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
@@ -492,8 +490,8 @@ let ring_tac status =
             "exact sym_eqt su t1 ...", exact_tac
             ~term:(
               Cic.Appl
-               [mkConst Logic.sym_eq_URI
-                 [equality_is_a_congruence_A, Reals.r;
+               [mkConst HelmLibraryObjects.Logic.sym_eq_URI
+                 [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
                   equality_is_a_congruence_x, t1'' ;
                   equality_is_a_congruence_y, t1
                  ] ;
@@ -534,8 +532,8 @@ let ring_tac status =
                       exact_tac
                        ~term:(
                          Cic.Appl
-                          [mkConst Logic.sym_eq_URI
-                            [equality_is_a_congruence_A, Reals.r;
+                          [mkConst HelmLibraryObjects.Logic.sym_eq_URI
+                            [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
                              equality_is_a_congruence_x, t2'' ;
                              equality_is_a_congruence_y, t2
                             ] ;