diff options
| -rw-r--r-- | ltac/taccoerce.ml | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5078.v | 5 |
2 files changed, 11 insertions, 5 deletions
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index 46469df6a..b0a80ef73 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -236,13 +236,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 @@ -251,12 +253,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 diff --git a/test-suite/bugs/closed/5078.v b/test-suite/bugs/closed/5078.v new file mode 100644 index 000000000..ca73cbcc1 --- /dev/null +++ b/test-suite/bugs/closed/5078.v @@ -0,0 +1,5 @@ +(* Test coercion from ident to evaluable reference *) +Tactic Notation "unfold_hyp" hyp(H) := cbv delta [H]. +Goal True -> Type. + intro H''. + Fail unfold_hyp H''. |