From 723c344d3e4cf7fdc2e4854ea7d55d140570424d Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Nov 2000 16:43:51 +0000
Subject: nouveau discharge fait par le noyau; plus de recettes dans les corps
 des constantes

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

(limited to 'kernel/instantiate.ml')

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index f99ccb0c47..7f6f1258b5 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -41,15 +41,12 @@ exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (sp,args) =
   let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque) else
-  if not (is_defined cb) then raise (NotEvaluableConst NoBody) else
+  if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
-    | Some v -> 
-	let body = cook_constant v in
+    | Some body -> 
         instantiate_constr cb.const_hyps body (Array.to_list args)
     | None ->
-	anomalylabstrm "termenv__constant_value"
-	  [< 'sTR "a defined constant with no body." >]
+	raise (NotEvaluableConst NoBody)
 
 let constant_opt_value env cst =
   try Some (constant_value env cst)
-- 
cgit v1.2.3