Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars

Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 4 insertions, 4 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index ac6870a39e..0923ab6f4b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -310,15 +310,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
 
 let pr_evar_list env sigma l =
   let open Evd in
-  let pr_restrict ev =
-    match is_restricted_evar sigma ev with
+  let pr_alias ev =
+    match is_aliased_evar sigma ev with
     | None -> mt ()
-    | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")"
+    | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")"
   in
   let pr (ev, evi) =
     h 0 (Evar.print ev ++
       str "==" ++ pr_evar_info env sigma evi ++
-      pr_restrict ev ++
+      pr_alias ev ++
       (if evi.evar_body == Evar_empty
        then str " {" ++ pr_existential_key sigma ev ++ str "}"
        else mt ()))