Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable_constant qui change de type au passage

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

4 files changed, 29 insertions, 10 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 87d9e306fe..29078174e0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -305,14 +305,27 @@ let make_all_name_different env =
     env
 
 (* Constants *)
-let defined_constant env (sp,_) = is_defined (lookup_constant sp env)
+let defined_constant env sp = is_defined (lookup_constant sp env)
 
-let opaque_constant env (sp,_) = is_opaque (lookup_constant sp env)
+let opaque_constant env sp = is_opaque (lookup_constant sp env)
 
-(* A const is evaluable if it is defined and not opaque *)
-let evaluable_constant env k =
+(* A global const is evaluable if it is defined and not opaque *)
+let evaluable_constant env sp =
   try 
-    defined_constant env k && not (opaque_constant env k)
+    defined_constant env sp && not (opaque_constant env sp)
+  with Not_found -> 
+    false
+
+(* A local const is evaluable if it is defined and not opaque *)
+let evaluable_named_decl env id =
+  try 
+    lookup_named_value id env <> None
+  with Not_found -> 
+    false
+
+let evaluable_rel_decl env n =
+  try 
+    lookup_rel_value n env <> None
   with Not_found -> 
     false
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c0a0dcc9a7..14209cd723 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -145,8 +145,11 @@ val it_mkNamedProd_or_LetIn : constr -> named_context -> constr
 val lambda_create : env -> types * constr -> constr
 val prod_create : env -> types * constr -> constr
 
-val defined_constant : env -> constant -> bool
-val evaluable_constant : env -> constant -> bool
+val defined_constant : env -> constant_path -> bool
+val evaluable_constant : env -> constant_path -> bool
+
+val evaluable_named_decl : env -> identifier -> bool
+val evaluable_rel_decl : env -> int -> bool
 
 (*s Opaque / Transparent switching *)
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 4cd1641b1e..fa27696878 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -150,8 +150,11 @@ let glob_const_nvar loc id =
   let qid = make_qualid [] (string_of_id id) in
   try
     match Nametab.locate qid with
-      | ConstRef sp -> sp
-      | _ -> error ((string_of_qualid qid) ^ " does not denote a constant")
+      | ConstRef sp when Environ.evaluable_constant (Global.env ()) sp -> sp
+      | VarRef sp when
+	  Environ.evaluable_named_decl (Global.env ()) (basename sp) -> sp
+      | _ -> error ((string_of_qualid qid) ^
+		    " does not denote an evaluable constant")
   with
     | Not_found ->
 	Pretype_errors.error_global_not_found_loc loc qid
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 575b189306..481a3a616e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -184,7 +184,7 @@ let w_ORELSE        = w_ORELSE
 let w_add_sign      = w_add_sign
 let ctxt_type_of    = ctxt_type_of
 
-let w_defined_const wc k     = defined_constant (w_env wc) k
+let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp
 let w_defined_evar wc k      = Evd.is_defined (w_Underlying wc) k
 let w_const_value wc         = constant_value (w_env wc)
 let w_conv_x wc m n          = is_conv (w_env wc) (w_Underlying wc) m n