From a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 29 May 2012 11:08:44 +0000
Subject: 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
---
 plugins/btauto/refl_btauto.ml                  |  2 +-
 plugins/decl_mode/decl_proof_instr.ml          |  1 +
 plugins/funind/functional_principles_proofs.ml |  6 +++---
 plugins/funind/glob_term_to_relation.ml        |  1 +
 plugins/funind/indfun.ml                       |  6 +++---
 plugins/funind/invfun.ml                       | 26 +++++++++++++-------------
 plugins/funind/recdef.ml                       |  3 ++-
 plugins/xml/doubleTypeInference.ml             |  1 -
 8 files changed, 24 insertions(+), 22 deletions(-)

(limited to 'plugins')

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 ***)
-- 
cgit v1.2.3