diff options
| author | Hugo Herbelin | 2016-09-13 13:42:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-13 13:44:10 +0200 |
| commit | 0e94cb62410354e5df4e65b34e7cbf8451b31d6e (patch) | |
| tree | e50d291966da1ad791458a3ceea6d827857d5852 | |
| parent | 93ae6db3375d442ef67154c832bbdf155cffe32f (diff) | |
Fixing #5078 (wrong detection of evaluable local hypotheses).
| -rw-r--r-- | ltac/taccoerce.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index 0110510d35..46469df6a1 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -241,9 +241,8 @@ let coerce_to_evaluable_ref env v = | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id | _ -> fail () else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id - else fail () + let ev = EvalVarRef (out_gen (topwit wit_var) v) in + if Tacred.is_evaluable env ev then ev else fail () else if has_type v (topwit wit_ref) then let open Globnames in let r = out_gen (topwit wit_ref) v in |