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

11 files changed, 54 insertions, 49 deletions

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 ->