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".