From 002d6cb09f2447134677b438ab09e880a2881151 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 13 Oct 1999 12:36:57 +0000
Subject: plus de recettes pour les corps des constantes

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

(limited to 'kernel/instantiate.ml')

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 679789d6ce..e1f9356df8 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -42,15 +42,14 @@ let constant_value env k =
   let cb = lookup_constant sp env in
   if not cb.const_opaque & defined_constant env k then
     match cb.const_body with
-      Some { contents = Cooked body } -> 
-        instantiate_constr 
-	  (ids_of_sign cb.const_hyps) body (Array.to_list args)
-    | Some { contents = Recipe _ } ->
-        anomalylabstrm "termenv__constant_value"
-          [< 'sTR "a transparent constant which was not cooked" >]
-    | None -> anomalylabstrm "termenv__constant_value"
-          [< 'sTR "a defined constant as no body." >]
-  else failwith "opaque"
+      | Some body -> 
+          instantiate_constr 
+	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
+      | None -> 
+	  anomalylabstrm "termenv__constant_value"
+	    [< 'sTR "a defined constant as no body." >]
+  else 
+    failwith "opaque"
 
 let const_abst_opt_value env c =
   match c with
-- 
cgit v1.2.3