From a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 Mon Sep 17 00:00:00 2001
From: letouzey
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
---
 tactics/auto.ml          | 2 +-
 tactics/eauto.ml4        | 2 +-
 tactics/elim.ml          | 1 +
 tactics/extratactics.ml4 | 1 +
 tactics/tacinterp.ml     | 4 +++-
 tactics/tactics.ml       | 2 +-
 6 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6e338c4cbb..f167a91a30 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 8b773762f0..e9602762d2 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 bd304d9753..de55128430 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 a2d1caf5f8..a74bdad29b 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 f3b6c58c0e..8e68d8e705 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 897e1d7ef2..ab4b08e7da 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
-- 
cgit v1.2.3