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

1 files changed, 3 insertions, 6 deletions

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)