From d1fd4e0344d81127f2307f1553642fc67911b68c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 25 Nov 1999 10:45:26 +0000
Subject: typage des existentielles dans Typing_ev; suppression metamap
 inutiles dans typage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@141 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.ml | 1 -
 kernel/evd.ml     | 2 --
 kernel/evd.mli    | 2 --
 3 files changed, 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f715e985aa..34261e7355 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,7 +43,6 @@ let empty_env = {
 
 let universes env = env.env_universes
 let context env = env.env_context
-let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
 
 (* Construction functions. *)
 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index b31f2f6b79..52e1a936eb 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -65,6 +65,4 @@ let is_defined sigma ev =
   let info = map sigma ev in 
   not (info.evar_body = Evar_empty)
 
-let metamap sigma = failwith "metamap : NOT YET IMPLEMENTED"
-
 let evar_hyps ev = get_globals (context ev.evar_env)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 62378f921e..2e55f578e9 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -48,6 +48,4 @@ val is_evar : 'a evar_map -> evar -> bool
 
 val is_defined : 'a evar_map -> evar -> bool
 
-val metamap : 'a evar_map -> (int * constr) list
-
 val evar_hyps : 'a evar_info -> typed_type signature
-- 
cgit v1.2.3