blob: 825a26e167308560d1c18ea5568f9d95f94b593f (
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
|
Module X.
Set Universe Polymorphism.
Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
Axioms A B : Type.
Axiom P : A = B.
Definition foo : A = B.
Fail abstract (rewrite <- P; reflexivity).
(* Error: internal_paths_rew already exists. *)
Admitted.
Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
End X.
Module Y.
Set Universe Polymorphism.
Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
Axioms A B : Type.
Axiom P : A = B.
Definition foo : (A = B) * (A = B).
Fail split; abstract (rewrite <- P; reflexivity).
(* Error: internal_paths_rew already exists. *)
Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
Fail End Y.
|
