diff options
Diffstat (limited to 'ltac/taccoerce.ml')
| -rw-r--r-- | ltac/taccoerce.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index 2af872daf..df38a42cb 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -235,13 +235,15 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env v = let fail () = raise (CannotCoerceTo "an evaluable reference") in let v = Value.normalize v in + let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id | _ -> fail () else if has_type v (topwit wit_var) then - let ev = EvalVarRef (out_gen (topwit wit_var) v) in - if Tacred.is_evaluable env ev then ev else fail () + let id = out_gen (topwit wit_var) v in + if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id + else fail () else if has_type v (topwit wit_ref) then let open Globnames in let r = out_gen (topwit wit_ref) v in @@ -250,12 +252,11 @@ let coerce_to_evaluable_ref env v = | ConstRef c -> EvalConstRef c | IndRef _ | ConstructRef _ -> fail () else - let ev = match Value.to_constr v with + match Value.to_constr v with | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) | Some c when isVar c -> EvalVarRef (destVar c) | _ -> fail () - in - if Tacred.is_evaluable env ev then ev else fail () + in if Tacred.is_evaluable env ev then ev else fail () let coerce_to_constr_list env v = let v = Value.to_list v in |