From 8e82c4096357355a148705341742702ff285f72a Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 28 Mar 2001 15:11:26 +0000
Subject: amelioration de la structure des univers elimination des compteurs
 globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de
 flags)

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

(limited to 'contrib')

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 71bfbe290a..6c8badb5fa 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -26,6 +26,7 @@ open Environ
 open Sign
 open Inductive
 open Tacmach
+open Evar_refiner
 open Tactics
 open Clenv
 open Logic
@@ -560,7 +561,7 @@ let rec decompile af =
   in
   loop af.body
 
-let mkNewMeta () = mkMeta (Environ.new_meta())
+let mkNewMeta () = mkMeta (Clenv.new_meta())
 
 let clever_rewrite_base_poly typ p result theorem gl = 
   let full = pf_concl gl in
-- 
cgit v1.2.3