evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait

boucler la condition de garde


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2454 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 21 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0d341aabc4..7e638f5175 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -207,18 +207,33 @@ let keep_hyps env needed =
 
 
 (* Constants *)
+
+(* Not taking opacity into account *)
 let defined_constant env sp =
   match (lookup_constant sp env).const_body with
       Some _ -> true
     | None -> false
-      
-let opaque_constant env sp = (lookup_constant sp env).const_opaque
+
+(* Taking opacity into account *)
+type const_evaluation_result = NoBody | Opaque
+
+exception NotEvaluableConst of const_evaluation_result
+
+let constant_value env sp =
+  let cb = lookup_constant sp env in
+  if cb.const_opaque then raise (NotEvaluableConst Opaque);
+  match cb.const_body with
+    | Some body -> body
+    | None -> raise (NotEvaluableConst NoBody)
+
+let constant_opt_value env cst =
+  try Some (constant_value env cst)
+  with NotEvaluableConst _ -> None
 
 (* A global const is evaluable if it is defined and not opaque *)
-let evaluable_constant env sp =
-  try defined_constant env sp
-  with Not_found -> 
-    false
+let evaluable_constant env cst =
+  try let _  = constant_value env cst in true
+  with NotEvaluableConst _ -> false
 
 (* A local const is evaluable if it is defined and not opaque *)
 let evaluable_named_decl env id =
@@ -242,21 +257,6 @@ let constant_type env sp =
   let cb = lookup_constant sp env in
   cb.const_type  
 
-type const_evaluation_result = NoBody | Opaque
-
-exception NotEvaluableConst of const_evaluation_result
-
-let constant_value env sp =
-  let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque);
-  match cb.const_body with
-    | Some body -> body
-    | None -> raise (NotEvaluableConst NoBody)
-
-let constant_opt_value env cst =
-  try Some (constant_value env cst)
-  with NotEvaluableConst _ -> None
-
 (*s Modules (i.e. compiled environments). *)
 
 type compiled_env = {