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

3 files changed, 25 insertions, 22 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 = {
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8e1d848de4..9a00f053ac 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -102,7 +102,9 @@ val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
 
+(* A constant is defined when it has a body (theorems do) *)
 val defined_constant : env -> constant -> bool
+(* A constant is evaluable when delta reduction applies (theorems don't) *)
 val evaluable_constant : env -> constant -> bool
 
 val evaluable_named_decl : env -> variable -> bool
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 26f4d51c6d..b4a74061f0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -642,7 +642,8 @@ let check_one_fix renv recpos def =
           (try List.for_all (check_rec_call renv) l
            with (FixGuardError _ ) as e ->
              if evaluable_constant renv.env sp then 
-	       check_rec_call renv (whd_betadeltaiota renv.env t)
+	       check_rec_call renv
+                 (applist(constant_value renv.env sp, l))
 	     else raise e)
 
       (* The cases below simply check recursively the condition on the