remove not used hypotheses in TREE

1 files changed, 4 insertions, 9 deletions

diff --git a/lib/Maps.v b/lib/Maps.v
index 2b6badcb..63ac0c09 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -64,13 +64,13 @@ Module Type TREE.
   Hypothesis gsspec:
     forall (A: Type) (i j: elt) (x: A) (m: t A),
     get i (set j x m) = if elt_eq i j then Some x else get i m.
+  (* We could implement the following, but it's not needed for the moment.
   Hypothesis gsident:
     forall (A: Type) (i: elt) (m: t A) (v: A),
     get i m = Some v -> set i v m = m.
-  (* We could implement the following, but it's not needed for the moment.
-    Hypothesis grident:
-      forall (A: Type) (i: elt) (m: t A) (v: A),
-      get i m = None -> remove i m = m.
+  Hypothesis grident:
+    forall (A: Type) (i: elt) (m: t A) (v: A),
+    get i m = None -> remove i m = m.
   *)
   Hypothesis grs:
     forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
@@ -115,11 +115,6 @@ Module Type TREE.
     f None None = None ->
     forall (m1: t A) (m2: t B) (i: elt),
     get i (combine f m1 m2) = f (get i m1) (get i m2).
-  Hypothesis combine_commut:
-    forall (A B: Type) (f g: option A -> option A -> option B),
-    (forall (i j: option A), f i j = g j i) ->
-    forall (m1 m2: t A),
-    combine f m1 m2 = combine g m2 m1.
 
   (** Enumerating the bindings of a tree. *)
   Variable elements: