From 36c150fac098e1a038d23b812744e1aaaa5993da Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 25 May 2000 15:00:43 +0000
Subject: Bug existential_value au lieu de existential_type + divers sur
 existential

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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b62e31714f..6c7e1bbe5e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -114,7 +114,8 @@ let type_inst_construct i (IndFamily (mis,globargs)) =
   let tc = mis_type_mconstruct i mis in
   prod_applist tc globargs
 
-let type_of_existential env sigma c = Instantiate.existential_value sigma c
+let type_of_existential env sigma c =
+  Instantiate.existential_type sigma (destEvar c)
 
 (* Case. *)
 
-- 
cgit v1.2.3