From 5fa47f1258408541150e2e4c26d60ff694e7c1bc Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:37 +0000
Subject: locus.mli for occurrences+clauses, misctypes.mli for various little
 things

 Corresponding operations in locusops.ml and miscops.ml

 The type of occurrences is now a clear algebraic one instead of
 a bool*list hard to understand.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/omega/coq_omega.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 1057c646f8..2c82bab7b0 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -34,6 +34,7 @@ open Logic
 open Libnames
 open Nametab
 open Contradiction
+open Misctypes
 
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -129,12 +130,12 @@ let intern_id,unintern_id =
 
 let mk_then = tclTHENLIST
 
-let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c])
+let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
 let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
 
 let rev_assoc k =
   let rec loop = function
-- 
cgit v1.2.3