diff options
Diffstat (limited to 'theories/Numbers/Integer/TreeMod/ZTreeMod.v')
| -rw-r--r-- | theories/Numbers/Integer/TreeMod/ZTreeMod.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v index db09c2ec7a..e885d25bc7 100644 --- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v +++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v @@ -143,7 +143,7 @@ Hypothesis A0 : A 0. Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *) Add Morphism A with signature NZeq ==> iff as A_morph. -Proof A_wd. +Proof. apply A_wd. Qed. Let B (n : Z) := A (Z_to_NZ n). |