Ltac, move:, and name resolution

[vbgl]

A name, that is bound in a Ltac tactic, fails to be resolved when the tactic is used in a different module. A minimal non-working example follows. The expected behavior is the one of generalize, so it seems a bug related to the move: tactic.

Versions

The Coq Proof Assistant, version 8.7.1 (January 2018)
compiled on Jan 20 2018 9:56:24 with OCaml 4.04.2

The Coq Proof Assistant, version 8.8+alpha (February 2018)
compiled on Feb 2 2018 13:36:42 with OCaml 4.04.2

Operating system

macOS

Description of the problem

a.v

Require Import ssreflect.

Definition truth := I.

Ltac t :=
  move: truth.

Ltac t' :=
  generalize truth.

b.v

Require a.

Goal True.
  Fail a.t.
(* The reference truth was not found in the current environment. *)
  a.t'.
  refine (@id _).
Qed.

[Zimmi48]

@gares It seems like you had started working on this issue. What stopped you?

[gares]

I've opened #8314 with that commit, it needs a rebase I guess.
I think I did not open the PR when I made the commit because the fix is partial, and the full fix is much more involved. But yea, better than nothing.

[eponier]

Actually, it seems that truth is evaluated in the context where the tactic is called.

Require Import ssreflect.

Module Import A.
Definition truth := I.

Ltac t :=
  move: truth.

Ltac t' :=
  generalize truth.
End A.

Definition truth := 2.
Goal True.
  t.
  (* nat -> True *)