From 12c096d156c4f33d0601bc53067a5780b898cfd4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Feb 2001 10:07:15 +0000
Subject: Chgt signature de type_of_existential

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1341 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml  | 4 ++--
 kernel/typeops.mli | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 5b6d45b748..ae1bb46cfa 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -94,8 +94,8 @@ let type_of_constructor env sigma cstr =
     (index_of_constructor cstr)
     (inductive_of_constructor cstr)
 
-let type_of_existential env sigma c =
-  Instantiate.existential_type sigma (destEvar c)
+let type_of_existential env sigma ev =
+  Instantiate.existential_type sigma ev
 
 (* Case. *)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6e5cdca3e0..f06e656537 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -34,15 +34,15 @@ val type_of_inductive : env -> 'a evar_map -> inductive -> types
 
 val type_of_constructor : env -> 'a evar_map -> constructor -> types
 
-val type_of_existential : env -> 'a evar_map -> constr -> constr
+val type_of_existential : env -> 'a evar_map -> existential -> types
 
 val type_of_case : env -> 'a evar_map -> case_info
   -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment array -> unsafe_judgment
 
 val type_case_branches :
-  env -> 'a evar_map -> Inductive.inductive_type -> constr -> constr
-    -> constr -> constr array * constr 
+  env -> 'a evar_map -> Inductive.inductive_type -> constr -> types
+    -> constr -> types array * types
 
 val judge_of_prop_contents : contents -> unsafe_judgment
 
-- 
cgit v1.2.3