Merge branch 'v8.6'

2 files changed, 8 insertions, 7 deletions

diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index 5f2617e44d..80cafb3abd 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -669,7 +669,7 @@ module Make
       let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
       let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
 
-      let pr_constrarg c = spc () ++ pr.pr_constr c in
+      let _pr_constrarg c = spc () ++ pr.pr_constr c in
       let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
       let pr_intarg n = spc () ++ int n in
 
@@ -717,7 +717,7 @@ module Make
                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
                   pr_lconstrarg ty ++ str")") in
       (*  spc() ++
-          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
           c)
       *)
       let pr_cofix_tac (id,c) =
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index 2af872daf6..df38a42cb9 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