diff options
Diffstat (limited to 'proofs/tacinterp.ml')
| -rw-r--r-- | proofs/tacinterp.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 |