aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3264.v
blob: 4eb218906f80c234aa548ff0c6b56d2e1e35f3ad (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
Module File1.
  Module Export DirA.
    Module A.
      Inductive paths {A : Type} (a : A) : A -> Type :=
        idpath : paths a a.

      Arguments idpath {A a} , [A] a.

      Notation "x = y :> A" := (@paths A x y) : type_scope.
      Notation "x = y" := (x = y :>_) : type_scope.
    End A.
  End DirA.
End File1.

Module File2.
  Module Export DirA.
    Module B.
      Import File1.
      Export A.
      Lemma foo : forall x y : Type, x = y -> y = x.
      Proof.
        intros x y H.
        rewrite <- H.
        constructor.
      Qed.
    End B.
  End DirA.
End File2.

Module File3.
  Module Export DirA.
    Module C.
      Import File1.
      Export A.
      Lemma bar : forall x y : Type, x = y -> y = x.
      Proof.
        intros x y H.
        rewrite <- H.
        constructor.
      Defined.
      Definition bar'
        := Eval cbv beta iota zeta delta [bar internal_paths_rew] in bar.
    End C.
  End DirA.
End File3.