From 2441ab708c0a880fd9b85c24e277306940aee634 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Wed, 25 Mar 2015 16:47:02 +0100 Subject: remove not used hypotheses in TREE --- lib/Maps.v | 13 ++++--------- 1 file 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: -- cgit