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

5 files changed, 22 insertions, 20 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5bf772fc5a..a3bb2eee96 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 f18309d049..ccf2caaf56 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 96bde6f1ba..1c2509f6e2 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 667be89d09..4d072eca56 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 d11909043f..0b61c5f858 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