Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 7 insertions, 0 deletions

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 215713d9..ab71f5f2 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -176,6 +176,13 @@ let coerce_to_evaluable_ref env v =
     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
+    match r with
+    | VarRef var -> EvalVarRef var
+    | ConstRef c -> EvalConstRef c
+    | IndRef _ | ConstructRef _ -> fail ()
   else
     let ev = match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))