From 78384438637eb9ce2f11f61bafc59f17c5f933da Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Feb 2001 10:02:40 +0000
Subject: Retrait de EvarRef de global_reference; nettoyage autour de
 ast_of_ref

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

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 287cff5981..0c51f085ef 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -219,8 +219,6 @@ let sp_of_global env = function
       let mip = mind_nth_type_packet mib tyi in
       assert (i <= Array.length mip.mind_consnames && i > 0);
       make_path (dirpath sp) mip.mind_consnames.(i-1) CCI
-  | EvarRef n -> 
-      make_path [] (id_of_string ("?"^(string_of_int n))) CCI
 
 let id_of_global env ref = basename (sp_of_global env ref)
 
diff --git a/kernel/term.ml b/kernel/term.ml
index ee98a70549..7503aa03a6 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -44,7 +44,6 @@ type global_reference =
   | ConstRef of constant_path
   | IndRef of inductive_path
   | ConstructRef of constructor_path
-  | EvarRef of int
 
 (********************************************************************)
 (*       Constructions as implemented                               *)
diff --git a/kernel/term.mli b/kernel/term.mli
index e3f6b44635..08b1e5e863 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -39,7 +39,6 @@ type global_reference =
   | ConstRef of constant_path
   | IndRef of inductive_path
   | ConstructRef of constructor_path
-  | EvarRef of int
 
 (********************************************************************)
 (* The type of constructions *)
@@ -79,7 +78,7 @@ type arity = rel_declaration list * sorts
 
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type existential = int * constr array
+type existential = existential_key * constr array
 type constant = constant_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
@@ -314,8 +313,8 @@ val path_of_const : constr -> constant_path
 val args_of_const : constr -> constr array
 
 (* Destructs an existential variable *)
-val destEvar : constr -> int * constr array
-val num_of_evar : constr -> int
+val destEvar : constr -> existential_key * constr array
+val num_of_evar : constr -> existential_key
 
 (* Destructs a (co)inductive type *)
 val destMutInd : constr -> inductive
-- 
cgit v1.2.3