summaryrefslogtreecommitdiff
path: root/AAC.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-09-20 09:41:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-09-20 09:41:14 +0200
commit8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e (patch)
treeddabcfad1c52bf730690b1be7c900f25dcdf0ec3 /AAC.v
parent9216cffaaa1ef137ef5bdb5b290a930cc6198850 (diff)
Imported Upstream version 0.3upstream/0.3
Diffstat (limited to 'AAC.v')
-rw-r--r--AAC.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/AAC.v b/AAC.v
index 0f5e85d..a16f1a0 100644
--- a/AAC.v
+++ b/AAC.v
@@ -82,7 +82,7 @@ Proof.
Qed.
Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E}
- {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4.
+ {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4 := {}.
@@ -1132,4 +1132,4 @@ Section t.
End t.
-Declare ML Module "aac_tactics".
+Declare ML Module "aac".