diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:27:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:27:43 +0000 |
| commit | 1ad33441e62419ff735c09588b3e228c313378e1 (patch) | |
| tree | bfa3e125b1b6038485bf386a93d27906bb8f4a0a /proofs | |
| parent | c8a6a2b4e9bc7bd03c5022e4dc90de4029a4d7e5 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 7 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 4cd1641b1..fa2769687 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 575b18930..481a3a616 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 |