diff options
| -rwxr-xr-x | configure | 4 | ||||
| -rw-r--r-- | lib/Maps.v | 13 |
2 files changed, 6 insertions, 11 deletions
@@ -64,9 +64,9 @@ while : ; do -toolprefix|--toolprefix) toolprefix="$2"; shift;; -no-runtime-lib) - has_runtime_lib=false; shift;; + has_runtime_lib=false;; -no-checklink) - build_checklink=false; shift;; + build_checklink=false;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -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: |