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

55 files changed, 268 insertions, 334 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 436fa287f..c3b5742ac 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -73,7 +73,8 @@ Miscops
 Termops
 Namegen
 Evd
-Glob_term
+Glob_ops
+Redops
 Reductionops
 Inductiveops
 Retyping
@@ -115,7 +116,6 @@ Smartlocate
 Constrintern
 Modintern
 Constrextern
-Tacops
 Proof_type
 Goal
 Logic
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d45e6b9b3..62b8cdcea 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -23,6 +23,7 @@ open Libnames
 open Impargs
 open Topconstr
 open Glob_term
+open Glob_ops
 open Pattern
 open Nametab
 open Notation
@@ -876,7 +877,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
-      let loc = Glob_term.loc_of_glob_constr t in
+      let loc = Glob_ops.loc_of_glob_constr t in
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4467cf9f2..d125caf54 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -16,6 +16,7 @@ open Namegen
 open Libnames
 open Impargs
 open Glob_term
+open Glob_ops
 open Pattern
 open Pretyping
 open Cases
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b1bc63658..250871b9e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -82,7 +82,7 @@ val intern_gen : bool -> evar_map -> env ->
 
 val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
-    ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
+    ((Names.identifier * Names.identifier) list * cases_pattern) list
 
 val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 0368e99e0..de1fa0fef 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -12,6 +12,7 @@ open Names
 open Term
 open Libnames
 open Glob_term
+open Genredexpr
 open Pattern
 open Topconstr
 open Term
diff --git a/interp/notation.ml b/interp/notation.ml
index 72a713866..b6496f535 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -17,6 +17,7 @@ open Nametab
 open Libnames
 open Summary
 open Glob_term
+open Glob_ops
 open Topconstr
 open Ppextend
 (*i*)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3773305a..9ea6c7e4c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Libnames
 open Glob_term
+open Glob_ops
 open Term
 open Mod_subst
 open Misctypes
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
new file mode 100644
index 000000000..8aab193fd
--- /dev/null
+++ b/intf/genredexpr.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Reduction expressions *)
+
+(** The parsing produces initially a list of [red_atom] *)
+
+type 'a red_atom =
+  | FBeta
+  | FIota
+  | FZeta
+  | FConst of 'a list
+  | FDeltaBut of 'a list
+
+(** This list of atoms is immediately converted to a [glob_red_flag] *)
+
+type 'a glob_red_flag = {
+  rBeta : bool;
+  rIota : bool;
+  rZeta : bool;
+  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+  rConst : 'a list
+}
+
+(** Generic kinds of reductions *)
+
+type ('a,'b,'c) red_expr_gen =
+  | Red of bool
+  | Hnf
+  | Simpl of 'c Locus.with_occurrences option
+  | Cbv of 'b glob_red_flag
+  | Lazy of 'b glob_red_flag
+  | Unfold of 'b Locus.with_occurrences list
+  | Fold of 'a list
+  | Pattern of 'a Locus.with_occurrences list
+  | ExtraRedExpr of string
+  | CbvVm of 'c Locus.with_occurrences option
+
+type ('a,'b,'c) may_eval =
+  | ConstrTerm of 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
+  | ConstrContext of (Pp.loc * Names.identifier) * 'a
+  | ConstrTypeOf of 'a
diff --git a/pretyping/glob_term.mli b/intf/glob_term.mli
index f654925ef..93f391afa 100644
--- a/pretyping/glob_term.mli
+++ b/intf/glob_term.mli
@@ -6,22 +6,21 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(**Untyped intermediate terms, after constr_expr and before constr
+(** Untyped intermediate terms *)
+
+(** [glob_constr] comes after [constr_expr] and before [constr].
 
    Resolution of names, insertion of implicit arguments placeholder,
    and notations are done, but coercions, inference of implicit
    arguments and pattern-matching compilation are not. *)
 
-open Errors
 open Pp
 open Names
 open Sign
 open Term
 open Libnames
-open Nametab
 open Decl_kinds
 open Misctypes
-open Locus
 
 (**  The kind of patterns that occurs in "match ... with ... end"
 
@@ -31,8 +30,6 @@ type cases_pattern =
   | PatCstr of loc * constructor * cases_pattern list * name
       (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
 
-val cases_pattern_loc : cases_pattern -> loc
-
 type glob_constr =
   | GRef of (loc * global_reference)
   | GVar of (loc * identifier)
@@ -43,7 +40,7 @@ type glob_constr =
   | GProd of loc * name * binding_kind * glob_constr * glob_constr
   | GLetIn of loc * name * glob_constr * glob_constr
   | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
-      (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in 
+      (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
 	  [MatchStyle]) *)
 
   | GLetTuple of loc * name list * (name * glob_constr option) *
@@ -72,67 +69,6 @@ and tomatch_tuple = (glob_constr * predicate_pattern)
 and tomatch_tuples = tomatch_tuple list
 
 and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
-(** [(p,il,cl,t)] = "|'cl' => 't'" where FV(t) \subset il *)
+(** [(p,il,cl,t)] = "|'cl' as 'il' => 't'" *)
 
 and cases_clauses = cases_clause list
-
-val cases_predicate_names : tomatch_tuples -> name list
-
-(* Apply one argument to a glob_constr *)
-val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr
-
-val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr
-
-(* Ensure traversal from left to right *)
-val map_glob_constr_left_to_right :
-  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
-
-(*
-val map_glob_constr_with_binders_loc : loc ->
-  (identifier -> 'a -> identifier * 'a) ->
-  ('a -> glob_constr -> glob_constr) -> 'a -> glob_constr -> glob_constr
-*)
-
-val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
-val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
-val occur_glob_constr : identifier -> glob_constr -> bool
-val free_glob_vars : glob_constr -> identifier list
-val loc_of_glob_constr : glob_constr -> loc
-
-(** Conversion from glob_constr to cases pattern, if possible
-    
-    Take the current alias as parameter, 
-    @raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
-
-val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
-
-(** {6 Reduction expressions} *)
-
-type 'a glob_red_flag = {
-  rBeta : bool;
-  rIota : bool;
-  rZeta : bool;
-  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
-  rConst : 'a list
-}
-
-val all_flags : 'a glob_red_flag
-
-type ('a,'b,'c) red_expr_gen =
-  | Red of bool
-  | Hnf
-  | Simpl of 'c with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
-  | Unfold of 'b with_occurrences list
-  | Fold of 'a list
-  | Pattern of 'a with_occurrences list
-  | ExtraRedExpr of string
-  | CbvVm of 'c with_occurrences option
-
-type ('a,'b,'c) may_eval =
-  | ConstrTerm of 'a
-  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (loc * identifier) * 'a
-  | ConstrTypeOf of 'a
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 9d6820346..2aec5ed32 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -27,6 +27,13 @@ type intro_pattern_expr =
   | IntroAnonymous
 and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
 
 (** Sorts *)
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 16ba9f95e..d8e340d1e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -10,15 +10,13 @@ open Names
 open Topconstr
 open Libnames
 open Nametab
-open Glob_term
-open Errors
-open Pp
-open Util
+open Genredexpr
 open Genarg
 open Pattern
 open Decl_kinds
 open Misctypes
 open Locus
+open Pp
 
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
@@ -33,21 +31,6 @@ type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 
 type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
 
-type glob_red_flag =
-  | FBeta
-  | FIota
-  | FZeta
-  | FConst of reference or_by_notation list
-  | FDeltaBut of reference or_by_notation list
-
-type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
-
-type 'id move_location =
-  | MoveAfter of 'id
-  | MoveBefore of 'id
-  | MoveFirst
-  | MoveLast (* can be seen as "no move" when doing intro *)
-
 type 'a induction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of identifier located
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e2edbb096..811fd58ff 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -18,6 +18,7 @@ open Prim
 open Tactic
 open Tok
 open Misctypes
+open Genredexpr
 
 let fail_default_value = ArgArg 0
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 55c03a481..4c1d747ea 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -11,7 +11,7 @@ open Pcoq
 open Errors
 open Util
 open Tacexpr
-open Glob_term
+open Genredexpr
 open Genarg
 open Topconstr
 open Libnames
@@ -22,7 +22,7 @@ open Misctypes
 open Locus
 open Decl_kinds
 
-let all_with delta = Tacops.make_red_flag [FBeta;FIota;FZeta;delta]
+let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
 
 let tactic_kw = [ "->"; "<-" ; "by" ]
 let _ = List.iter Lexer.add_keyword tactic_kw
@@ -327,7 +327,7 @@ GEXTEND Gram
     ] ]
   ;
   strategy_flag:
-    [ [ s = LIST1 red_flag -> Tacops.make_red_flag s
+    [ [ s = LIST1 red_flag -> Redops.make_red_flag s
       | d = delta_flag -> all_with d
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 34e0d9532..83c5e6f31 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -819,7 +819,7 @@ GEXTEND Gram
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
       | IDENT "Compute"; c = lconstr ->
-	  fun g -> VernacCheckMayEval (Some (Glob_term.CbvVm None), g, c)
+	  fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c)
       | IDENT "Check"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 7c26ac124..50270f863 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -22,6 +22,7 @@ open Detyping
 open Tok
 open Misctypes
 open Decl_kinds
+open Genredexpr
 
 (* Generic xml parser without raw data *)
 
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index caf3d8508..c2dce0231 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -63,13 +63,12 @@ Evd
 Reductionops
 Inductiveops
 Miscops
-Glob_term
+Glob_ops
 Detyping
 Pattern
 Topconstr
 Genarg
 Ppextend
-Tacops
 Tok
 Lexer
 Extend
@@ -84,6 +83,7 @@ Argextend
 Tacextend
 Vernacextend
 
+Redops
 G_prim
 G_tactic
 G_ltac
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5bc6bddd9..e113bb711 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -18,6 +18,7 @@ open Tacexpr
 open Libnames
 open Compat
 open Misctypes
+open Genredexpr
 
 (** The parser of Coq *)
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 45ea77d13..6b2e206b6 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -18,12 +18,12 @@ open Ppextend
 open Topconstr
 open Term
 open Pattern
-open Glob_term
 open Constrextern
 open Termops
 open Decl_kinds
 open Misctypes
 open Locus
+open Genredexpr
 (*i*)
 
 let sep_v = fun _ -> str"," ++ spc()
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 1497c90e7..390869cf7 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -18,6 +18,7 @@ open Errors
 open Util
 open Misctypes
 open Locus
+open Genredexpr
 
 val extract_lam_binders :
   constr_expr -> local_binder list * constr_expr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 58ce29a04..5d03b6028 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -23,6 +23,7 @@ open Printer
 open Misctypes
 open Locus
 open Decl_kinds
+open Genredexpr
 
 let pr_global x = Nametab.pr_global_env Idset.empty x
 
@@ -650,7 +651,7 @@ and pr_atom1 = function
   | TacIntroMove (None,MoveLast) as t -> pr_atom0 t
   | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
   | TacIntroMove (ido,hto) ->
-      hov 1 (str"intro" ++ pr_opt pr_id ido ++ Tacops.pr_move_location pr_ident hto)
+      hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscops.pr_move_location pr_ident hto)
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -764,7 +765,7 @@ and pr_atom1 = function
       assert b;
       hov 1
         (str "move" ++ brk (1,1) ++ pr_ident id1 ++
-	 Tacops.pr_move_location pr_ident id2)
+	 Miscops.pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1
         (str "rename" ++ brk (1,1) ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 20fbda2d7..a932a608f 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -519,7 +519,7 @@ let pr_prim_rule = function
 
   | Move (withdep,id1,id2) ->
       (str (if withdep then "dependent " else "") ++
-	 str"move "  ++ pr_id id1 ++ Tacops.pr_move_location pr_id id2)
+	 str"move "  ++ pr_id id1 ++ Miscops.pr_move_location pr_id id2)
 
   | Order ord ->
       (str"order "  ++ pr_sequence pr_id ord)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index c4581fe1e..a75d1f6cc 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -108,17 +108,17 @@ let mlexpr_of_clause cl =
            Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >>
 
 let mlexpr_of_red_flags {
-  Glob_term.rBeta = bb;
-  Glob_term.rIota = bi;
-  Glob_term.rZeta = bz;
-  Glob_term.rDelta = bd;
-  Glob_term.rConst = l
+  Genredexpr.rBeta = bb;
+  Genredexpr.rIota = bi;
+  Genredexpr.rZeta = bz;
+  Genredexpr.rDelta = bd;
+  Genredexpr.rConst = l
 } = <:expr< {
-  Glob_term.rBeta = $mlexpr_of_bool bb$;
-  Glob_term.rIota = $mlexpr_of_bool bi$;
-  Glob_term.rZeta = $mlexpr_of_bool bz$;
-  Glob_term.rDelta = $mlexpr_of_bool bd$;
-  Glob_term.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
+  Genredexpr.rBeta = $mlexpr_of_bool bb$;
+  Genredexpr.rIota = $mlexpr_of_bool bi$;
+  Genredexpr.rZeta = $mlexpr_of_bool bz$;
+  Genredexpr.rDelta = $mlexpr_of_bool bd$;
+  Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
 } >>
 
 let mlexpr_of_explicitation = function
@@ -162,25 +162,25 @@ let mlexpr_of_occ_constr =
   mlexpr_of_occurrences mlexpr_of_constr
 
 let mlexpr_of_red_expr = function
-  | Glob_term.Red b -> <:expr< Glob_term.Red $mlexpr_of_bool b$ >>
-  | Glob_term.Hnf -> <:expr< Glob_term.Hnf >>
-  | Glob_term.Simpl o -> <:expr< Glob_term.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
-  | Glob_term.Cbv f ->
-      <:expr< Glob_term.Cbv $mlexpr_of_red_flags f$ >>
-  | Glob_term.Lazy f ->
-      <:expr< Glob_term.Lazy $mlexpr_of_red_flags f$ >>
-  | Glob_term.Unfold l ->
+  | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
+  | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
+  | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+  | Genredexpr.Cbv f ->
+      <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
+  | Genredexpr.Lazy f ->
+      <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >>
+  | Genredexpr.Unfold l ->
       let f1 = mlexpr_of_by_notation mlexpr_of_reference in
       let f = mlexpr_of_list (mlexpr_of_occurrences f1) in
-      <:expr< Glob_term.Unfold $f l$ >>
-  | Glob_term.Fold l ->
-      <:expr< Glob_term.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Glob_term.Pattern l ->
+      <:expr< Genredexpr.Unfold $f l$ >>
+  | Genredexpr.Fold l ->
+      <:expr< Genredexpr.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
+  | Genredexpr.Pattern l ->
       let f = mlexpr_of_list mlexpr_of_occ_constr in
-      <:expr< Glob_term.Pattern $f l$ >>
-  | Glob_term.CbvVm o -> <:expr< Glob_term.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
-  | Glob_term.ExtraRedExpr s ->
-      <:expr< Glob_term.ExtraRedExpr $mlexpr_of_string s$ >>
+      <:expr< Genredexpr.Pattern $f l$ >>
+  | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+  | Genredexpr.ExtraRedExpr s ->
+      <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
   | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >>
@@ -210,15 +210,15 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
 
 let rec mlexpr_of_may_eval f = function
-  | Glob_term.ConstrEval (r,c) ->
-      <:expr< Glob_term.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
-  | Glob_term.ConstrContext ((loc,id),c) ->
+  | Genredexpr.ConstrEval (r,c) ->
+      <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
+  | Genredexpr.ConstrContext ((loc,id),c) ->
       let id = mlexpr_of_ident id in
-      <:expr< Glob_term.ConstrContext (loc,$id$) $f c$ >>
-  | Glob_term.ConstrTypeOf c ->
-      <:expr< Glob_term.ConstrTypeOf $mlexpr_of_constr c$ >>
-  | Glob_term.ConstrTerm c ->
-      <:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >>
+      <:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >>
+  | Genredexpr.ConstrTypeOf c ->
+      <:expr< Genredexpr.ConstrTypeOf $mlexpr_of_constr c$ >>
+  | Genredexpr.ConstrTerm c ->
+      <:expr< Genredexpr.ConstrTerm $mlexpr_of_constr c$ >>
 
 let mlexpr_of_binding_kind = function
   | Misctypes.ExplicitBindings l ->
@@ -236,10 +236,10 @@ let mlexpr_of_constr_with_binding =
   mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
 
 let mlexpr_of_move_location f = function
-  | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >>
-  | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >>
-  | Tacexpr.MoveFirst -> <:expr< Tacexpr.MoveFirst >>
-  | Tacexpr.MoveLast -> <:expr< Tacexpr.MoveLast >>
+  | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >>
+  | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >>
+  | Misctypes.MoveFirst -> <:expr< Misctypes.MoveFirst >>
+  | Misctypes.MoveLast -> <:expr< Misctypes.MoveLast >>
 
 let mlexpr_of_induction_arg = function
   | Tacexpr.ElimOnConstr c ->
@@ -487,7 +487,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
 and mlexpr_of_tactic_arg = function
   | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id
   | Tacexpr.MetaIdArg (loc,false,id) ->
-      <:expr< Tacexpr.ConstrMayEval (Glob_term.ConstrTerm $anti loc id$) >>
+      <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
   | Tacexpr.TacCall (loc,t,tl) ->
       <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
   | Tacexpr.Tacexp t ->
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 334dcd7e0..58d809bdb 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -176,7 +176,7 @@ module Btauto = struct
   let print_counterexample p env gl =
     let var = lapp witness [|p|] in
     (* Compute an assignment that dissatisfies the goal *)
-    let var = Tacmach.pf_reduction_of_red_expr gl (Glob_term.CbvVm None) var in
+    let var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
     let rec to_list l = match decomp_term l with
     | Term.App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 956a561aa..820da1c3c 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -19,6 +19,7 @@ open Decl_expr
 open Decl_mode
 open Decl_interp
 open Glob_term
+open Glob_ops
 open Names
 open Nameops
 open Declarations
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5bf772fc5..a3bb2eee9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -397,9 +397,9 @@ let isLetIn t =
 
 let h_reduce_with_zeta =
   h_reduce
-    (Glob_term.Cbv
-       {Glob_term.all_flags
-	with Glob_term.rDelta = false;
+    (Genredexpr.Cbv
+       {Redops.all_flags
+	with Genredexpr.rDelta = false;
        })
 
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f18309d04..ccf2caaf5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -3,6 +3,7 @@ open Pp
 open Names
 open Term
 open Glob_term
+open Glob_ops
 open Libnames
 open Indfun_common
 open Errors
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 96bde6f1b..1c2509f6e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -104,9 +104,9 @@ let functional_induction with_clean c princl pat =
 	    (Tacmach.pf_ids_of_hyps g)
 	in
 	let flag =
-	  Glob_term.Cbv
-	    {Glob_term.all_flags
-	     with Glob_term.rDelta = false;
+	  Genredexpr.Cbv
+	    {Redops.all_flags
+	     with Genredexpr.rDelta = false;
 	    }
 	in
 	Tacticals.tclTHEN
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 667be89d0..4d072eca5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -415,10 +415,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    (* observe_tac "unfolding" pre_tac; *)
 	    (* $zeta$ normalizing of the conclusion *)
 	    h_reduce
-	      (Glob_term.Cbv
-		 { Glob_term.all_flags with
-		     Glob_term.rDelta = false ;
-		     Glob_term.rConst = []
+	      (Genredexpr.Cbv
+		 { Redops.all_flags with
+		     Genredexpr.rDelta = false ;
+		     Genredexpr.rConst = []
 		 }
 	      )
 	      Locusops.onConcl;
@@ -804,9 +804,9 @@ and intros_with_rewrite_aux : tactic =
 		  | LetIn _ ->
 		      tclTHENSEQ[
 			h_reduce
-			  (Glob_term.Cbv
-			     {Glob_term.all_flags
-			      with Glob_term.rDelta = false;
+			  (Genredexpr.Cbv
+			     {Redops.all_flags
+			      with Genredexpr.rDelta = false;
 			     })
 			  Locusops.onConcl
 			;
@@ -819,9 +819,9 @@ and intros_with_rewrite_aux : tactic =
 	  | LetIn _ ->
 	      tclTHENSEQ[
 		h_reduce
-		  (Glob_term.Cbv
-		     {Glob_term.all_flags
-		      with Glob_term.rDelta = false;
+		  (Genredexpr.Cbv
+		     {Redops.all_flags
+		      with Genredexpr.rDelta = false;
 		     })
 		  Locusops.onConcl
 		;
@@ -958,9 +958,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  Equality.rewriteLR (mkConst eq_lemma);
 	  (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *)
 	  h_reduce
-	    (Glob_term.Cbv
-	       {Glob_term.all_flags
-		with Glob_term.rDelta = false;
+	    (Genredexpr.Cbv
+	       {Redops.all_flags
+		with Genredexpr.rDelta = false;
 	       })
 	    Locusops.onConcl
 	  ;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d11909043..0b61c5f85 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -39,12 +39,13 @@ open Pretyping
 open Safe_typing
 open Constrintern
 open Hiddentac
+open Misctypes
+open Genredexpr
 
 open Equality
 open Auto
 open Eauto
 
-open Misctypes
 open Indfun_common
 
 
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 30cd5c18b..24a383250 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -27,7 +27,6 @@ let cprop =
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
- let module R = Glob_term in
  let module C = Closure in
  let module CR = C.RedFlags in
  (*** CProp is made Opaque ***)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7019495af..4b7f9187f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -23,6 +23,7 @@ open Reductionops
 open Typeops
 open Type_errors
 open Glob_term
+open Glob_ops
 open Retyping
 open Pretype_errors
 open Evarutil
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 832d32086..c1e0d123d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -18,6 +18,7 @@ open Inductiveops
 open Environ
 open Sign
 open Glob_term
+open Glob_ops
 open Nameops
 open Termops
 open Namegen
diff --git a/pretyping/glob_term.ml b/pretyping/glob_ops.ml
index 466e73b8e..7a48ee9de 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_ops.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i*)
 open Errors
 open Pp
 open Util
@@ -18,58 +17,14 @@ open Nametab
 open Decl_kinds
 open Misctypes
 open Locus
-(*i*)
+open Glob_term
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
-(* locs here refers to the ident's location, not whole pat *)
-(* the last argument of PatCstr is a possible alias ident for the pattern *)
-type cases_pattern =
-  | PatVar of loc * name
-  | PatCstr of loc * constructor * cases_pattern list * name
-
 let cases_pattern_loc = function
     PatVar(loc,_) -> loc
   | PatCstr(loc,_,_,_) -> loc
 
-type glob_constr =
-  | GRef of (loc * global_reference)
-  | GVar of (loc * identifier)
-  | GEvar of loc * existential_key * glob_constr list option
-  | GPatVar of loc * (bool * patvar) (* Used for patterns only *)
-  | GApp of loc * glob_constr * glob_constr list
-  | GLambda of loc * name * binding_kind * glob_constr * glob_constr
-  | GProd of loc * name * binding_kind * glob_constr * glob_constr
-  | GLetIn of loc * name * glob_constr * glob_constr
-  | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
-  | GLetTuple of loc * name list * (name * glob_constr option) *
-      glob_constr * glob_constr
-  | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
-  | GRec of loc * fix_kind * identifier array * glob_decl list array *
-      glob_constr array * glob_constr array
-  | GSort of loc * glob_sort
-  | GHole of (loc * Evar_kinds.t)
-  | GCast of loc * glob_constr * glob_constr cast_type
-
-and glob_decl = name * binding_kind * glob_constr option * glob_constr
-
-and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option
-
-and fix_kind =
-  | GFix of ((int option * fix_recursion_order) array * int)
-  | GCoFix of int
-
-and predicate_pattern =
-    name * (loc * inductive * name list) option
-
-and tomatch_tuple = (glob_constr * predicate_pattern)
-
-and tomatch_tuples = tomatch_tuple list
-
-and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
-
-and cases_clauses = cases_clause list
-
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
@@ -80,37 +35,37 @@ let mkGApp loc p t =
   | GApp (loc,f,l) -> GApp (loc,f,l@[t])
   | _ -> GApp (loc,p,[t])
 
-let map_glob_decl_left_to_right f (na,k,obd,ty) = 
+let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp1 = Option.map f obd in
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
 let map_glob_constr_left_to_right f = function
-  | GApp (loc,g,args) -> 
-      let comp1 = f g in 
-      let comp2 = Util.list_map_left f args in 
+  | GApp (loc,g,args) ->
+      let comp1 = f g in
+      let comp2 = Util.list_map_left f args in
       GApp (loc,comp1,comp2)
-  | GLambda (loc,na,bk,ty,c) -> 
-      let comp1 = f ty in 
-      let comp2 = f c in 
+  | GLambda (loc,na,bk,ty,c) ->
+      let comp1 = f ty in
+      let comp2 = f c in
       GLambda (loc,na,bk,comp1,comp2)
-  | GProd (loc,na,bk,ty,c) -> 
-      let comp1 = f ty in 
-      let comp2 = f c in 
+  | GProd (loc,na,bk,ty,c) ->
+      let comp1 = f ty in
+      let comp2 = f c in
       GProd (loc,na,bk,comp1,comp2)
-  | GLetIn (loc,na,b,c) -> 
-      let comp1 = f b in 
-      let comp2 = f c in 
+  | GLetIn (loc,na,b,c) ->
+      let comp1 = f b in
+      let comp2 = f c in
       GLetIn (loc,na,comp1,comp2)
   | GCases (loc,sty,rtntypopt,tml,pl) ->
-      let comp1 = Option.map f rtntypopt in 
+      let comp1 = Option.map f rtntypopt in
       let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
       let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
       GCases (loc,sty,comp1,comp2,comp3)
   | GLetTuple (loc,nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
       let comp2 = f b in
-      let comp3 = f c in 
+      let comp3 = f c in
       GLetTuple (loc,nal,(na,comp1),comp2,comp3)
   | GIf (loc,c,(na,po),b1,b2) ->
       let comp1 = Option.map f po in
@@ -122,7 +77,7 @@ let map_glob_constr_left_to_right f = function
       let comp2 = Array.map f tyl in
       let comp3 = Array.map f bv in
       GRec (loc,fk,idl,comp1,comp2,comp3)
-  | GCast (loc,c,k) -> 
+  | GCast (loc,c,k) ->
       let comp1 = f c in
       let comp2 = Miscops.map_cast_type f k in
       GCast (loc,comp1,comp2)
@@ -130,43 +85,6 @@ let map_glob_constr_left_to_right f = function
 
 let map_glob_constr = map_glob_constr_left_to_right
 
-(*
-let name_app f e = function
-  | Name id -> let (id, e) = f id e in (Name id, e)
-  | Anonymous -> Anonymous, e
-
-let fold_ident g idl e =
-  let (idl,e) =
-    Array.fold_right
-      (fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e)
-  in (Array.of_list idl,e)
-
-let map_glob_constr_with_binders_loc loc g f e = function
-  | GVar (_,id) -> GVar (loc,id)
-  | GApp (_,a,args) -> GApp (loc,f e a, List.map (f e) args)
-  | GLambda (_,na,ty,c) ->
-      let na,e = name_app g e na in GLambda (loc,na,f e ty,f e c)
-  | GProd (_,na,ty,c) ->
-      let na,e = name_app g e na in GProd (loc,na,f e ty,f e c)
-  | GLetIn (_,na,b,c) ->
-      let na,e = name_app g e na in GLetIn (loc,na,f e b,f e c)
-  | GCases (_,tyopt,tml,pl) ->
-      (* We don't modify pattern variable since we don't traverse patterns *)
-      let g' id e = snd (g id e) in
-      let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
-      GCases
-	(loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl)
-  | GRec (_,fk,idl,tyl,bv) ->
-      let idl',e' = fold_ident g idl e in
-      GRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
-  | GCast (_,c,t) -> GCast (loc,f e c,f e t)
-  | GSort (_,x) -> GSort (loc,x)
-  | GHole (_,x)  -> GHole (loc,x)
-  | GRef (_,x) -> GRef (loc,x)
-  | GEvar (_,x,l) -> GEvar (loc,x,l)
-  | GPatVar (_,x) -> GPatVar (loc,x)
-*)
-
 let fold_glob_constr f acc =
   let rec fold acc = function
   | GVar _ -> acc
@@ -347,35 +265,3 @@ let glob_constr_of_closed_cases_pattern = function
       na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
   | _ ->
       raise Not_found
-
-(**********************************************************************)
-(* Reduction expressions                                              *)
-
-type 'a glob_red_flag = {
-  rBeta : bool;
-  rIota : bool;
-  rZeta : bool;
-  rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
-  rConst : 'a list
-}
-
-let all_flags =
-  {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
-
-type ('a,'b,'c) red_expr_gen =
-  | Red of bool
-  | Hnf
-  | Simpl of 'c with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
-  | Unfold of 'b with_occurrences list
-  | Fold of 'a list
-  | Pattern of 'a with_occurrences list
-  | ExtraRedExpr of string
-  | CbvVm of 'c with_occurrences option
-
-type ('a,'b,'c) may_eval =
-  | ConstrTerm of 'a
-  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (loc * identifier) * 'a
-  | ConstrTypeOf of 'a
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
new file mode 100644
index 000000000..19d003a92
--- /dev/null
+++ b/pretyping/glob_ops.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  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 Errors
+open Pp
+open Util
+open Names
+open Sign
+open Term
+open Libnames
+open Nametab
+open Decl_kinds
+open Misctypes
+open Locus
+open Glob_term
+
+(** Operations on [glob_constr] *)
+
+val cases_pattern_loc : cases_pattern -> loc
+
+val cases_predicate_names : tomatch_tuples -> name list
+
+(** Apply one argument to a glob_constr *)
+val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr
+
+val map_glob_constr :
+  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
+
+(** Ensure traversal from left to right *)
+val map_glob_constr_left_to_right :
+  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
+
+val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
+val occur_glob_constr : identifier -> glob_constr -> bool
+val free_glob_vars : glob_constr -> identifier list
+val loc_of_glob_constr : glob_constr -> loc
+
+(** Conversion from glob_constr to cases pattern, if possible
+
+    Take the current alias as parameter,
+    @raise Not_found if translation is impossible *)
+val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
+
+val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 2528d57f3..0f659f1b6 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -10,6 +10,8 @@ open Misctypes
 open Pp
 open Nameops
 
+(** Mapping [cast_type] *)
+
 let map_cast_type f = function
   | CastConv a -> CastConv (f a)
   | CastVM a -> CastVM (f a)
@@ -41,3 +43,11 @@ and pr_or_and_intro_pattern = function
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
+
+(** Printing of [move_location] *)
+
+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/pretyping/miscops.mli b/pretyping/miscops.mli
index b8f6f6860..123d307de 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -8,11 +8,17 @@
 
 open Misctypes
 
-val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+(** Mapping [cast_type] *)
 
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
 val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
 
 (** Printing of [intro_pattern] *)
 
 val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds
 val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
+
+(** Printing of [move_location] *)
+
+val pr_move_location :
+  ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index ef81aa4d3..08e5ac75c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -13,6 +13,7 @@ open Libnames
 open Nameops
 open Term
 open Glob_term
+open Glob_ops
 open Environ
 open Nametab
 open Pp
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 82f030ae0..b241336e7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,6 +42,7 @@ open Recordops
 open Evarutil
 open Pretype_errors
 open Glob_term
+open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index e520602db..fca2d714f 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -15,7 +15,8 @@ Evarconv
 Arguments_renaming
 Typing
 Miscops
-Glob_term
+Glob_ops
+Redops
 Pattern
 Matching
 Tacred
diff --git a/proofs/tacops.ml b/pretyping/redops.ml
index 05c4e6093..53ac6e6c8 100644
--- a/proofs/tacops.ml
+++ b/pretyping/redops.ml
@@ -6,21 +6,9 @@
 (*         *       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
+open Genredexpr
 
-let make_red_flag =
+let make_red_flag l =
   let rec add_flag red = function
     | [] -> red
     | FBeta :: lf -> add_flag { red with rBeta = true } lf
@@ -28,24 +16,21 @@ let make_red_flag =
     | FZeta :: lf -> add_flag { red with rZeta = true } lf
     | FConst l :: lf ->
 	if red.rDelta then
-	  error
+	  Errors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag { red with rConst = list_union red.rConst l } lf
+        add_flag { red with rConst = Util.list_union red.rConst l } lf
     | FDeltaBut l :: lf ->
 	if red.rConst <> [] & not red.rDelta then
-	  error
+	  Errors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
         add_flag
-	  { red with rConst = list_union red.rConst l; rDelta = true }
+	  { red with rConst = Util.list_union red.rConst l; rDelta = true }
 	  lf
   in
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
+    l
 
-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"
+let all_flags =
+  {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
diff --git a/proofs/tacops.mli b/pretyping/redops.mli
index be17e035a..b55597098 100644
--- a/proofs/tacops.mli
+++ b/pretyping/redops.mli
@@ -6,9 +6,8 @@
 (*         *       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
+open Genredexpr
 
-val pr_move_location :
-  ('a -> Pp.std_ppcmds) -> 'a Tacexpr.move_location -> Pp.std_ppcmds
+val make_red_flag : 'a red_atom list -> 'a glob_red_flag
+
+val all_flags : 'a glob_red_flag
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/tactics/auto.ml b/tactics/auto.ml
index 6e338c4cb..f167a91a3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -26,7 +26,7 @@ open Matching
 open Tacmach
 open Proof_type
 open Pfedit
-open Glob_term
+open Genredexpr
 open Evar_refiner
 open Tacred
 open Tactics
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 8b773762f..e9602762d 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -26,7 +26,7 @@ open Tactics
 open Pattern
 open Clenv
 open Auto
-open Glob_term
+open Genredexpr
 open Hiddentac
 open Tacexpr
 open Misctypes
diff --git a/tactics/elim.ml b/tactics/elim.ml
index bd304d975..de5512843 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -25,6 +25,7 @@ open Tactics
 open Hiddentac
 open Genarg
 open Tacexpr
+open Misctypes
 
 let introElimAssumsThen tac ba =
   let nassums =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a2d1caf5f..a74bdad29 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -16,6 +16,7 @@ open Mod_subst
 open Names
 open Tacexpr
 open Glob_term
+open Glob_ops
 open Tactics
 open Errors
 open Util
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f3b6c58c0..8e68d8e70 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -15,7 +15,9 @@ open Libobject
 open Pattern
 open Matching
 open Pp
+open Genredexpr
 open Glob_term
+open Glob_ops
 open Sign
 open Tacred
 open Errors
@@ -172,7 +174,7 @@ let _ =
       [ "red", TacReduce(Red false,nocl);
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl None,nocl);
-        "compute", TacReduce(Cbv all_flags,nocl);
+        "compute", TacReduce(Cbv Redops.all_flags,nocl);
         "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
         "assumption", TacAssumption;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 897e1d7ef..ab4b08e7d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -25,7 +25,7 @@ open Libnames
 open Evd
 open Pfedit
 open Tacred
-open Glob_term
+open Genredexpr
 open Tacmach
 open Proof_type
 open Logic