test-suite/bugs/opened/bug_4771.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

Module Type Foo.

Parameter Inline t : nat.

End Foo.

Module F(X : Foo).

Tactic Notation "foo" ref(x) := idtac.

Ltac g := foo X.t.

End F.

Module N.
Definition t := 0 + 0.
End N.

Module K := F(N).

(* Was
Anomaly: Uncaught exception Not_found. Please report. *)