Glob_term now mli-only, operations now in Glob_ops

Stuff about reductions now in genredexpr.mli, operations in redops.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 8 insertions, 70 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 1eb982b03..4e0eac128 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -44,7 +44,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     try Pretyping.understand_ltac ~resolve_classes:true true 
       sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
-      let loc = Glob_term.loc_of_glob_constr rawc in
+      let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3361752ed..3a5d2139b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -27,6 +27,7 @@ open Type_errors
 open Retyping
 open Evarutil
 open Tacexpr
+open Misctypes
 
 type refiner_error =
 
@@ -264,7 +265,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	      (first, d::middle)
             else
 	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
-	        Tacops.pr_move_location pr_id hto ++
+	        Miscops.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
           else
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 876982407..61e89ac1d 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -19,6 +19,7 @@ open Glob_term
 open Genarg
 open Nametab
 open Pattern
+open Misctypes
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 10e2ad323..3476eaaab 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -17,6 +17,7 @@ open Glob_term
 open Genarg
 open Nametab
 open Pattern
+open Misctypes
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 6b8fbf24b..ca0c7dd0d 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -3,7 +3,6 @@ Evar_refiner
 Proofview
 Proof
 Proof_global
-Tacops
 Proof_type
 Redexpr
 Logic
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 21948b481..12aec9142 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -13,7 +13,7 @@ open Names
 open Term
 open Declarations
 open Libnames
-open Glob_term
+open Genredexpr
 open Pattern
 open Reductionops
 open Tacred
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 99f942e11..6282abd9f 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -10,7 +10,7 @@ open Names
 open Term
 open Closure
 open Pattern
-open Glob_term
+open Genredexpr
 open Reductionops
 open Termops
 open Locus
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 86a1edd76..26fb3d466 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -19,6 +19,7 @@ open Tacexpr
 open Glob_term
 open Pattern
 open Locus
+open Misctypes
 
 (** Operations for handling terms under a local typing context. *)
 
diff --git a/proofs/tacops.ml b/proofs/tacops.ml
deleted file mode 100644
index 05c4e6093..000000000
--- a/proofs/tacops.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Topconstr
-open Libnames
-open Nametab
-open Glob_term
-open Errors
-open Util
-open Genarg
-open Pattern
-open Decl_kinds
-open Misctypes
-open Locus
-open Tacexpr
-
-let make_red_flag =
-  let rec add_flag red = function
-    | [] -> red
-    | FBeta :: lf -> add_flag { red with rBeta = true } lf
-    | FIota :: lf -> add_flag { red with rIota = true } lf
-    | FZeta :: lf -> add_flag { red with rZeta = true } lf
-    | FConst l :: lf ->
-	if red.rDelta then
-	  error
-	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag { red with rConst = list_union red.rConst l } lf
-    | FDeltaBut l :: lf ->
-	if red.rConst <> [] & not red.rDelta then
-	  error
-	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag
-	  { red with rConst = list_union red.rConst l; rDelta = true }
-	  lf
-  in
-  add_flag
-    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
-
-open Pp
-
-let pr_move_location pr_id = function
-  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
-  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
-  | MoveFirst -> str " at top"
-  | MoveLast -> str " at bottom"
diff --git a/proofs/tacops.mli b/proofs/tacops.mli
deleted file mode 100644
index be17e035a..000000000
--- a/proofs/tacops.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-val make_red_flag :
- Tacexpr.glob_red_flag list ->
- (Libnames.reference Misctypes.or_by_notation) Glob_term.glob_red_flag
-
-val pr_move_location :
-  ('a -> Pp.std_ppcmds) -> 'a Tacexpr.move_location -> Pp.std_ppcmds