From a2eb60e7b2f91919b3fd4f099c6dba923916395b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 22 Nov 2012 20:28:15 +0100
Subject: [PATCH] Fix inconsistency of map.MapPermut detected by Benedikt
Huber.
This reverts part of commit b45604c2ca016075874b66b2e7fb1cec1d4f59e3.
---
theories/map.why | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/theories/map.why b/theories/map.why
index a92e143918..d38f76ab34 100644
--- a/theories/map.why
+++ b/theories/map.why
@@ -85,7 +85,6 @@ theory MapPermut
use import int.Int
use export Map
- use import MapEq
predicate exchange (a1 a2 : map int 'a) (i j : int) =
a1[i] = a2[j] /\ a2[i] = a1[j] /\
@@ -97,8 +96,7 @@ theory MapPermut
inductive permut_sub (map int 'a) (map int 'a) int int =
| permut_refl :
- forall a1 a2 : map int 'a. forall l u : int.
- map_eq_sub a1 a2 l u -> permut_sub a1 a2 l u
+ forall a : map int 'a. forall l u : int. permut_sub a a l u
| permut_sym :
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
--
GitLab