From 1ad33441e62419ff735c09588b3e228c313378e1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 27 Nov 2000 10:27:43 +0000
Subject: 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
---
 kernel/environ.ml  | 23 ++++++++++++++++++-----
 kernel/environ.mli |  7 +++++--
 2 files changed, 23 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 87d9e306f..29078174e 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 c0a0dcc9a..14209cd72 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 *)
 
-- 
cgit v1.2.3