From e72024e2292a50684b7f280d6efb8fee090e2dbf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 Sep 2000 20:37:37 +0000
Subject: Suppression de Abst

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/instantiate.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/instantiate.ml')

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 627f0d45c1..9b1d9289a5 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -72,7 +72,7 @@ let existential_value sigma (n,args) =
     | Evar_empty ->
 	anomaly "a defined existential with no body"
 
-let const_abst_opt_value env sigma c =
+let const_evar_opt_value env sigma c =
   match c with
     | DOPN(Const sp,_) ->
 	if evaluable_constant env c then Some (constant_value env c) else None
@@ -81,7 +81,5 @@ let const_abst_opt_value env sigma c =
 	  Some (existential_value sigma (ev,args)) 
 	else 
 	  None
-    | DOPN(Abst sp,_) ->
-	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
 
-- 
cgit v1.2.3