diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-26 09:54:32 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-26 09:54:32 +0100 |
commit | 4c81d739be2a2e409c7e76bac3e616c4415a1efd (patch) | |
tree | 7b1a9ac77ef06a5de4da4eb108b6f781c465a5d4 | |
parent | 2ebf8bfda476966209d681470ebe6301fb10db0a (diff) | |
parent | c58e3bdadde3ab60c982bdd036964987add72bee (diff) | |
download | compcert-4c81d739be2a2e409c7e76bac3e616c4415a1efd.tar.gz compcert-4c81d739be2a2e409c7e76bac3e616c4415a1efd.zip |
Merge branch 'master' into dwarf
-rw-r--r-- | lib/Maps.v | 13 |
1 files changed, 4 insertions, 9 deletions
@@ -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: |