Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_division

23 files changed, 1903 insertions, 894 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9534282d..c8ccedb8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -302,7 +302,7 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace
     - ./.download_from_Kalray.sh
-    - rm -f download/*dkms*.deb download/*eclipse*.deb download/*llvm*.deb download/*board-mgmt* download/*oce-host* download/*pocl* download/*flash-util* download/*barebox*
+    - (cd download ; rm -f *dkms*.deb *eclipse*.deb *llvm*.deb *board-mgmt* *oce-host* *pocl* *flash-util* *barebox* *-kann-* *-kaf-* *-stb-* *-opencv* *-eigen* *-task* *-blis* *-lz4*)
     - sudo dpkg -i download/*.deb
     - rm -rf download
     - eval `opam config env`
@@ -311,14 +311,13 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil
     - opam repo add coq-released https://coq.inria.fr/opam/released
     - opam install coq-coq2html
   script:
+    - mkdir public
     - source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh
     - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS"
     - make -j "$NJOBS" clightgen
     - source /opt/kalray/accesscore/kalray.sh && make documentation
-    - mkdir public
-    - cp -r doc/* public/
-    - tools/fix_html_date.sh doc/index-kvx.html " (" ")" > public/index.html
-    - rm public/index-kvx.html
+    - cp -rf doc/* public/
+    - mv doc/index-verimag.html public/index.html
   artifacts:
     paths:
     - public
diff --git a/Changelog b/Changelog
index d3a4cc4b..94d85535 100644
--- a/Changelog
+++ b/Changelog
@@ -1,5 +1,62 @@
+Release 3.10, 2021-11-19
+========================
+
+Major improvement:
+- Bit fields in structs and unions are now handled in the
+  formally-verified part of CompCert. (Before, they were being
+  implemented through an unverified source-to-source translation.)
+  The CompCert C and Clight languages provide abstract syntax for
+  bit-field declarations and formal semantics for bit-field accesses.
+  The translation of bit-field accesses to bit manipulations is
+  performed in the Cshmgen pass and proved correct.
+
+Usability:
+- The layout of bit-fields in memory now follows the ELF ABI
+  algorithm, improving ABI compatibility for the CompCert target
+  platforms that use ELF.
+- Handle the `# 0` line directive generated by some C preprocessors (#398).
+- Un-define the `__SIZEOF_INT128__` macro that is predefined by some C
+  preprocessors (#419).
+- macOS assembler: use `##` instead of `#` to delimit comments (#399).
+
+ISO C conformance:
+- Stricter checking of multi-character constants `'abc'`.
+  Multi-wide-character constants `L'ab'` are now rejected,
+  like GCC and Clang do.
+- Ignore (but still warn about) unnamed plain members of structs
+  and unions (#411).
+- Ignore unnamed bit fields when initializing unions.
+
+Bug fixing:
+- x86 64 bits: overflow in offset of `leaq` instructions (#407).
+- AArch64, ARM, PowerPC, RISC-V: wrong expansion of `__builtin_memcpy_aligned`
+  in cases involving arguments that are stack addresses (#410, #412)
+- PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask
+  instructions (`rldic`, `rldicl`, `rldicr`), resulting in assertion
+  failures later in the compiler.
+- RISC-V: update the Asm semantics to reflect the fact that
+  register X1 is destroyed by some builtins.
+
+Compiler internals:
+- The "PTree" data structure (binary tries) was reimplemented, using
+  a canonical representation that guarantees extensionality and
+  improves performance.
+- Add the ability to give formal semantics to numerical builtins
+  with small integer return types.
+- PowerPC: share code for memory accesses between Asmgen and Asmexpand
+- Declare `__compcert_i64*` helper runtime functions during the C2C
+  pass, so that they are not visible during source elaboration.
+
+The clightgen tool:
+- Add support for producing Csyntax abstract syntax instead of Clight
+  abstract syntax (option `-csyntax` to `clightgen`)
+  (contributed by Bart Jacobs; #404, #413).
+
 Coq development:
+- Added support for Coq 8.14 (#415).
+- Added support for OCaml 4.13.
 - Updated the Flocq library to version 3.4.2.
+- Replaced `Global Set Asymmetric Patterns` by more local settings (#408).
 
 
 Release 3.9, 2021-05-10
diff --git a/INSTALL.md b/INSTALL.md
index f072a211..5e2e800d 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -16,6 +16,7 @@ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.
 ```
 
 ## Post-install
+
 Run
 ```
 eval `opam config env`
@@ -26,8 +27,8 @@ Add this to your `.bashrc` or `.bash_profile`
 ```
 Switch to a recent OCaml compiler version
 ```
-opam switch create 4.09.0
-opam switch 4.09.0
+opam switch create 4.12.0
+opam switch 4.12.0
 ```
 Install dependencies available through opam
 ```
@@ -37,18 +38,20 @@ opam install coq menhir
 Note: it may happen that a newer version of Coq is not supported yet.
 You may downgrade to solve the problem:
 ```
-opam pin add coq 8.11.0 # example of Coq version
+opam pin add coq 8.12.2 # example of Coq version
 ```
 
 ## Compilation
-Pre-compilation configure replace the placeholder with your desired platform
-(for Kalray Coolidge it is `kvx-cos`)
+
+You can choose change the installation directory by modifying the
+`config_simple.sh` file before running the configuration script.
+
+Then, use the configuration script corresponding to your desired platform:
+(for Kalray Coolidge it is `config_kvx.sh`)
 ```
-./configure -prefix ~/.usr <platform>
+./config_<platform>.sh
 ```
 
-`PREFIX` is where CompCert will be installed after `make install`
-
 If using Kalray's platform, make sure that the kvx tools are on your path
 Compile (adapt -j# to the number of cores and available RAM)
 ```
@@ -56,8 +59,22 @@ make -j12
 make install
 ```
 
+## Tests
+
+## Documentation
+
+You can generate the documentation locally with:
+```
+make documentation
+```
+
+Note that you need to install [coq2html](https://github.com/xavierleroy/coq2html)
+before doing so.
+
 ## Utilization
-`ccomp` binaries are installed at `$(PREFIX)/bin`
+
+`ccomp` binaries are installed at `$(CCOMP_INSTALL_PREFIX)/bin`
+(variable defined in `config_simple.sh`).
 Make sure to add that to your path to ease its use
 Now you may use it like a regular compiler
 ```
@@ -66,9 +83,21 @@ ccomp -O3 test.c -o test.bin
 ```
 
 ## Changing platform
+
 If you decide to change the platform, for instance from kvx-cos to kvx-mbr, you
 should change the `compcert.ini` file with the respective tools and then run
 ```
 make install
 ```
 
+## Cleaning
+
+To clean only object files while keeping the platform configuration:
+```
+make clean
+```
+
+To clean everything (to then reconfigure for another platform):
+```
+make distclean
+```
diff --git a/README.md b/README.md
index 3990048e..6406cd27 100644
--- a/README.md
+++ b/README.md
@@ -17,24 +17,51 @@ refer to the [Web site](https://compcert.org/) and especially
 the [user's manual](https://compcert.org/man/).
 
 ## Verimag-Kalray version
+
 This is a special version with additions from Verimag and Kalray :
 
-* A backend for the KVX processor: see [`README_Kalray.md`](README_Kalray.md) for details.
-* Some general-purpose optimization phases (e.g. profiling).
-  * see [`PROFILING.md`](PROFILING.md) for details on the profiling system
+* A backend for the Coolidge VLIW KVX processor.
+* Postpass scheduling passes for KVX, ARMv8 (aarch64) and RISC-V along with a
+  preprocessing peephole optimizer.
+* Improved subexpression elimination: two passes CSE2 and CSE3. Both go through
+  loops and feature a small alias analysis.
+* A generic prepass scheduling optimizer with a multi-purpose preprocessing
+  front-end: rewritings, register renaming, if-lifting and some generic code
+  transformations such as loop-rotation, loop-unrolling, or tail-duplication.
+* A profiling system: see [`PROFILING.md`](PROFILING.md) for details.
+* Static branch prediction.
+* And some experimental features that are work in progress.
+
+_Please refer to the resources listed below for more information._
 	
 The people responsible for this version are
 
 * Sylvain Boulmé (Grenoble-INP, Verimag)
 * David Monniaux (CNRS, Verimag)
 * Cyril Six (Kalray)
+* Léo Gourdin (UGA, Verimag)
+
+with contributions of:
+
+* Justus Fasse (M2R UGA, now at KU Leuven).
+* Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon).
+
+## Installing
+
+Please follow the instructions in [`INSTALL.md`](INSTALL.md)
 
 ## Papers, docs, etc on this CompCert version
 
-* [a 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend
+* [The documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx).
+* [A 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend
 (also on [YouTube if you need subtitles](https://www.youtube.com/watch?v=RAzMDS9OVSw)).
 * [Certified and Efficient Instruction Scheduling](https://hal.archives-ouvertes.fr/hal-02185883), an OOPSLA'20 paper, by Six, Boulmé and Monniaux.
-* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx)
+* [Formally Verified Superblock Scheduling](https://hal.archives-ouvertes.fr/hal-03200774), a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino.
+* [Optimized and formally-verified compilation for a VLIW processor](https://hal.archives-ouvertes.fr/tel-03326923), Phd Thesis of Cyril Six in 2021.
+* [Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) -- Chapters 1 to 3](https://hal.archives-ouvertes.fr/tel-03356701), Habilitation Thesis of Sylvain Boulmé in 2021.
+* [Code Transformations to Increase Prepass Scheduling Opportunities in CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf), MSc Thesis of Justus Fasse in 2021.
+* [Register-Pressure-Aware Prepass-Scheduling for CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf), BSc Thesis of Nicolas Nardino in 2021.
+* [Formally verified postpass scheduling with peephole optimization for AArch64](https://www.lirmm.fr/afadl2021/papers/afadl2021_paper_9.pdf), a short AFADL'21 paper, by Gourdin.
 
 ## License
 CompCert is not free software.  This non-commercial release can only
diff --git a/VERSION b/VERSION
index 51212887..5f95604a 100644
--- a/VERSION
+++ b/VERSION
@@ -1,4 +1,4 @@
-version=3.9
+version=3.10
 buildnr=
 tag=
 branch=
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index 9641d012..3fee2db6 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -149,7 +149,7 @@ Proof.
 - split; simpl; intros.
   + contradiction.
   + rewrite PTree.gempty in H; discriminate.
-  + rewrite PMap.gi in H; contradiction.
+  + contradiction.
 - contradiction.
 - rewrite PTree.gempty in H; discriminate.
 Qed.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 8c58e32e..fcc70ac8 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -4052,7 +4052,7 @@ Lemma ablock_init_sound:
   forall m b p, smatch m b p -> bmatch m b (ablock_init p).
 Proof.
   intros; split; auto; intros.
-  unfold ablock_load, ablock_init; simpl. rewrite ZTree.gempty.
+  unfold ablock_load, ablock_init; simpl.
   eapply vnormalize_cast; eauto. eapply H; eauto.
 Qed.
 
@@ -5172,7 +5172,7 @@ Lemma ematch_init:
   ematch (init_regs vl rl) (einit_regs rl).
 Proof.
   induction rl; simpl; intros.
-- red; intros. rewrite Regmap.gi. simpl AE.get. rewrite PTree.gempty.
+- red; intros. rewrite Regmap.gi. simpl.
   constructor.
 - destruct vl as [ | v1 vs ].
   + assert (ematch (init_regs nil rl) (einit_regs rl)).
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 4c97011e..4afb9285 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -875,7 +875,6 @@ Proof.
   intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto.
   instantiate (1 := f1). red; intros. eelim Mem.fresh_block_alloc; eauto.
   eapply Mem.valid_block_inject_2; eauto.
-  intros. apply PTree.gempty.
   eapply match_callstack_alloc_right; eauto.
   intros. destruct (In_dec peq id (map fst vars)).
   apply cenv_remove_gss; auto.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 507e2128..ea89a8ba 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -893,13 +893,9 @@ Qed.
 Lemma static_bool_val_sound:
   forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b.
 Proof.
-  assert (A: forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false).
-  { unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool; intros.
-    rewrite ! pred_dec_false by (apply Mem.perm_empty). auto. }  
   intros until b; unfold bool_val.
-  destruct (classify_bool t); destruct v; destruct Archi.ptr64 eqn:SF; auto.
-- rewrite A; congruence.
-- simpl; rewrite A; congruence.
+  destruct (classify_bool t); destruct v; destruct Archi.ptr64 eqn:SF; auto;
+  simpl; congruence.
 Qed.
 
 Lemma step_makeif:
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index c133d8ea..d2943f64 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -935,7 +935,6 @@ Proof.
   (* local var, lifted *)
   destruct R as [U V]. exploit H2; eauto. intros [chunk X].
   eapply match_var_lifted with (v := Vundef) (tv := Vundef); eauto.
-  rewrite U; apply PTree.gempty.
   eapply alloc_variables_initial_value; eauto.
   red. unfold empty_env; intros. rewrite PTree.gempty in H4; congruence.
   apply create_undef_temps_charact with ty.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 4c9e7889..f424a69d 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -265,15 +265,6 @@ Qed.
 
 Program Definition empty_genv (pub: list ident): t :=
   @mkgenv pub (PTree.empty _) (PTree.empty _) 1%positive _ _ _.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
 
 Definition globalenv (p: program F V) :=
   add_globals (empty_genv p.(prog_public)) p.(prog_defs).
diff --git a/common/Memory.v b/common/Memory.v
index ff17efb0..e243d475 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -348,15 +348,6 @@ Program Definition empty: mem :=
   mkmem (PMap.init (ZMap.init Undef))
         (PMap.init (fun ofs k => None))
         1%positive _ _ _.
-Next Obligation.
-  repeat rewrite PMap.gi. red; auto.
-Qed.
-Next Obligation.
-  rewrite PMap.gi. auto.
-Qed.
-Next Obligation.
-  rewrite PMap.gi. auto.
-Qed.
 
 (** Allocation of a fresh block with the given bounds.  Return an updated
   memory state and the address of the fresh block, which initially contains
@@ -675,7 +666,7 @@ Proof. reflexivity. Qed.
 
 Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Proof.
-  intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto.
+  intros. unfold perm, empty; simpl. tauto.
 Qed.
 
 Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
diff --git a/configure b/configure
index c8a956ec..3da00fb3 100755
--- a/configure
+++ b/configure
@@ -548,7 +548,7 @@ case "$coq_ver" in
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.0"
+            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.1"
             missingtools=true
         fi;;
   "")
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 4fae584e..aa71eb1a 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -413,34 +413,29 @@ let elab_float_constant f =
   (v, ty)
 
 let elab_char_constant loc wide chars =
+  let len = List.length chars in
   let nbits = if wide then 8 * !config.sizeof_wchar else 8 in
-  (* Treat multi-char constants as a number in base 2^nbits *)
   let max_digit = Int64.shift_left 1L nbits in
-  let max_val = Int64.shift_left 1L (64 - nbits) in
-  let v,_ =
-    List.fold_left
-      (fun (acc,err) d ->
-        if not err then begin
-          let overflow = acc < 0L || acc >= max_val
-          and out_of_range = d < 0L || d >= max_digit in
-          if overflow then
-            error loc "character constant too long for its type";
-          if out_of_range then
+  (* Treat multi-character constants as a number in base 2^nbits.
+     It must fit in type int for a normal constant and in type wchar_t
+     for a wide constant. *)
+  let v =
+    if len > (if wide then 1 else !config.sizeof_int) then begin
+      error loc "%d-character constant too long for its type" len;
+      0L
+    end else
+      List.fold_left
+        (fun acc d ->
+          if d < 0L || d >= max_digit then
             error loc "escape sequence is out of range (code 0x%LX)" d;
-          Int64.add (Int64.shift_left acc nbits) d,overflow || out_of_range
-        end else
-          Int64.add (Int64.shift_left acc nbits) d,true
-      )
-      (0L,false) chars in
-  if not (integer_representable v IInt) then
-    warning loc Unnamed "character constant too long for its type";
-  (* C99 6.4.4.4 item 10: single character -> represent at type char
-     or wchar_t *)
+          Int64.add (Int64.shift_left acc nbits) d)
+        0L chars in
+  (* C99 6.4.4.4 items 10 and 11:
+       single-character constant -> represent at type char
+       multi-character constant -> represent at type int
+       wide character constant -> represent at type wchar_t *)
   Ceval.normalize_int v
-    (if List.length chars = 1 then
-       if wide then wchar_ikind() else IChar
-     else
-       IInt)
+    (if wide then wchar_ikind() else if len = 1 then IChar else IInt)
 
 let elab_string_literal loc wide chars =
   let nbits = if wide then 8 * !config.sizeof_wchar else 8 in
@@ -646,6 +641,36 @@ let get_nontype_attrs env ty =
   let nta = List.filter to_be_removed (attributes_of_type_no_expand ty) in
   (remove_attributes_type env nta ty, nta)
 
+(* Auxiliary for elaborating bitfield declarations. *)
+
+let check_bitfield loc env id ty ik n =
+  let max = Int64.of_int(sizeof_ikind ik * 8) in
+  if n < 0L then begin
+    error loc "bit-field '%a' has negative width (%Ld)" pp_field id n;
+    None
+  end else if n >  max then begin
+    error loc "size of bit-field '%a' (%Ld bits) exceeds its type (%Ld bits)" pp_field id n max;
+    None
+  end else if n = 0L && id <> "" then begin
+    error loc "named bit-field '%a' has zero width" pp_field id;
+    None
+  end else begin
+    begin match unroll env ty with
+    | TEnum(eid, _) ->
+      let info = wrap Env.find_enum loc env eid in
+      let w = Int64.to_int n in
+      let representable sg =
+        List.for_all (fun (_, v, _) -> Cutil.int_representable v w sg)
+                     info.Env.ei_members in
+      if not (representable false || representable true) then
+        warning loc Unnamed
+          "not all values of type 'enum %s' can be represented in bit-field '%a' (%d bits are not enough)"
+          eid.C.name pp_field id w
+    | _ -> ()
+    end;
+    Some (Int64.to_int n)
+  end
+
 (* Elaboration of a type specifier.  Returns 6-tuple:
      (storage class, "inline" flag, "noreturn" flag, "typedef" flag,
       elaborated type, new env)
@@ -1041,23 +1066,11 @@ and elab_field_group env = function
             error loc "alignment specified for bit-field '%a'" pp_field id;
             None, env
           end else begin
-            let expr,env' =(!elab_expr_f loc env sz) in
+            let expr,env' = !elab_expr_f loc env sz in
             match Ceval.integer_expr env' expr with
             | Some n ->
-                if n < 0L then begin
-                  error loc "bit-field '%a' has negative width (%Ld)" pp_field id n;
-                  None,env
-                end else
-                  let max = Int64.of_int(sizeof_ikind ik * 8) in
-                  if n >  max then begin
-                    error loc "size of bit-field '%a' (%Ld bits) exceeds its type (%Ld bits)" pp_field id n max;
-                    None,env
-                end else
-                if n = 0L && id <> "" then begin
-                  error loc "named bit-field '%a' has zero width" pp_field id;
-                  None,env
-                end else
-                  Some(Int64.to_int n),env'
+                let bf = check_bitfield loc env' id ty ik n in
+                bf,env'
             | None ->
                 error loc "bit-field '%a' width not an integer constant" pp_field id;
                 None,env
diff --git a/doc/ccomp.1 b/doc/ccomp.1
index 89e8c823..edae57e1 100644
--- a/doc/ccomp.1
+++ b/doc/ccomp.1
@@ -9,7 +9,7 @@ ccomp \- the CompCert C compiler
 \fBCompCert C\fP is a compiler for the C programming language.
 Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance.
 It accepts most of the ISO C 99 language, with some exceptions and a few extensions.
-It produces machine code for the PowerPC (32bit), ARM (32bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
+It produces machine code for the PowerPC (32bit), ARM (32bit), AArch64 (ARM 64bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
 .PP
 What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues.
 In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program.
@@ -327,11 +327,6 @@ Language Support Options
 .INDENT 0.0
 .
 .TP
-.BR \-fbitfields ", " \-fno\-bitfields
-Turn on/off support for emulation bit fields in structs.
-Disabled by default.
-.
-.TP
 .BR \-flongdouble ", " \-fno\-longdouble
 Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP.
 Disabled by default.
diff --git a/doc/index-verimag.html b/doc/index-verimag.html
new file mode 100644
index 00000000..daed4d6d
--- /dev/null
+++ b/doc/index-verimag.html
@@ -0,0 +1,707 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<HTML>
+<HEAD>
+<TITLE>The CompCert verified compiler</TITLE>
+<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
+
+<style type="text/css">
+body {
+  color: black; background: white;
+  margin-left: 5%; margin-right: 5%;
+}
+h2 { margin-left: -5%;}
+h3 { margin-left: -3%; }
+h1,h2,h3 { font-family: sans-serif; }
+hr { margin-left: -5%; margin-right:-5%; }
+a:visited {color : #416DFF; text-decoration : none; font-weight : bold}
+a:link {color : #416DFF; text-decoration : none; font-weight : bold}
+a:hover {color : Red; text-decoration : underline; }
+a:active {color : Red; text-decoration : underline; }
+</style>
+
+</HEAD>
+<BODY>
+  <font color=gray>
+<H1 align="center">The CompCert verified compiler</H1>
+<H2 align="center">Commented Coq development</H2>
+<H3 align="center">Version 3.10, 2021-11-19</H3>
+</font>
+<H3 align="center"><a href="https://www-verimag.imag.fr">VERIMAG</a> fork version 2021-12-07</H3>
+
+<H2>The CompCert Verimag's fork</H2>
+<p>This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on <A HREF="http://compcert.org/doc/index.html">the CompCert Web site</A>.
+  The unmodified parts of this table appear in <font color=gray>gray</font>.
+  <br>
+  <br>
+  A high-level view of this CompCert backend is provided by the following documents:
+
+  <ul>
+    <li><a href="https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx">The Git repo README.md</a>.</li>
+    <li><a href="http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4">A 5-minutes video</a> by C. Six, presenting the postpass scheduling and the KVX backend
+    (also on <a href="https://www.youtube.com/watch?v=RAzMDS9OVSw">YouTube if you need subtitles</a>).</li>
+    <li><a href="https://hal.archives-ouvertes.fr/hal-02185883">Certified and Efficient Instruction Scheduling</a>, an OOPSLA'20 paper, by Six, Boulm&eacute; and Monniaux.</li>
+    <li><a href="https://hal.archives-ouvertes.fr/hal-03200774">Formally Verified Superblock Scheduling</a>, a CPP'22 paper, by Six, Gourdin, Boulm&eacute;, Monniaux, Fasse and Nardino.</li>
+    <li><a href="https://hal.archives-ouvertes.fr/tel-03326923">Optimized and formally-verified compilation for a VLIW processor</a>, Phd Thesis of Cyril Six in 2021.</li>
+    <li><a href="https://hal.archives-ouvertes.fr/tel-03356701">Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) &ndash; Chapters 1 to 3</a>, Habilitation Thesis of Sylvain Boulm&eacute; in 2021.</li>
+    <li><a href="https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf">Code Transformations to Increase Prepass Scheduling Opportunities in CompCert</a>, MSc Thesis of Justus Fasse in 2021.</li>
+    <li><a href="https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf">Register-Pressure-Aware Prepass-Scheduling for CompCert</a>, BSc Thesis of Nicolas Nardino in 2021.</li>
+    <li><a href="https://www.lirmm.fr/afadl2021/papers/afadl2021_paper_9.pdf">Formally verified postpass scheduling with peephole optimization for AArch64</a>, a short AFADL'21 paper, by Gourdin.</li>
+  </ul>
+
+  <p>The people responsible for this version are</p>
+
+  <ul>
+    <li>Sylvain Boulm&eacute; (Grenoble-INP, Verimag)</li>
+    <li>David Monniaux (CNRS, Verimag)</li>
+    <li>Cyril Six (Kalray)</li>
+    <li>L&eacute;o Gourdin (UGA, Verimag)</li>
+  </ul>
+
+
+  <p>with contributions of:</p>
+
+  <ul>
+    <li>Justus Fasse (M2R UGA, now at KU Leuven).</li>
+    <li>Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon).</li>
+  </ul>
+
+</p>
+
+<H2>Introduction</H2>
+
+<font color="gray">
+<P>CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly
+code from CompCert C, a large subset of the C programming language.
+The particularity of this compiler is that it is written mostly within
+the specification language of the Coq proof assistant, and its
+correctness --- the fact that the generated assembly code is
+semantically equivalent to its source program --- was entirely proved
+within the Coq proof assistant.</P>
+
+<P>High-level descriptions of the CompCert compiler and its proof of 
+correctness can be found in the following papers (in increasing order of technical details):</P>
+<UL>
+<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
+<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
+Journal of Automated Reasoning 43(4):363-446, 2009.
+</UL>
+
+<P>This Web site gives a commented listing of the underlying Coq
+specifications and proofs.  Proof scripts are folded by default, but
+can be viewed by clicking on "Proof".  Some modules (written in <I>italics</I> below) differ between the five target architectures.  The
+PowerPC versions of these modules are shown below; the AArch64, ARM,
+x86 and RISC-V versions can be found in the source distribution.
+</P>
+
+<P> This development is a work in progress; some parts have
+substantially changed since the overview papers above were
+written.</P>
+
+<P>The complete sources for CompCert can be downloaded from
+<A HREF="https://github.com/AbsInt/CompCert/">the Git repository</A>
+or <A HREF="https://compcert.org/">the CompCert Web site</A>.
+</P>
+
+<P>This document and the CompCert sources are copyright Institut
+National de Recherche en Informatique et en Automatique (INRIA) and
+AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the
+following <A HREF="https://compcert.org/doc/LICENSE.txt">license</A>.
+</P>
+</font>
+
+<H2>Table of contents</H2>
+
+<font color="gray">
+<H3>General-purpose libraries, data structures and algorithms</H3>
+
+<UL>
+<LI> <A HREF="html/compcert.lib.Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
+<LI> <A HREF="html/compcert.lib.Maps.html">Maps</A>: finite maps.
+<LI> <A HREF="html/compcert.lib.Integers.html">Integers</A>: machine integers.
+<LI> <A HREF="html/compcert.lib.Floats.html">Floats</A>: machine floating-point numbers.
+<LI> <A HREF="html/compcert.lib.Iteration.html">Iteration</A>: various forms of "while" loops.
+<LI> <A HREF="html/compcert.lib.Ordered.html">Ordered</A>: construction of
+ordered types.
+<LI> <A HREF="html/compcert.lib.Lattice.html">Lattice</A>: construction of
+semi-lattices.
+<LI> <A HREF="html/compcert.backend.Kildall.html">Kildall</A>: resolution of dataflow
+inequations by fixpoint iteration.
+<LI> <A HREF="html/compcert.lib.UnionFind.html">UnionFind</A>: a persistent union-find data structure.
+<LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph.
+</UL></font>
+
+<H4><A HREF=https://github.com/boulme/ImpureDemo>The Impure library</A> (of Boulm&eacute;)</H4>
+<UL>
+<LI><A HREF="html/compcert.lib.Impure.ImpConfig.html">ImpConfig</A>: declares the <tt>Impure</tt> monad and defines its extraction.</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpCore.html">ImpCore</A>: defines notations for the <tt>Impure</tt> monad and a <tt>wlp_simplify</tt> tactic (to reason about <tt>Impure</tt> functions in a Hoare-logic style).</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpLoops.html">ImpLoops</A>, <A HREF="html/compcert.lib.Impure.ImpIO.html">ImpIO</A>, <A HREF="html/compcert.lib.Impure.ImpHCons.html">ImpHCons</A>: declare <tt>Impure</tt> oracles and define operators from these oracles. <A HREF="html/compcert.lib.Impure.ImpExtern.html">ImpExtern</A> exports all these impure operators.</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpMonads.html">ImpMonads</A>: axioms of "impure computations" and some Coq models of these axioms.</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpPrelude.html">ImpPrelude</A>: declares the data types exchanged with <tt>Impure</tt> oracles.</LI>
+</UL>
+
+<H4 id="abstractbb">The <tt>abstractbb</tt> library, introduced for Aarch64 and KVX cores</H4>
+This library introduces a block intermediate representation used for postpass scheduling verification. It might be extended to others backends.
+<UL>
+<LI> <A HREF="html/compcert.scheduling.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks.
+<LI> <A HREF="html/compcert.scheduling.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
+<LI> <A HREF="html/compcert.scheduling.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.scheduling.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing and uses <A HREF=https://github.com/boulme/ImpureDemo>the Impure library</A> to reason on physical equality and handling of imperative code in Coq.
+</UL>
+
+<font color=gray>
+<H3>Definitions and theorems used in many parts of the development</H3>
+
+<UL>
+<LI> <A HREF="html/compcert.common.Errors.html">Errors</A>: the Error monad.
+<LI> <A HREF="html/compcert.common.AST.html">AST</A>: identifiers, whole programs and other
+common elements of abstract syntaxes.
+<LI> <A HREF="html/compcert.common.Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages.
+<LI> <A HREF="html/compcert.common.Values.html">Values</A>: run-time values.
+<LI> <A HREF="html/compcert.common.Events.html">Events</A>: observable events and traces.
+<LI> <A HREF="html/compcert.common.Memory.html">Memory</A>: memory model. <BR>
+See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory representation of data).
+<LI> <A HREF="html/compcert.common.Globalenvs.html">Globalenvs</A>: global execution environments.
+<LI> <A HREF="html/compcert.common.Smallstep.html">Smallstep</A>: tools for small-step semantics.
+<LI> <A HREF="html/compcert.common.Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
+<LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics.
+<LI> <A HREF="html/compcert.kvx.Op.html"><I>Op</I></A>: operators, addressing modes and their
+semantics.
+<LI> <A HREF="html/compcert.common.Builtins.html">Builtins</A>: semantics of built-in functions. <BR>
+See also: <A HREF="html/compcert.common.Builtins0.html">Builtins0</A> (target-independent part), <A HREF="html/compcert.kvx.Builtins1.html"><I>Builtins1</I></A> (target-dependent part).
+<LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints.
+</UL>
+
+<H3>Source, intermediate and target languages: syntax and semantics</H3>
+
+<UL>
+<LI> The CompCert C source language:
+<A HREF="html/compcert.cfrontend.Csyntax.html">syntax</A> and
+<A HREF="html/compcert.cfrontend.Csem.html">semantics</A> and
+<A HREF="html/compcert.cfrontend.Cstrategy.html">determinized semantics</A> and
+<A HREF="html/compcert.cfrontend.Ctyping.html">type system</A>.<BR>
+See also: <A HREF="html/compcert.cfrontend.Ctypes.html">type expressions</A> and
+<A HREF="html/compcert.cfrontend.Cop.html">operators (syntax and semantics)</A>.<BR>
+See also: <A HREF="html/compcert.cfrontend.Cexec.html">reference interpreter</A>.
+<LI> <A HREF="html/compcert.cfrontend.Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects.
+<LI> <A HREF="html/compcert.cfrontend.Csharpminor.html">Csharpminor</A>: low-level
+ structured language.
+<LI> <A HREF="html/compcert.backend.Cminor.html">Cminor</A>: low-level structured
+language, with explicit stack allocation of certain local variables.
+<LI> <A HREF="html/compcert.backend.CminorSel.html">CminorSel</A>: like Cminor,
+with machine-specific operators and addressing modes.
+<LI> <A HREF="html/compcert.backend.RTL.html">RTL</A>: register transfer language (3-address
+code, control-flow graph, infinitely many pseudo-registers). <BR>
+See also: <A HREF="html/compcert.backend.Registers.html">Registers</A> (representation of
+pseudo-registers).
+<LI> <A HREF="html/compcert.backend.LTL.html">LTL</A>: location transfer language (3-address
+code, control-flow graph of basic blocks, finitely many physical registers, infinitely
+many stack slots). <BR>
+See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of
+locations) and <A HREF="html/compcert.kvx.Machregs.html"><I>Machregs</I></A> (description of processor registers).
+<LI> <A HREF="html/compcert.backend.Linear.html">Linear</A>: like LTL, but the CFG is
+replaced by a linear list of instructions with explicit branches and labels.
+<LI> <A HREF="html/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete
+view of the activation record.  
+<LI> <A HREF="html/compcert.kvx.Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
+code.
+</font>
+
+<H4>Languages introduced in the VERIMAG version</H4>
+
+Generic (or possibly adaptable) Intermediate Representations (IR):
+<UL>
+  <LI> <A HREF="html/compcert.scheduling.BTL.html">BTL</A>: an IR dedicated to defensive certification of middle-end optimizations (before register allocation).
+  BTL stands for "Block Transfer Language". <!-- TODO add a link to some markdown draft here -->
+  <LI> <A HREF="html/compcert.scheduling.postpass_lib.Machblock.html">Machblock</A>: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step).
+  This IR is generic over the processor and used for KVX and Aarch64.
+  <LI> <A HREF="html/compcert.kvx.Asmblock.html"><I>Asmblock</I></A>: a variant of Asm, with a big-step semantics of basic-blocks.
+  This IR is an intermediate step between Machblock and Asm on backends featuring postpass scheduling (KVX and Aarch64).
+  <LI> <A HREF="#abstractbb"><I>AbstractBasicBlocks</I></A>: the AbstractBasicBlocks Domain Specific Language (DSL) used in the postpass scheduling verification.
+  This DSL is only used as a library on KVX and Aarch64.
+</UL>
+
+Specific to KVX:
+<UL>
+  <LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles.
+  <LI> <A HREF="html/compcert.kvx.Asm.html"><I>kvx/Asm</I></A>: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of <I>Asmvliw</I> for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax).
+</UL>
+
+<H3>Compiler passes</H3>
+
+<TABLE cellpadding="5%" style="color:#808080">
+<TR valign="top">
+  <TH align=left>Pass</TH>
+  <TH align=left>Source &amp; target</TH>
+  <TH align=left>Compiler&nbsp;code</TH>
+  <TH align=left>Correctness&nbsp;proof</TH>
+</TR>
+
+<TR valign="top">
+  <TD>Pulling side-effects out of expressions;<br>
+      fixing an evaluation order</TD>
+  <TD>CompCert C to Clight</TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplExpr.html">SimplExpr</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplExprspec.html">SimplExprspec</A><br>
+      <A HREF="html/compcert.cfrontend.SimplExprproof.html">SimplExprproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Pulling non-adressable scalar local variables out of memory</TD>
+  <TD>Clight to Clight</TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplLocals.html">SimplLocals</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplLocalsproof.html">SimplLocalsproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Simplification of control structures; <br>
+      explication of type-dependent computations</TD>
+  <TD>Clight to Csharpminor</TD>
+  <TD><A HREF="html/compcert.cfrontend.Cshmgen.html">Cshmgen</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cshmgenproof.html">Cshmgenproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Stack allocation of local variables<br>
+      whose address is taken;<br>
+      simplification of switch statements</TD>
+  <TD>Csharpminor to Cminor</TD>
+  <TD><A HREF="html/compcert.cfrontend.Cminorgen.html">Cminorgen</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cminorgenproof.html">Cminorgenproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Recognition of operators<br>and addressing modes;<br>
+      if-conversion</TD>
+  <TD>Cminor to CminorSel</TD>
+  <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br>
+      <A HREF="html/compcert.kvx.SelectOp.html"><I>SelectOp</I></A><br>
+      <A HREF="html/compcert.kvx.SelectLong.html"><I>SelectLong</I></A><br>
+      <A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br>
+      <A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD>
+  <TD><A HREF="html/compcert.backend.Selectionproof.html">Selectionproof</A><br>
+      <A HREF="html/compcert.kvx.SelectOpproof.html"><I>SelectOpproof</I></A><br>
+      <A HREF="html/compcert.kvx.SelectLongproof.html"><I>SelectLongproof</I></A><br>
+      <A HREF="html/compcert.backend.SelectDivproof.html">SelectDivproof</A><br>
+      <A HREF="html/compcert.backend.SplitLongproof.html">SplitLongproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Construction of the CFG, <br>3-address code generation</TD>
+  <TD>CminorSel to RTL</TD>
+  <TD><A HREF="html/compcert.backend.RTLgen.html">RTLgen</A></TD>
+  <TD><A HREF="html/compcert.backend.RTLgenspec.html">RTLgenspec</A><BR>
+      <A HREF="html/compcert.backend.RTLgenproof.html">RTLgenproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Recognition of tail calls</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Tailcall.html">Tailcall</A></TD>
+  <TD><A HREF="html/compcert.backend.Tailcallproof.html">Tailcallproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Function inlining</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Inlining.html">Inlining</A></TD>
+  <TD><A HREF="html/compcert.backend.Inliningspec.html">Inliningspec</A><BR>
+      <A HREF="html/compcert.backend.Inliningproof.html">Inliningproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>Passes introduced for profiling (for later use in trace selection)</b></TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Insert profiling annotations (for recording experiments -- see PROFILE.md).
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Profiling.html">Profiling</A></TD>
+  <TD><A HREF="html/compcert.backend.Profilingproof.html">Profilingproof</A></TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Update ICond nodes (from recorded experiments -- see PROFILE.md).
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.ProfilingExploit.html">ProfilingExploit</A></TD>
+  <TD><A HREF="html/compcert.backend.ProfilingExploitproof.html">ProfilingExploitproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>FirstNop: Inserting a no-op instruction at each RTL function entrypoint</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.FirstNop.html">FirstNop</A></TD>
+  <TD><A HREF="html/compcert.backend.FirstNopproof.html">FirstNopproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (1)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>[CSE1] Common subexpression elimination (1)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR>
+      <A HREF="html/compcert.kvx.CombineOp.html"><I>CombineOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
+      <A HREF="html/compcert.kvx.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>[Duplicate pass] Static Prediction + Unroll single</b></TD>
+<TR valign="top" style="color:#000000">
+  <TD>Add static prediction information to Icond nodes<BR>
+      Unrolls a single iteration of innermost loops
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Duplicate.html">Duplicate</A> (generic checker)</TD>
+  <TD><A HREF="html/compcert.backend.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR>
+    <a href="html/compcert.backend.Duplicatepasses.html">Duplicatepasses</a> (several passes from several oracles)</TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (2)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>[Duplicate pass] Tail Duplication</b></TD>
+<TR valign="top" style="color:#000000">
+  <TD>Performs tail duplication on interesting traces to form superblocks
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Duplicate.html">Duplicate</A> (generic checker)</TD>
+  <TD><A HREF="html/compcert.backend.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR>
+    <a href="html/compcert.backend.Duplicatepasses.html">Duplicatepasses</a> (several passes from several oracles)</TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (3)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>[Duplicate pass] Unroll body</b></TD>
+<TR valign="top" style="color:#000000">
+  <TD>Unrolling the body of innermost loops
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Duplicate.html">Duplicate</A> (generic checker)</TD>
+  <TD><A HREF="html/compcert.backend.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR>
+    <a href="html/compcert.backend.Duplicatepasses.html">Duplicatepasses</a> (several passes from several oracles)</TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (4)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Constant propagation</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br>
+      <A HREF="html/compcert.kvx.ConstpropOp.html"><I>ConstpropOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br>
+      <A HREF="html/compcert.kvx.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (5)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>[CSE1] Common subexpression elimination (1)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR>
+      <A HREF="html/compcert.kvx.CombineOp.html"><I>CombineOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
+      <A HREF="html/compcert.kvx.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>[CSE2] Common subexpression elimination</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.CSE2.html">CSE2</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.CSE2proof.html">CSE2proof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>[CSE3] Common subexpression elimination (1)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.CSE3.html">CSE3</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.CSE3proof.html">CSE3proof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>KillUselessMoves: removing useless moves instructions after CSE3</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.KillUselessMoves.html">KillUselessMoves</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.KillUselessMovesproof.html">KillUselessMovesproof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>Forwarding Moves</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.ForwardMoves.html">ForwardMoves</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.ForwardMovesproof.html">ForwardMovesproof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top">
+  <TD>Redundancy elimination (1)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Deadcode.html">Deadcode</A></TD>
+  <TD><A HREF="html/compcert.backend.Deadcodeproof.html">Deadcodeproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>RTL Tunneling</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.RTLTunneling.html">RTLTunneling</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.RTLTunnelingproof.html">RTLTunnelingproof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (6)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>[Duplicate pass] Loop Rotate</b></TD>
+<TR valign="top" style="color:#000000">
+  <TD>Loop rotation
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Duplicate.html">Duplicate</A> (generic checker)</TD>
+  <TD><A HREF="html/compcert.backend.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR>
+    <a href="html/compcert.backend.Duplicatepasses.html">Duplicatepasses</a> (several passes from several oracles)</TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (7)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>Loop Invariant Code Motion
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.LICM.html">LICM</A></TD>
+  <TD><A HREF="html/compcert.backend.LICMproof.html">LICMproof</A>
+  </TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG (8)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>[CSE3] Common subexpression elimination (2)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.CSE3.html">CSE3</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.CSE3proof.html">CSE3proof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top">
+  <TD>Redundancy elimination (2)</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Deadcode.html">Deadcode</A></TD>
+  <TD><A HREF="html/compcert.backend.Deadcodeproof.html">Deadcodeproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>Allnontrap: transforming loads to non-trapping ones</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Allnontrap.html">Allnontrap</A><BR>
+  </TD>
+  <TD><A HREF="html/compcert.backend.Allnontrapproof.html">Allnontrapproof</A><BR>
+  </TD>
+</TR>
+
+<TR valign="top">
+  <TD>Removal of unused static globals</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Unusedglob.html">Unusedglob</A></TD>
+  <TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>Passes introduced for BTL</b></TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Block selection (with Liveness information)</TD>
+  <TD>RTL to BTL</TD>
+  <TD><A HREF="html/compcert.scheduling.RTLtoBTL.html">RTLtoBTL</A></TD>
+  <TD><A HREF="html/compcert.scheduling.RTLtoBTLproof.html">RTLtoBTLproof</A><BR>
+  <A HREF="html/compcert.scheduling.BTLmatchRTL.html">BTLmatchRTL</A><BR>
+  <A HREF="html/compcert.scheduling.BTL_Livecheck.html">BTL_Livecheck</A>
+  </TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Superblock prepass scheduling</TD>
+  <TD>BTL to BTL</TD>
+  <TD><A HREF="html/compcert.scheduling.BTL_Scheduler.html">BTL_Scheduler</A></TD>
+  <TD><A HREF="html/compcert.scheduling.BTL_Schedulerproof.html">BTL_Schedulerproof</A><BR>
+    with <A HREF="html/compcert.scheduling.BTL_SEtheory.html">BTL_SEtheory</A> (the theory of symbolic execution on BTL_)<BR>
+    and <A HREF="html/compcert.scheduling.BTL_SEsimuref.html">BTL_SEsimuref</A> (the low-level specifications of the simulation checker)<BR>
+    and <A HREF="html/compcert.scheduling.BTL_SEimpl.html">BTL_SEimpl</A> (the simulation checker with hash-consing)</TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Forgeting blocks</TD>
+  <TD>BTL to RTL</TD>
+  <TD><A HREF="html/compcert.scheduling.BTLtoRTL.html">BTLtoRTL</A></TD>
+  <TD><A HREF="html/compcert.scheduling.BTLtoRTLproof.html">BTLtoRTLproof</A><BR>
+  <A HREF="html/compcert.scheduling.BTLmatchRTL.html">BTLmatchRTL</A>
+  </TD>
+</TR>
+
+<TR valign="top">
+  <TD colspan="4"><b>Passes from register allocation</b></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Register allocation (validation a posteriori)</TD>
+  <TD>RTL to LTL</TD>
+  <TD><A HREF="html/compcert.backend.Allocation.html">Allocation</A></TD>
+  <TD><A HREF="html/compcert.backend.Allocationproof.html">Allocationproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Branch tunneling</TD>
+  <TD>LTL to LTL</TD>
+  <TD><A HREF="html/compcert.backend.LTLTunneling.html">LTLTunneling</A></TD>
+  <TD><A HREF="html/compcert.backend.LTLTunnelingproof.html">LTLTunnelingproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Linearization of the CFG</TD>
+  <TD>LTL to Linear</TD>
+  <TD><A HREF="html/compcert.backend.Linearize.html">Linearize</A></TD>
+  <TD><A HREF="html/compcert.backend.Linearizeproof.html">Linearizeproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Removal of unreferenced labels</TD>
+  <TD>Linear to Linear</TD>
+  <TD><A HREF="html/compcert.backend.CleanupLabels.html">CleanupLabels</A></TD>
+  <TD><A HREF="html/compcert.backend.CleanupLabelsproof.html">CleanupLabelsproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Synthesis of debugging information</TD>
+  <TD>Linear to Linear</TD>
+  <TD><A HREF="html/compcert.backend.Debugvar.html">Debugvar</A></TD>
+  <TD><A HREF="html/compcert.backend.Debugvarproof.html">Debugvarproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Laying out the activation records</TD>
+  <TD>Linear to Mach</TD>
+  <TD><A HREF="html/compcert.backend.Stacking.html">Stacking</A><BR>
+      <A HREF="html/compcert.backend.Bounds.html">Bounds</A><BR>
+      <A HREF="html/compcert.kvx.Stacklayout.html"><I>Stacklayout</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Stackingproof.html">Stackingproof</A><br>
+      <A HREF="html/compcert.common.Separation.html">Separation</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>Passes introduced for backends with postpass scheduling</b></TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Reconstruction of basic-blocks at Mach level</TD>
+  <TD>Mach to Machblock</TD>
+  <TD><A HREF="html/compcert.scheduling.postpass_lib.Machblockgen.html">Machblockgen</A></TD>
+  <TD><A HREF="html/compcert.scheduling.postpass_lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR>
+      <A HREF="html/compcert.scheduling.postpass_lib.Machblockgenproof.html">Machblockgenproof</A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>Emission of purely sequential assembly code</TD>
+  <TD>Machblock to Asmblock</TD>
+  <TD><A HREF="html/compcert.kvx.Asmblockgen.html"><I>Asmblockgen</I></A></TD>
+  <TD><A HREF="html/compcert.kvx.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR>
+      <A HREF="html/compcert.kvx.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR>
+      <A HREF="html/compcert.kvx.Asmblockgenproof.html"><I>Asmblockgenproof</I></A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>Bundling (and basic-block scheduling)</TD>
+  <TD>Asmblock to Asmvliw</TD>
+  <TD><A HREF="html/compcert.kvx.PostpassScheduling.html"><I>PostpassScheduling</I></A><BR>
+    using <A HREF="html/compcert.kvx.Asmblockdeps.html"><I>Asmblockdeps</I></A><BR>
+    and the <tt>abstractbb</tt> library</TD>
+  <TD><A HREF="html/compcert.kvx.PostpassSchedulingproof.html"><I>PostpassSchedulingproof</I></A><BR>
+    <A HREF="html/compcert.kvx.Asmblockprops.html"><I>Asmblockprops</I></A></TD>
+</TR>
+
+<TR valign="top" style="color:#000000">
+  <TD>Flattening bundles (only a bureaucratic operation)</TD>
+  <TD>Asmvliw to Asm</TD>
+  <TD><A HREF="html/compcert.kvx.Asmgen.html"><I>Asmgen</I></A></TD>
+  <TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A> (whole simulation proof from <tt>Mach</tt> to <tt>Asm</tt>)</TD>
+</TR>
+</TABLE>
+
+<H3>All together (there are many more passes than on vanilla CompCert: their order is specified in Compiler)</H3>
+</font>
+<font color=gray>
+
+<UL>
+<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together;
+whole-compiler semantic preservation theorems.
+<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
+</UL>
+
+<H3>Static analyses</H3>
+
+The following static analyses are performed over the RTL intermediate
+representation to support optimizations such as constant propagation,
+CSE, and dead code elimination.
+<UL>
+<LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>.
+<LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
+See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
+See also: <A HREF="html/compcert.kvx.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
+<LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
+See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
+See also: <A HREF="html/compcert.kvx.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
+</UL>
+
+<H3>Type systems</H3>
+
+The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
+<UL>
+<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for CompCert C + type-checking functions.
+<LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type
+reconstruction.
+<LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
+</UL>
+</font>
+
+</BODY>
+</HTML>
diff --git a/doc/index.html b/doc/index.html
index 34b87924..e7d97a5d 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -25,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.9, 2021-05-10</H3>
+<H3 align="center">Version 3.10, 2021-11-19</H3>
 
 <H2>Introduction</H2>
 
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 016dad75..99a31632 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -3,6 +3,7 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*          Andrew W. Appel, Princeton University                      *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
@@ -240,7 +241,7 @@ Definition bot : t := PTree.empty _.
 
 Lemma get_bot: forall p, get p bot = L.bot.
 Proof.
-  unfold bot, get; intros; simpl. rewrite PTree.gempty. auto.
+  intros; reflexivity.
 Qed.
 
 Lemma ge_bot: forall x, ge x bot.
@@ -248,13 +249,7 @@ Proof.
   unfold ge; intros. rewrite get_bot. apply L.ge_bot.
 Qed.
 
-(** A [combine] operation over the type [PTree.t L.t] that attempts
-  to share its result with its arguments. *)
-
-Section COMBINE.
-
-Variable f: option L.t -> option L.t -> option L.t.
-Hypothesis f_none_none: f None None = None.
+(** Equivalence modulo L.eq *)
 
 Definition opt_eq (ox oy: option L.t) : Prop :=
   match ox, oy with
@@ -294,182 +289,181 @@ Proof.
   auto.
 Qed.
 
-Definition tree_eq (m1 m2: PTree.t L.t) : Prop :=
-  forall i, opt_eq (PTree.get i m1) (PTree.get i m2).
-
-Lemma tree_eq_refl: forall m, tree_eq m m.
-Proof. intros; red; intros; apply opt_eq_refl. Qed.
-
-Lemma tree_eq_sym: forall m1 m2, tree_eq m1 m2 -> tree_eq m2 m1.
-Proof. intros; red; intros; apply opt_eq_sym; auto. Qed.
+Local Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym : combine.
 
-Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3.
-Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed.
-
-Lemma tree_eq_node:
-  forall l1 o1 r1 l2 o2 r2,
-  tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
-  tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2).
-Proof.
-  intros; red; intros. destruct i; simpl; auto.
-Qed.
-
-Lemma tree_eq_node':
-  forall l1 o1 r1 l2 o2 r2,
-  tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
-  tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2).
-Proof.
-  intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto.
-Qed.
+(** A [combine] operation over the type [PTree.t L.t] that attempts
+  to share its result with its arguments. *)
 
-Lemma tree_eq_node'':
-  forall l1 o1 r1 l2 o2 r2,
-  tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
-  tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2).
-Proof.
-  intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto.
-Qed.
+Section COMBINE.
 
-Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym
-             tree_eq_refl tree_eq_sym
-             tree_eq_node tree_eq_node' tree_eq_node'' : combine.
+Variable f: option L.t -> option L.t -> option L.t.
+Hypothesis f_none_none: f None None = None.
 
-Inductive changed: Type := Unchanged | Changed (m: PTree.t L.t).
+Inductive changed : Type :=
+  | Same
+  | Same1
+  | Same2
+  | Changed (m: PTree.t L.t).
+
+Let Node_combine_l (l1: PTree.t L.t) (lres: changed) (o1: option L.t)
+                   (r1: PTree.t L.t) (rres: changed) : changed :=
+  let o' := f o1 None in
+  match lres, rres with
+  | Same1, Same1 =>
+      if opt_beq o' o1 then Same1 else Changed (PTree.Node l1 o' r1)
+  | Same1, Changed r' => Changed (PTree.Node l1 o' r')
+  | Changed l', Same1 => Changed (PTree.Node l' o' r1)
+  | Changed l', Changed r' => Changed (PTree.Node l' o' r')
+  | _, _ => Same (**r impossible cases *)
+  end.
 
-Fixpoint combine_l (m : PTree.t L.t) {struct m} : changed :=
-  match m with
-  | PTree.Leaf =>
-      Unchanged
-  | PTree.Node l o r =>
-      let o' := f o None in
-      match combine_l l, combine_l r with
-      | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r)
-      | Unchanged, Changed r' => Changed (PTree.Node' l o' r')
-      | Changed l', Unchanged => Changed (PTree.Node' l' o' r)
-      | Changed l', Changed r' => Changed (PTree.Node' l' o' r')
-      end
+Let xcombine_l (m: PTree.t L.t) : changed :=
+  PTree.tree_rec Same1 Node_combine_l m.
+
+Let Node_combine_r (l1: PTree.t L.t) (lres: changed) (o1: option L.t)
+                   (r1: PTree.t L.t) (rres: changed) : changed :=
+  let o' := f None o1 in
+  match lres, rres with
+  | Same2, Same2 =>
+      if opt_beq o' o1 then Same2 else Changed (PTree.Node l1 o' r1)
+  | Same2, Changed r' => Changed (PTree.Node l1 o' r')
+  | Changed l', Same2 => Changed (PTree.Node l' o' r1)
+  | Changed l', Changed r' => Changed (PTree.Node l' o' r')
+  | _, _ => Same (**r impossible cases *)
   end.
 
-Lemma combine_l_eq:
-  forall m,
-  tree_eq (match combine_l m with Unchanged => m | Changed m' => m' end)
-          (PTree.xcombine_l f m).
-Proof.
-  induction m; simpl.
-  auto with combine.
-  destruct (combine_l m1) as [ | l']; destruct (combine_l m2) as [ | r'];
-  auto with combine.
-  case_eq (opt_beq (f o None) o); auto with combine.
-Qed.
-
-Fixpoint combine_r (m : PTree.t L.t) {struct m} : changed :=
-  match m with
-  | PTree.Leaf =>
-      Unchanged
-  | PTree.Node l o r =>
-      let o' := f None o in
-      match combine_r l, combine_r r with
-      | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r)
-      | Unchanged, Changed r' => Changed (PTree.Node' l o' r')
-      | Changed l', Unchanged => Changed (PTree.Node' l' o' r)
-      | Changed l', Changed r' => Changed (PTree.Node' l' o' r')
+Let xcombine_r (m: PTree.t L.t) : changed :=
+  PTree.tree_rec Same2 Node_combine_r m.
+
+Let Node_combine_2
+             (l1: PTree.t L.t) (o1: option L.t) (r1: PTree.t L.t)
+             (l2: PTree.t L.t) (o2: option L.t) (r2: PTree.t L.t)
+             (lres: changed) (rres: changed) : changed :=
+  let o := f o1 o2 in
+  match lres, rres with
+  | Same, Same =>
+      match opt_beq o o1, opt_beq o o2 with
+      | true, true => Same
+      | true, false => Same1
+      | false, true => Same2
+      | false, false => Changed (PTree.Node l1 o r1)
       end
+  | Same, Same1
+  | Same1, Same
+  | Same1, Same1 =>
+      if opt_beq o o1 then Same1 else Changed (PTree.Node l1 o r1)
+  | Same, Same2
+  | Same2, Same
+  | Same2, Same2 =>
+      if opt_beq o o2 then Same2 else Changed (PTree.Node l2 o r2)
+  | Same, Changed m2 => Changed (PTree.Node l1 o m2)
+  | Same1, Same2 => Changed (PTree.Node l1 o r2)
+  | Same1, Changed m2 => Changed (PTree.Node l1 o m2)
+  | Same2, Same1 => Changed (PTree.Node l2 o r1)
+  | Same2, Changed m2 => Changed (PTree.Node l2 o m2)
+  | Changed m1, (Same|Same1) => Changed (PTree.Node m1 o r1)
+  | Changed m1, Same2 => Changed (PTree.Node m1 o r2)
+  | Changed m1, Changed m2 => Changed (PTree.Node m1 o m2)
   end.
 
-Lemma combine_r_eq:
-  forall m,
-  tree_eq (match combine_r m with Unchanged => m | Changed m' => m' end)
-          (PTree.xcombine_r f m).
+Definition xcombine :=
+  PTree.tree_rec2
+    Same
+    xcombine_r
+    xcombine_l
+    Node_combine_2.
+
+Definition tree_agree (m1 m2 m: PTree.t L.t) : Prop :=
+  forall i, opt_eq m!i (f m1!i m2!i).
+
+Lemma tree_agree_node: forall l1 o1 r1 l2 o2 r2 l o r,
+  tree_agree l1 l2 l -> tree_agree r1 r2 r -> opt_eq (f o1 o2) o ->
+  tree_agree (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2) (PTree.Node l o r).
 Proof.
-  induction m; simpl.
-  auto with combine.
-  destruct (combine_r m1) as [ | l']; destruct (combine_r m2) as [ | r'];
-  auto with combine.
-  case_eq (opt_beq (f None o) o); auto with combine.
+  intros; red; intros. rewrite ! PTree.gNode. destruct i; auto using opt_eq_sym.
 Qed.
 
-Inductive changed2 : Type :=
-  | Same
-  | Same1
-  | Same2
-  | CC(m: PTree.t L.t).
-
-Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 :=
-    match m1, m2 with
-    | PTree.Leaf, PTree.Leaf =>
-        Same
-    | PTree.Leaf, _ =>
-        match combine_r m2 with
-        | Unchanged => Same2
-        | Changed m => CC m
-        end
-    | _, PTree.Leaf =>
-        match combine_l m1 with
-        | Unchanged => Same1
-        | Changed m => CC m
-        end
-    | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
-        let o := f o1 o2 in
-        match xcombine l1 l2, xcombine r1 r2 with
-        | Same, Same =>
-            match opt_beq o o1, opt_beq o o2 with
-            | true, true => Same
-            | true, false => Same1
-            | false, true => Same2
-            | false, false => CC(PTree.Node' l1 o r1)
-            end
-        | Same1, Same | Same, Same1 | Same1, Same1 =>
-            if opt_beq o o1 then Same1 else CC(PTree.Node' l1 o r1)
-        | Same2, Same | Same, Same2 | Same2, Same2 =>
-            if opt_beq o o2 then Same2 else CC(PTree.Node' l2 o r2)
-        | Same1, Same2 => CC(PTree.Node' l1 o r2)
-        | (Same|Same1), CC r => CC(PTree.Node' l1 o r)
-        | Same2, Same1 => CC(PTree.Node' l2 o r1)
-        | Same2, CC r => CC(PTree.Node' l2 o r)
-        | CC l, (Same|Same1) => CC(PTree.Node' l o r1)
-        | CC l, Same2 => CC(PTree.Node' l o r2)
-        | CC l, CC r => CC(PTree.Node' l o r)
-        end
-    end.
+Local Hint Resolve tree_agree_node : combine.
 
-Lemma xcombine_eq:
-  forall m1 m2,
-  match xcombine m1 m2 with
-  | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2)
-  | Same1 => tree_eq m1 (PTree.combine f m1 m2)
-  | Same2 => tree_eq m2 (PTree.combine f m1 m2)
-  | CC m => tree_eq m (PTree.combine f m1 m2)
+Lemma gxcombine_l: forall m,
+  match xcombine_l m with
+  | Same1 => forall i, opt_eq m!i (f m!i None)
+  | Changed m' => forall i, opt_eq m'!i (f m!i None)
+  | _ => False
   end.
 Proof.
-Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r.
-  induction m1; destruct m2; simpl.
-  split; apply tree_eq_refl.
-  generalize (combine_r_eq (PTree.Node m2_1 o m2_2)).
-  destruct (combine_r (PTree.Node m2_1 o m2_2)); auto.
-  generalize (combine_l_eq (PTree.Node m1_1 o m1_2)).
-  destruct (combine_l (PTree.Node m1_1 o m1_2)); auto.
-  generalize (IHm1_1 m2_1) (IHm1_2 m2_2).
-  destruct (xcombine m1_1 m2_1);
-  destruct (xcombine m1_2 m2_2); auto with combine;
-  intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine.
+  unfold xcombine_l. induction m using PTree.tree_ind.
+- simpl; intros. rewrite PTree.gempty, f_none_none. auto.
+- rewrite PTree.unroll_tree_rec by auto.
+  destruct (PTree.tree_rec Same1 Node_combine_l l);
+  destruct (PTree.tree_rec Same1 Node_combine_l r);
+  try contradiction;
+  unfold Node_combine_l;
+  try (intros i; rewrite ! PTree.gNode; destruct i; auto with combine).
+  destruct (opt_beq (f o None) o) eqn:BEQ; intros i; rewrite ! PTree.gNode; destruct i; auto with combine.
+Qed.
+
+Lemma gxcombine_r: forall m,
+  match xcombine_r m with
+  | Same2 => forall i, opt_eq m!i (f None m!i)
+  | Changed m' => forall i, opt_eq m'!i (f None m!i)
+  | _ => False
+  end.
+Proof.
+  unfold xcombine_r. induction m using PTree.tree_ind.
+- simpl; intros. rewrite PTree.gempty, f_none_none. auto.
+- rewrite PTree.unroll_tree_rec by auto.
+  destruct (PTree.tree_rec Same2 Node_combine_r l);
+  destruct (PTree.tree_rec Same2 Node_combine_r r);
+  try contradiction;
+  unfold Node_combine_r;
+  try (intros i; rewrite ! PTree.gNode; destruct i; auto with combine).
+  destruct (opt_beq (f None o) o) eqn:BEQ; intros i; rewrite ! PTree.gNode; destruct i; auto with combine.
+Qed.
+
+Inductive xcombine_spec (m1 m2: PTree.t L.t) : changed -> Prop :=
+  | XCS_Same:
+      tree_agree m1 m2 m1 -> tree_agree m1 m2 m2 -> xcombine_spec m1 m2 Same
+  | XCS_Same1:
+      tree_agree m1 m2 m1 -> xcombine_spec m1 m2 Same1
+  | XCS_Same2:
+      tree_agree m1 m2 m2 -> xcombine_spec m1 m2 Same2
+  | XCS_Changed: forall m',
+      tree_agree m1 m2 m' -> xcombine_spec m1 m2 (Changed m').
+
+Local Hint Constructors xcombine_spec : combine.
+
+Lemma gxcombine: forall m1 m2, xcombine_spec m1 m2 (xcombine m1 m2).
+Proof.
+  Local Opaque opt_eq.
+  unfold xcombine.
+  induction m1 using PTree.tree_ind; induction m2 using PTree.tree_ind; intros.
+- constructor; red; intros; rewrite ! PTree.gEmpty, f_none_none; auto with combine.
+- rewrite PTree.unroll_tree_rec2_EN by auto. set (m2 := PTree.Node l o r).
+  generalize (gxcombine_r m2); destruct (xcombine_r m2); 
+  try contradiction; constructor; auto.
+- rewrite PTree.unroll_tree_rec2_NE by auto. set (m1 := PTree.Node l o r).
+  generalize (gxcombine_l m1); destruct (xcombine_l m1); 
+  try contradiction; constructor; auto.
+- rewrite PTree.unroll_tree_rec2_NN by auto.
+  clear IHm2 IHm3. specialize (IHm1 l0). specialize (IHm0 r0).
+  inv IHm1; inv IHm0; unfold Node_combine_2; auto with combine;
+  destruct (opt_beq (f o o0) o) eqn:E1; destruct (opt_beq (f o o0) o0) eqn:E2;
+  auto with combine.
 Qed.
 
 Definition combine (m1 m2: PTree.t L.t) : PTree.t L.t :=
   match xcombine m1 m2 with
   | Same|Same1 => m1
   | Same2 => m2
-  | CC m => m
+  | Changed m => m
   end.
 
-Lemma gcombine:
+Theorem gcombine:
   forall m1 m2 i, opt_eq (PTree.get i (combine m1 m2)) (f (PTree.get i m1) (PTree.get i m2)).
 Proof.
-  intros.
-  assert (tree_eq (combine m1 m2) (PTree.combine f m1 m2)).
-  unfold combine.
-  generalize (xcombine_eq m1 m2).
-  destruct (xcombine m1 m2); tauto.
-  eapply opt_eq_trans. apply H. rewrite PTree.gcombine; auto. apply opt_eq_refl.
+  intros. unfold combine. 
+  generalize (gxcombine m1 m2); intros XS; inv XS; auto.
 Qed.
 
 End COMBINE.
@@ -626,7 +620,7 @@ Definition top := Top_except (PTree.empty L.t).
 
 Lemma get_top: forall p, get p top = L.top.
 Proof.
-  unfold top; intros; simpl. rewrite PTree.gempty. auto.
+  unfold top; intros; auto.
 Qed.
 
 Lemma ge_top: forall x, ge top x.
diff --git a/lib/Maps.v b/lib/Maps.v
index c648af23..19d1fb5b 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -2,7 +2,8 @@
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*     Xavier Leroy and Damien Doligez, INRIA Paris-Rocquencourt       *)
+(*     Andrew W. Appel, Princeton University                           *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
@@ -33,7 +34,6 @@
   inefficient implementation of maps as functions is also provided.
 *)
 
-Require Import Equivalence EquivDec.
 Require Import Coqlib.
 
 (* To avoid useless definitions of inductors in extracted code. *)
@@ -65,14 +65,6 @@ Module Type TREE.
   Axiom 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.
-  Hypothesis grident:
-    forall (A: Type) (i: elt) (m: t A) (v: A),
-    get i m = None -> remove i m = m.
-  *)
   Axiom grs:
     forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
   Axiom gro:
@@ -117,19 +109,6 @@ Module Type TREE.
     forall (m1: t A) (m2: t B) (i: elt),
     get i (combine f m1 m2) = f (get i m1) (get i m2).
 
-  Parameter combine_null :
-    forall (A B C: Type) (f: A -> B -> option C),
-    t A -> t B -> t C.
-
-  Axiom gcombine_null:
-    forall (A B C: Type) (f: A -> B -> option C),
-    forall (m1: t A) (m2: t B) (i: elt),
-      get i (combine_null f m1 m2) =
-      match (get i m1), (get i m2) with
-      | (Some x1), (Some x2) => f x1 x2
-      | _, _ => None
-      end.
-
   (** Enumerating the bindings of a tree. *)
   Parameter elements:
     forall (A: Type), t A -> list (elt * A).
@@ -165,12 +144,6 @@ Module Type TREE.
     forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A),
     fold1 f m v =
     List.fold_left (fun a p => f a (snd p)) (elements m) v.
-
-  Parameter bempty_canon :
-    forall (A : Type), t A -> bool.
-  Axiom bempty_canon_correct:
-    forall (A : Type) (tr : t A) (i : elt),
-      bempty_canon tr = true -> get i tr = None.
 End TREE.
 
 (** * The abstract signatures of maps *)
@@ -206,111 +179,208 @@ Module PTree <: TREE.
   Definition elt := positive.
   Definition elt_eq := peq.
 
-  Inductive tree (A : Type) : Type :=
-    | Leaf : tree A
-    | Node : tree A -> option A -> tree A -> tree A.
+(** ** Representation of trees *)
 
-  Arguments Leaf {A}.
-  Arguments Node [A].
-  Scheme tree_ind := Induction for tree Sort Prop.
+(** The type [tree'] of nonempty trees.  Each constructor is of the form
+    [NodeXYZ], where the bit [X] says whether there is a left subtree,
+    [Y] whether there is a value at this node, and [Z] whether there is
+    a right subtree. *)
+
+  Inductive tree' (A: Type) : Type := 
+  | Node001: tree' A -> tree' A
+  | Node010: A -> tree' A
+  | Node011: A -> tree' A -> tree' A
+  | Node100: tree' A -> tree' A
+  | Node101: tree' A -> tree' A ->tree' A
+  | Node110: tree' A -> A -> tree' A
+  | Node111: tree' A -> A -> tree' A -> tree' A.
+
+  Inductive tree (A: Type) : Type := 
+  | Empty : tree A
+  | Nodes: tree' A -> tree A.
+
+  Arguments Node001 {A} _.
+  Arguments Node010 {A} _.
+  Arguments Node011 {A} _ _.
+  Arguments Node100 {A} _.
+  Arguments Node101 {A} _ _.
+  Arguments Node110 {A} _ _.
+  Arguments Node111 {A} _ _ _.
+
+  Arguments Empty {A}.
+  Arguments Nodes {A} _.
+
+  Scheme tree'_ind := Induction for tree' Sort Prop.
 
   Definition t := tree.
 
-  Definition empty (A : Type) := (Leaf : t A).
+  (** A smart constructor for type [tree]: given a (possibly empty)
+      left subtree, a (possibly absent) value, and a (possibly empty)
+      right subtree, it builds the corresponding tree. *)
+
+  Definition Node {A} (l: tree A) (o: option A) (r: tree A) : tree A := 
+    match l,o,r with
+    | Empty, None, Empty => Empty
+    | Empty, None, Nodes r' => Nodes (Node001 r')
+    | Empty, Some x, Empty => Nodes (Node010 x)
+    | Empty, Some x, Nodes r' => Nodes (Node011 x r')
+    | Nodes l', None, Empty => Nodes (Node100 l')
+    | Nodes l', None, Nodes r' => Nodes (Node101 l' r')
+    | Nodes l', Some x, Empty => Nodes (Node110 l' x)
+    | Nodes l', Some x, Nodes r' => Nodes (Node111 l' x r')
+    end.
 
-  Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
-    match m with
-    | Leaf => None
-    | Node l o r =>
-        match i with
-        | xH => o
-        | xO ii => get ii l
-        | xI ii => get ii r
-        end
+(** ** Basic operations: [empty], [get], [set], [remove] *)
+
+  Definition empty (A: Type) : t A := Empty.
+
+  Fixpoint get' {A} (p: positive) (m: tree' A) : option A :=
+    match p, m with
+    | xH, Node001 _ => None
+    | xH, Node010 x => Some x
+    | xH, Node011 x _ => Some x
+    | xH, Node100 _ => None
+    | xH, Node101 _ _ => None
+    | xH, Node110 _ x => Some x
+    | xH, Node111 _ x _ => Some x
+    | xO q, Node001 _ => None
+    | xO q, Node010 _ => None
+    | xO q, Node011 _ _ => None
+    | xO q, Node100 m' => get' q m'
+    | xO q, Node101 m' _ => get' q m'
+    | xO q, Node110 m' _ => get' q m'
+    | xO q, Node111 m' _ _ => get' q m'
+    | xI q, Node001 m' => get' q m'
+    | xI q, Node010 _ => None
+    | xI q, Node011 _ m' => get' q m'
+    | xI q, Node100 m' => None
+    | xI q, Node101 _ m' => get' q m'
+    | xI q, Node110 _ _ => None
+    | xI q, Node111 _ _ m' => get' q m'
     end.
 
-  Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A :=
+  Definition get {A} (p: positive) (m: tree A) : option A :=
     match m with
-    | Leaf =>
-        match i with
-        | xH => Node Leaf (Some v) Leaf
-        | xO ii => Node (set ii v Leaf) None Leaf
-        | xI ii => Node Leaf None (set ii v Leaf)
-        end
-    | Node l o r =>
-        match i with
-        | xH => Node l (Some v) r
-        | xO ii => Node (set ii v l) o r
-        | xI ii => Node l o (set ii v r)
-        end
+    | Empty => None
+    | Nodes m' => get' p m'
     end.
 
-  Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A :=
-    match i with
-    | xH =>
-        match m with
-        | Leaf => Leaf
-        | Node Leaf o Leaf => Leaf
-        | Node l o r => Node l None r
-        end
-    | xO ii =>
-        match m with
-        | Leaf => Leaf
-        | Node l None Leaf =>
-            match remove ii l with
-            | Leaf => Leaf
-            | mm => Node mm None Leaf
-            end
-        | Node l o r => Node (remove ii l) o r
-        end
-    | xI ii =>
-        match m with
-        | Leaf => Leaf
-        | Node Leaf None r =>
-            match remove ii r with
-            | Leaf => Leaf
-            | mm => Node Leaf None mm
-            end
-        | Node l o r => Node l o (remove ii r)
-        end
-    end.
+  (** [set0 p x] constructs the singleton tree that maps [p] to [x]
+      and has no other bindings. *)
+
+  Fixpoint set0 {A} (p: positive) (x: A) : tree' A :=
+  match p with
+  | xH => Node010 x
+  | xO q => Node100 (set0 q x)
+  | xI q => Node001 (set0 q x)
+  end.
+
+  Fixpoint set' {A} (p: positive) (x: A) (m: tree' A) : tree' A :=
+  match p, m with
+  | xH, Node001 r => Node011 x r
+  | xH, Node010 _ => Node010 x
+  | xH, Node011 _ r => Node011 x r
+  | xH, Node100 l => Node110 l x
+  | xH, Node101 l r => Node111 l x r
+  | xH, Node110 l _ => Node110 l x
+  | xH, Node111 l _ r => Node111 l x r
+  | xO q, Node001 r => Node101 (set0 q x) r
+  | xO q, Node010 y => Node110 (set0 q x) y
+  | xO q, Node011 y r => Node111 (set0 q x) y r
+  | xO q, Node100 l => Node100 (set' q x l)
+  | xO q, Node101 l r => Node101 (set' q x l) r
+  | xO q, Node110 l y => Node110 (set' q x l) y
+  | xO q, Node111 l y r => Node111 (set' q x l) y r
+  | xI q, Node001 r => Node001 (set' q x r)
+  | xI q, Node010 y => Node011 y (set0 q x)
+  | xI q, Node011 y r => Node011 y (set' q x r)
+  | xI q, Node100 l => Node101 l (set0 q x)
+  | xI q, Node101 l r => Node101 l (set' q x r)
+  | xI q, Node110 l y => Node111 l y (set0 q x)
+  | xI q, Node111 l y r => Node111 l y (set' q x r)
+  end.
+
+  Definition set {A} (p: positive) (x: A) (m: tree A) : tree A :=
+  match m with
+  | Empty => Nodes (set0 p x)
+  | Nodes m' => Nodes (set' p x m')
+  end.
+
+  (** Removal in a nonempty tree produces a possibly empty tree.
+      To simplify the code, we use the [Node] smart constructor in the
+      cases where the result can be empty or nonempty, depending on the
+      results of the recursive calls. *)
+
+  Fixpoint rem' {A} (p: positive) (m: tree' A) : tree A :=
+  match p, m with
+  | xH, Node001 r => Nodes m
+  | xH, Node010 _ => Empty
+  | xH, Node011 _ r => Nodes (Node001 r)
+  | xH, Node100 l => Nodes m
+  | xH, Node101 l r => Nodes m
+  | xH, Node110 l _ => Nodes (Node100 l)
+  | xH, Node111 l _ r => Nodes (Node101 l r)
+  | xO q, Node001 r => Nodes m
+  | xO q, Node010 y => Nodes m
+  | xO q, Node011 y r => Nodes m
+  | xO q, Node100 l => Node (rem' q l) None Empty
+  | xO q, Node101 l r => Node (rem' q l) None (Nodes r)
+  | xO q, Node110 l y => Node (rem' q l) (Some y) Empty
+  | xO q, Node111 l y r => Node (rem' q l) (Some y) (Nodes r)
+  | xI q, Node001 r => Node Empty None (rem' q r)
+  | xI q, Node010 y => Nodes m
+  | xI q, Node011 y r => Node Empty (Some y) (rem' q r)
+  | xI q, Node100 l => Nodes m
+  | xI q, Node101 l r => Node (Nodes l) None (rem' q r)
+  | xI q, Node110 l y => Nodes m
+  | xI q, Node111 l y r => Node (Nodes l) (Some y) (rem' q r)
+  end.
+
+  (** This use of [Node] causes some run-time overhead, which we eliminate
+      by partial evaluation within Coq. *)
+
+  Definition remove' := Eval cbv [rem' Node] in @rem'.
+
+  Definition remove {A} (p: positive) (m: tree A) : tree A :=
+  match m with
+  | Empty => Empty
+  | Nodes m' => remove' p m'
+  end.
+
+(** ** Good variable properties for the basic operations *)
 
   Theorem gempty:
     forall (A: Type) (i: positive), get i (empty A) = None.
-  Proof.
-    induction i; simpl; auto.
-  Qed.
+  Proof. reflexivity. Qed.
 
-  Definition bempty_canon (A : Type) (tr : t A) : bool :=
-    match tr with
-    | Leaf => true
-    | _ => false
-    end.
+  Lemma gEmpty:
+    forall (A: Type) (i: positive), get i (@Empty A) = None.
+  Proof. reflexivity. Qed.
 
-  Theorem gss:
-    forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
+  Lemma gss0: forall {A} p (x: A), get' p (set0 p x) = Some x.
+  Proof. induction p; simpl; auto. Qed.
+
+  Lemma gso0: forall {A} p q (x: A), p<>q -> get' p (set0 q x) = None.
   Proof.
-    induction i; destruct m; simpl; auto.
+    induction p; destruct q; simpl; intros; auto; try apply IHp; congruence.
   Qed.
 
-    Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None.
-    Proof. exact gempty. Qed.
-    
-  Lemma bempty_canon_correct:
-    forall (A : Type) (tr : t A) (i : elt),
-      bempty_canon tr = true -> get i tr = None.
+  Theorem gss:
+    forall (A: Type) (i: positive) (x: A) (m: tree A), get i (set i x m) = Some x.
   Proof.
-    destruct tr; intros.
-    - rewrite gleaf; trivial.
-    - discriminate.
+   intros. destruct m as [|m]; simpl.
+   - apply gss0.
+   - revert m; induction i; destruct m; simpl; intros; auto using gss0.
   Qed.
-  
+
   Theorem gso:
-    forall (A: Type) (i j: positive) (x: A) (m: t A),
+    forall (A: Type) (i j: positive) (x: A) (m: tree A),
     i <> j -> get i (set j x m) = get i m.
   Proof.
-    induction i; intros; destruct j; destruct m; simpl;
-       try rewrite <- (gleaf A i); auto; try apply IHi; congruence.
+   intros. destruct m as [|m]; simpl.
+   - apply gso0; auto.
+   - revert m j H; induction i; destruct j,m; simpl; intros; auto;
+     solve [apply IHi; congruence | apply gso0; congruence | congruence].
   Qed.
 
   Theorem gsspec:
@@ -321,72 +391,32 @@ Module PTree <: TREE.
     destruct (peq i j); [ rewrite e; apply gss | apply gso; auto ].
   Qed.
 
-  Theorem gsident:
-    forall (A: Type) (i: positive) (m: t A) (v: A),
-    get i m = Some v -> set i v m = m.
+  Lemma gNode:
+    forall {A} (i: positive) (l: tree A) (x: option A) (r: tree A),
+    get i (Node l x r) = match i with xH => x | xO j => get j l | xI j => get j r end.
   Proof.
-    induction i; intros; destruct m; simpl; simpl in H; try congruence.
-     rewrite (IHi m2 v H); congruence.
-     rewrite (IHi m1 v H); congruence.
+    intros. destruct l, x, r; simpl; auto; destruct i; auto.
   Qed.
 
-  Theorem set2:
-    forall (A: Type) (i: elt) (m: t A) (v1 v2: A),
-    set i v2 (set i v1 m) = set i v2 m.
-  Proof.
-    induction i; intros; destruct m; simpl; try (rewrite IHi); auto.
-  Qed.
-
-  Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.
-  Proof. destruct i; simpl; auto. Qed.
-
   Theorem grs:
-    forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None.
-  Proof.
-    induction i; destruct m.
-     simpl; auto.
-     destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto.
-      rewrite (rleaf A i); auto.
-      cut (get i (remove i (Node ll oo rr)) = None).
-        destruct (remove i (Node ll oo rr)); auto; apply IHi.
-        apply IHi.
-     simpl; auto.
-     destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto.
-      rewrite (rleaf A i); auto.
-      cut (get i (remove i (Node ll oo rr)) = None).
-        destruct (remove i (Node ll oo rr)); auto; apply IHi.
-        apply IHi.
-     simpl; auto.
-     destruct m1; destruct m2; simpl; auto.
+    forall (A: Type) (i: positive) (m: tree A), get i (remove i m) = None.
+  Proof.
+    Local Opaque Node.
+    destruct m as [ |m]; simpl. auto.
+    change (remove' i m) with (rem' i m).
+    revert m. induction i; destruct m; simpl; auto; rewrite gNode; auto.
   Qed.
 
   Theorem gro:
-    forall (A: Type) (i j: positive) (m: t A),
+    forall (A: Type) (i j: positive) (m: tree A),
     i <> j -> get i (remove j m) = get i m.
   Proof.
-    induction i; intros; destruct j; destruct m;
-        try rewrite (rleaf A (xI j));
-        try rewrite (rleaf A (xO j));
-        try rewrite (rleaf A 1); auto;
-        destruct m1; destruct o; destruct m2;
-        simpl;
-        try apply IHi; try congruence;
-        try rewrite (rleaf A j); auto;
-        try rewrite (gleaf A i); auto.
-     cut (get i (remove j (Node m2_1 o m2_2)) = get i (Node m2_1 o m2_2));
-        [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf A i); auto
-        | apply IHi; congruence ].
-     destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i);
-        auto.
-     destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i);
-        auto.
-     cut (get i (remove j (Node m1_1 o0 m1_2)) = get i (Node m1_1 o0 m1_2));
-        [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf A i); auto
-        | apply IHi; congruence ].
-     destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i);
-        auto.
-     destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i);
-        auto.
+    Local Opaque Node.
+    destruct m as [ |m]; simpl. auto.
+    change (remove' j m) with (rem' j m).
+    revert j m. induction i; destruct j, m; simpl; intros; auto;
+    solve [ congruence
+          | rewrite gNode; auto; apply IHi; congruence ].
   Qed.
 
   Theorem grspec:
@@ -396,47 +426,304 @@ Module PTree <: TREE.
     intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto.
   Qed.
 
+(** ** Custom case analysis principles and induction principles *)
+
+(** We can view trees as being of one of two (non-exclusive)
+    cases: either [Empty] for an empty tree, or [Node l o r] for a
+    nonempty tree, with [l] and [r] the left and right subtrees
+    and [o] an optional value.  The [Empty] constructor and the [Node]
+    smart function defined above provide one half of the view: the one
+    that lets us construct values of type [tree A].
+
+    We now define the other half of the view: the one that lets us
+    inspect and recurse over values of type [tree A].  This is achieved
+    by defining appropriate principles for case analysis and induction. *)
+
+  Definition not_trivially_empty {A} (l: tree A) (o: option A) (r: tree A) :=
+    match l, o, r with
+    | Empty, None, Empty => False
+    | _, _, _ => True
+    end.
+
+  (** A case analysis principle *)
+
+  Section TREE_CASE.
+
+  Context {A B: Type}
+          (empty: B)
+          (node: tree A -> option A -> tree A -> B).
+
+  Definition tree_case (m: tree A) : B :=
+    match m with
+    | Empty => empty
+    | Nodes (Node001 r) => node Empty None (Nodes r)
+    | Nodes (Node010 x) => node Empty (Some x) Empty
+    | Nodes (Node011 x r) => node Empty (Some x) (Nodes r)
+    | Nodes (Node100 l) => node (Nodes l) None Empty
+    | Nodes (Node101 l r) => node (Nodes l) None (Nodes r)
+    | Nodes (Node110 l x) => node (Nodes l) (Some x) Empty
+    | Nodes (Node111 l x r) => node (Nodes l) (Some x) (Nodes r)
+    end.
+
+  Lemma unroll_tree_case: forall l o r,
+    not_trivially_empty l o r ->
+    tree_case (Node l o r) = node l o r.
+  Proof.
+    destruct l, o, r; simpl; intros; auto. contradiction.
+  Qed.
+
+  End TREE_CASE.
+
+  (** A recursion principle *)
+
+  Section TREE_REC.
+
+  Context {A B: Type}
+          (empty: B)
+          (node: tree A -> B -> option A -> tree A -> B -> B).
+
+  Fixpoint tree_rec' (m: tree' A) : B :=
+    match m with
+    | Node001 r => node Empty empty None (Nodes r) (tree_rec' r)
+    | Node010 x => node Empty empty (Some x) Empty empty
+    | Node011 x r => node Empty empty (Some x) (Nodes r) (tree_rec' r)
+    | Node100 l => node (Nodes l) (tree_rec' l) None Empty empty
+    | Node101 l r => node (Nodes l) (tree_rec' l) None (Nodes r) (tree_rec' r)
+    | Node110 l x => node (Nodes l) (tree_rec' l) (Some x) Empty empty
+    | Node111 l x r => node (Nodes l) (tree_rec' l) (Some x) (Nodes r) (tree_rec' r)
+    end.
+
+  Definition tree_rec (m: tree A) : B :=
+    match m with
+    | Empty => empty
+    | Nodes m' => tree_rec' m'
+    end.
+
+  Lemma unroll_tree_rec: forall l o r,
+    not_trivially_empty l o r ->
+    tree_rec (Node l o r) = node l (tree_rec l) o r (tree_rec r).
+  Proof.
+    destruct l, o, r; simpl; intros; auto. contradiction.
+  Qed.
+
+  End TREE_REC.
+
+  (** A double recursion principle *)
+
+  Section TREE_REC2.
+
+  Context {A B C: Type}
+          (base: C)
+          (base1: tree B -> C) 
+          (base2: tree A -> C)
+          (nodes: forall (l1: tree A) (o1: option A) (r1: tree A)
+                         (l2: tree B) (o2: option B) (r2: tree B)
+                         (lrec: C) (rrec: C), C).
+
+  Fixpoint tree_rec2' (m1: tree' A) (m2: tree' B) : C.
+  Proof.
+    destruct m1 as [ r1 | x1 | x1 r1 | l1 | l1 r1 | l1 x1 | l1 x1 r1 ];
+    destruct m2 as [ r2 | x2 | x2 r2 | l2 | l2 r2 | l2 x2 | l2 x2 r2 ];
+    (apply nodes;
+    [ solve [ exact (Nodes l1) | exact Empty ]
+    | solve [ exact (Some x1)  | exact None ]
+    | solve [ exact (Nodes r1) | exact Empty ]
+    | solve [ exact (Nodes l2) | exact Empty ]
+    | solve [ exact (Some x2)  | exact None ]
+    | solve [ exact (Nodes r2) | exact Empty ]
+    | solve [ exact (tree_rec2' l1 l2) | exact (base2 (Nodes l1)) | exact (base1 (Nodes l2)) | exact base ]
+    | solve [ exact (tree_rec2' r1 r2) | exact (base2 (Nodes r1)) | exact (base1 (Nodes r2)) | exact base ]
+    ]).
+  Defined.
+
+  Definition tree_rec2 (a: tree A) (b: tree B) : C :=
+    match a, b with
+    | Empty, Empty => base
+    | Empty, _ => base1 b
+    | _, Empty => base2 a
+    | Nodes a', Nodes b' => tree_rec2' a' b'
+    end.
+
+  Lemma unroll_tree_rec2_NE:
+    forall l1 o1 r1,
+    not_trivially_empty l1 o1 r1 ->
+    tree_rec2 (Node l1 o1 r1) Empty = base2 (Node l1 o1 r1).
+  Proof.
+    intros. destruct l1, o1, r1; try contradiction; reflexivity.
+  Qed.
+
+  Lemma unroll_tree_rec2_EN:
+    forall l2 o2 r2,
+    not_trivially_empty l2 o2 r2 ->
+    tree_rec2 Empty (Node l2 o2 r2) = base1 (Node l2 o2 r2).
+  Proof.
+    intros. destruct l2, o2, r2; try contradiction; reflexivity.
+  Qed.
+
+  Lemma unroll_tree_rec2_NN:
+    forall l1 o1 r1 l2 o2 r2,
+    not_trivially_empty l1 o1 r1 -> not_trivially_empty l2 o2 r2 ->
+    tree_rec2 (Node l1 o1 r1) (Node l2 o2 r2) =
+    nodes l1 o1 r1 l2 o2 r2 (tree_rec2 l1 l2) (tree_rec2 r1 r2).
+  Proof.
+    intros.
+    destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction; reflexivity.
+  Qed.
+
+  End TREE_REC2.
+
+(** An induction principle *)
+
+  Section TREE_IND.
+
+  Context {A: Type} (P: tree A -> Type)
+          (empty: P Empty)
+          (node: forall l, P l -> forall o r, P r -> not_trivially_empty l o r ->
+                 P (Node l o r)).
+
+  Program Fixpoint tree_ind' (m: tree' A) : P (Nodes m) :=
+    match m with
+    | Node001 r => @node Empty empty None (Nodes r) (tree_ind' r) _
+    | Node010 x => @node Empty empty (Some x) Empty empty _
+    | Node011 x r => @node Empty empty (Some x) (Nodes r) (tree_ind' r) _
+    | Node100 l => @node (Nodes l) (tree_ind' l) None Empty empty _
+    | Node101 l r => @node (Nodes l) (tree_ind' l) None (Nodes r) (tree_ind' r) _
+    | Node110 l x => @node (Nodes l) (tree_ind' l) (Some x) Empty empty _
+    | Node111 l x r => @node (Nodes l) (tree_ind' l) (Some x) (Nodes r) (tree_ind' r) _
+    end.
+
+  Definition tree_ind (m: tree A) : P m :=
+    match m with
+    | Empty => empty
+    | Nodes m' => tree_ind' m'
+    end.
+
+  End TREE_IND.
+
+(** ** Extensionality property *)
+
+  Lemma tree'_not_empty:
+    forall {A} (m: tree' A), exists i, get' i m <> None.
+  Proof.
+   induction m; simpl; try destruct IHm as [p H].
+   - exists (xI p); auto.
+   - exists xH; simpl; congruence.
+   - exists xH; simpl; congruence.
+   - exists (xO p); auto.
+   - destruct IHm1 as [p H]; exists (xO p); auto.
+   - exists xH; simpl; congruence.
+   - exists xH; simpl; congruence.
+  Qed.
+
+  Corollary extensionality_empty:
+    forall {A} (m: tree A),
+    (forall i, get i m = None) -> m = Empty.
+  Proof.
+    intros. destruct m as [ | m]; auto. destruct (tree'_not_empty m) as [i GET].
+    elim GET. apply H.
+  Qed.
+
+  Theorem extensionality:
+    forall (A: Type) (m1 m2: tree A),
+    (forall i, get i m1 = get i m2) -> m1 = m2.
+  Proof.
+    intros A. induction m1 using tree_ind; induction m2 using tree_ind; intros.
+  - auto.
+  - symmetry. apply extensionality_empty. intros; symmetry; apply H0.
+  - apply extensionality_empty. apply H0.
+  - f_equal.
+    + apply IHm1_1. intros. specialize (H1 (xO i)); rewrite ! gNode in H1. auto.
+    + specialize (H1 xH); rewrite ! gNode in H1. auto.
+    + apply IHm1_2. intros. specialize (H1 (xI i)); rewrite ! gNode in H1. auto.
+  Qed.
+
+  (** Some consequences of extensionality *)
+
+  Theorem gsident:
+    forall {A} (i: positive) (m: t A) (v: A),
+    get i m = Some v -> set i v m = m.
+  Proof.
+    intros; apply extensionality; intros j.
+    rewrite gsspec. destruct (peq j i); congruence.
+  Qed.
+
+  Theorem set2:
+    forall {A} (i: elt) (m: t A) (v1 v2: A),
+    set i v2 (set i v1 m) = set i v2 m.
+  Proof.
+    intros; apply extensionality; intros j.
+    rewrite ! gsspec. destruct (peq j i); auto.
+  Qed.
+
+(** ** Boolean equality *)
+
   Section BOOLEAN_EQUALITY.
 
     Variable A: Type.
     Variable beqA: A -> A -> bool.
 
-    Fixpoint bempty (m: t A) : bool :=
-      match m with
-      | Leaf => true
-      | Node l None r => bempty l && bempty r
-      | Node l (Some _) r => false
-      end.
+    Fixpoint beq' (m1 m2: tree' A) {struct m1} : bool :=
+    match m1, m2 with
+    | Node001 r1, Node001 r2 => beq' r1 r2
+    | Node010 x1, Node010 x2 => beqA x1 x2
+    | Node011 x1 r1, Node011 x2 r2 => beqA x1 x2 && beq' r1 r2
+    | Node100 l1, Node100 l2 => beq' l1 l2
+    | Node101 l1 r1, Node101 l2 r2 => beq' l1 l2 && beq' r1 r2
+    | Node110 l1 x1, Node110 l2 x2 => beqA x1 x2 && beq' l1 l2
+    | Node111 l1 x1 r1, Node111 l2 x2 r2  => beqA x1 x2 && beq' l1 l2 && beq' r1 r2
+    | _, _ => false
+    end.
+
+    Definition beq (m1 m2: t A) : bool :=
+    match m1, m2 with
+    | Empty, Empty => true
+    | Nodes m1', Nodes m2' => beq' m1' m2'
+    | _, _ => false
+    end.
 
-    Fixpoint beq (m1 m2: t A) {struct m1} : bool :=
-      match m1, m2 with
-      | Leaf, _ => bempty m2
-      | _, Leaf => bempty m1
-      | Node l1 o1 r1, Node l2 o2 r2 =>
-          match o1, o2 with
-          | None, None => true
-          | Some y1, Some y2 => beqA y1 y2
-          | _, _ => false
-          end
-          && beq l1 l2 && beq r1 r2
+    Let beq_optA (o1 o2: option A) : bool :=
+      match o1, o2 with
+      | None, None => true
+      | Some a1, Some a2 => beqA a1 a2
+      | _, _ => false
       end.
 
-    Lemma bempty_correct:
-      forall m, bempty m = true <-> (forall x, get x m = None).
+    Lemma beq_correct_bool:
+      forall m1 m2,
+      beq m1 m2 = true <-> (forall x, beq_optA (get x m1) (get x m2) = true).
     Proof.
-      induction m; simpl.
-      split; intros. apply gleaf. auto.
-      destruct o; split; intros.
-      congruence.
-      generalize (H xH); simpl; congruence.
-      destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1.
-      destruct x; simpl; auto.
-      apply andb_true_intro; split.
-      apply IHm1. intros; apply (H (xO x)).
-      apply IHm2. intros; apply (H (xI x)).
+      Local Transparent Node.
+      assert (beq_NN: forall l1 o1 r1 l2 o2 r2,
+              not_trivially_empty l1 o1 r1 ->
+              not_trivially_empty l2 o2 r2 ->
+              beq (Node l1 o1 r1) (Node l2 o2 r2) =
+              beq l1 l2 && beq_optA o1 o2 && beq r1 r2).
+      { intros.
+        destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction;
+        simpl; rewrite ? andb_true_r, ? andb_false_r; auto.
+        rewrite andb_comm; auto.
+        f_equal; rewrite andb_comm; auto. }
+      induction m1 using tree_ind; [|induction m2 using tree_ind].
+    - intros. simpl; split; intros.
+      + destruct m2; try discriminate. simpl; auto.
+      + replace m2 with (@Empty A); auto. apply extensionality; intros x.
+        specialize (H x). destruct (get x m2); simpl; congruence.
+    - split; intros.
+      + destruct (Node l o r); try discriminate. simpl; auto.
+      + replace (Node l o r) with (@Empty A); auto. apply extensionality; intros x.
+        specialize (H0 x). destruct (get x (Node l o r)); simpl in *; congruence.
+    - rewrite beq_NN by auto. split; intros.
+      + InvBooleans. rewrite ! gNode. destruct x.
+        * apply IHm0; auto.
+        * apply IHm1; auto.
+        * auto.
+      + apply andb_true_intro; split; [apply andb_true_intro; split|].
+        * apply IHm1. intros. specialize (H1 (xO x)); rewrite ! gNode in H1; auto.
+        * specialize (H1 xH); rewrite ! gNode in H1; auto.
+        * apply IHm0. intros. specialize (H1 (xI x)); rewrite ! gNode in H1; auto.
     Qed.
 
-    Lemma beq_correct:
+    Theorem beq_correct:
       forall m1 m2,
       beq m1 m2 = true <->
       (forall (x: elt),
@@ -446,27 +733,15 @@ Module PTree <: TREE.
        | _, _ => False
        end).
     Proof.
-      induction m1; intros.
-    - simpl. rewrite bempty_correct. split; intros.
-      rewrite gleaf. rewrite H. auto.
-      generalize (H x). rewrite gleaf. destruct (get x m2); tauto.
-    - destruct m2.
-      + unfold beq. rewrite bempty_correct. split; intros.
-        rewrite H. rewrite gleaf. auto.
-        generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto.
-      + simpl. split; intros.
-        * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
-          rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
-          destruct x; simpl. apply H1. apply H3.
-          destruct o; destruct o0; auto || congruence.
-        * apply andb_true_intro. split. apply andb_true_intro. split.
-          generalize (H xH); simpl. destruct o; destruct o0; tauto.
-          apply IHm1_1. intros; apply (H (xO x)).
-          apply IHm1_2. intros; apply (H (xI x)).
+      intros. rewrite beq_correct_bool. unfold beq_optA. split; intros.
+    - specialize (H x). destruct (get x m1), (get x m2); intuition congruence.
+    - specialize (H x). destruct (get x m1), (get x m2); intuition auto.
     Qed.
 
   End BOOLEAN_EQUALITY.
 
+(** ** Collective operations *)
+
   Fixpoint prev_append (i j: positive) {struct i} : positive :=
     match i with
       | xH => j
@@ -498,78 +773,94 @@ Module PTree <: TREE.
     specialize (Hi _ _ H); congruence.
   Qed.
 
-    Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive)
-             {struct m} : t B :=
-      match m with
-      | Leaf => Leaf
-      | Node l o r => Node (xmap f l (xO i))
-                           (match o with None => None | Some x => Some (f (prev i) x) end)
-                           (xmap f r (xI i))
-      end.
+  Fixpoint map' {A B} (f: positive -> A -> B) (m: tree' A) (i: positive)
+           {struct m} : tree' B :=
+    match m with
+    | Node001 r => Node001 (map' f r (xI i))
+    | Node010 x => Node010 (f (prev i) x)
+    | Node011 x r => Node011 (f (prev i) x) (map' f r (xI i))
+    | Node100 l => Node100 (map' f l (xO i))
+    | Node101 l r => Node101 (map' f l (xO i)) (map' f r (xI i))
+    | Node110 l x => Node110 (map' f l (xO i)) (f (prev i) x)
+    | Node111 l x r => Node111 (map' f l (xO i)) (f (prev i) x) (map' f r (xI i))
+    end.
 
-  Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH.
+  Definition map {A B} (f: positive -> A -> B) (m: tree A) :=
+    match m with
+    | Empty => Empty
+    | Nodes m => Nodes (map' f m xH)
+    end.
 
-    Lemma xgmap:
-      forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
-      get i (xmap f m j) = option_map (f (prev (prev_append i j))) (get i m).
-    Proof.
-      induction i; intros; destruct m; simpl; auto.
-    Qed.
+  Lemma gmap':
+    forall {A B} (f: positive -> A -> B) (i j : positive) (m: tree' A),
+    get' i (map' f m j) = option_map (f (prev (prev_append i j))) (get' i m).
+  Proof.
+    induction i; intros; destruct m; simpl; auto.
+  Qed.
 
   Theorem gmap:
-    forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
+    forall {A B} (f: positive -> A -> B) (i: positive) (m: t A),
     get i (map f m) = option_map (f i) (get i m).
   Proof.
-    intros A B f i m.
-    unfold map.
-    rewrite xgmap. repeat f_equal. exact (prev_involutive i).
+    intros; destruct m as [|m]; simpl. auto. rewrite gmap'. repeat f_equal. exact (prev_involutive i).
   Qed.
 
-  Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B :=
+  Fixpoint map1' {A B} (f: A -> B) (m: tree' A) {struct m} : tree' B :=
     match m with
-    | Leaf => Leaf
-    | Node l o r => Node (map1 f l) (option_map f o) (map1 f r)
+    | Node001 r => Node001 (map1' f r)
+    | Node010 x => Node010 (f x)
+    | Node011 x r => Node011 (f x) (map1' f r)
+    | Node100 l => Node100 (map1' f l)
+    | Node101 l r => Node101 (map1' f l) (map1' f r)
+    | Node110 l x => Node110 (map1' f l) (f x)
+    | Node111 l x r => Node111 (map1' f l) (f x) (map1' f r)
+    end.
+
+  Definition map1 {A B} (f: A -> B) (m: t A) : t B :=
+    match m with
+    | Empty => Empty
+    | Nodes m => Nodes (map1' f m)
     end.
 
   Theorem gmap1:
-    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
+    forall {A B} (f: A -> B) (i: elt) (m: t A),
     get i (map1 f m) = option_map f (get i m).
   Proof.
-    induction i; intros; destruct m; simpl; auto.
+    intros. destruct m as [|m]; simpl. auto.
+    revert i; induction m; destruct i; simpl; auto.
   Qed.
 
-  Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A :=
-    match l, x, r with
-    | Leaf, None, Leaf => Leaf
-    | _, _, _ => Node l x r
-    end.
+  Definition map_filter1_nonopt {A B} (f: A -> option B) (m: tree A) : tree B :=
+    tree_rec
+      Empty
+      (fun l lrec o r rrec => Node lrec (match o with None => None | Some a => f a end) rrec)
+      m.
 
-  Lemma gnode':
-    forall (A: Type) (l r: t A) (x: option A) (i: positive),
-    get i (Node' l x r) = get i (Node l x r).
+  Local Transparent Node.
+
+  Definition map_filter1 :=
+    Eval cbv [map_filter1_nonopt tree_rec tree_rec' Node] in @map_filter1_nonopt.
+
+  Lemma gmap_filter1:
+    forall {A B} (f: A -> option B) (m: tree A) (i: positive),
+    get i (map_filter1 f m) = match get i m with None => None | Some a => f a end.
   Proof.
-    intros. unfold Node'.
-    destruct l; destruct x; destruct r; auto.
-    destruct i; simpl; auto; rewrite gleaf; auto.
+    change @map_filter1 with @map_filter1_nonopt. unfold map_filter1_nonopt.
+    intros until f. induction m using tree_ind; intros.
+  - auto.
+  - rewrite unroll_tree_rec by auto. rewrite ! gNode; destruct i; auto.
   Qed.
 
-  Fixpoint filter1 (A: Type) (pred: A -> bool) (m: t A) {struct m} : t A :=
-    match m with
-    | Leaf => Leaf
-    | Node l o r =>
-        let o' := match o with None => None | Some x => if pred x then o else None end in
-        Node' (filter1 pred l) o' (filter1 pred r)
-    end.
+  Definition filter1 {A} (pred: A -> bool) (m: t A) : t A :=
+    map_filter1 (fun a => if pred a then Some a else None) m.
 
   Theorem gfilter1:
-    forall (A: Type) (pred: A -> bool) (i: elt) (m: t A),
+    forall {A} (pred: A -> bool) (i: elt) (m: t A),
     get i (filter1 pred m) =
     match get i m with None => None | Some x => if pred x then Some x else None end.
   Proof.
-    intros until m. revert m i. induction m; simpl; intros.
-    rewrite gleaf; auto.
-    rewrite gnode'. destruct i; simpl; auto. destruct o; auto.
-  Qed.
+    intros. apply gmap_filter1.
+  Qed. 
 
   Section COMBINE.
 
@@ -577,275 +868,152 @@ Module PTree <: TREE.
   Variable f: option A -> option B -> option C.
   Hypothesis f_none_none: f None None = None.
 
-  Fixpoint xcombine_l (m : t A) {struct m} : t C :=
-      match m with
-      | Leaf => Leaf
-      | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r)
-      end.
+  Let combine_l := map_filter1 (fun a => f (Some a) None).
+  Let combine_r := map_filter1 (fun b => f None (Some b)).
 
-  Lemma xgcombine_l :
-          forall (m: t A) (i : positive),
-          get i (xcombine_l m) = f (get i m) None.
-    Proof.
-      induction m; intros; simpl.
-      repeat rewrite gleaf. auto.
-      rewrite gnode'. destruct i; simpl; auto.
-    Qed.
+  Let combine_nonopt (m1: tree A) (m2: tree B) : tree C :=
+    tree_rec2
+      Empty
+      combine_r
+      combine_l
+      (fun l1 o1 r1 l2 o2 r2 lrec rrec =>
+        Node lrec
+             (match o1, o2 with None, None => None | _, _ => f o1 o2 end)
+             rrec)
+      m1 m2.
 
-  Fixpoint xcombine_r (m : t B) {struct m} : t C :=
-      match m with
-      | Leaf => Leaf
-      | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r)
-      end.
+  Definition combine :=
+    Eval cbv [combine_nonopt tree_rec2 tree_rec2'] in combine_nonopt.
 
-  Lemma xgcombine_r :
-          forall (m: t B) (i : positive),
-          get i (xcombine_r m) = f None (get i m).
-    Proof.
-      induction m; intros; simpl.
-      repeat rewrite gleaf. auto.
-      rewrite gnode'. destruct i; simpl; auto.
-    Qed.
+  Lemma gcombine_l: forall m i, get i (combine_l m) = f (get i m) None.
+  Proof.
+    intros; unfold combine_l; rewrite gmap_filter1. destruct (get i m); auto.
+  Qed.
 
-  Fixpoint combine (m1: t A) (m2: t B) {struct m1} : t C :=
-    match m1 with
-    | Leaf => xcombine_r m2
-    | Node l1 o1 r1 =>
-        match m2 with
-        | Leaf => xcombine_l m1
-        | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2)
-        end
-    end.
+  Lemma gcombine_r: forall m i, get i (combine_r m) = f None (get i m).
+  Proof.
+    intros; unfold combine_r; rewrite gmap_filter1. destruct (get i m); auto.
+  Qed.
 
   Theorem gcombine:
       forall (m1: t A) (m2: t B) (i: positive),
       get i (combine m1 m2) = f (get i m1) (get i m2).
   Proof.
-    induction m1; intros; simpl.
-    rewrite gleaf. apply xgcombine_r.
-    destruct m2; simpl.
-    rewrite gleaf. rewrite <- xgcombine_l. auto.
-    repeat rewrite gnode'. destruct i; simpl; auto.
+    change combine with combine_nonopt.
+    induction m1 using tree_ind; induction m2 using tree_ind; intros.
+  - auto.
+  - unfold combine_nonopt; rewrite unroll_tree_rec2_EN by auto. apply gcombine_r.
+  - unfold combine_nonopt; rewrite unroll_tree_rec2_NE by auto. apply gcombine_l.
+  - unfold combine_nonopt; rewrite unroll_tree_rec2_NN by auto.
+    rewrite ! gNode; destruct i; auto. destruct o, o0; auto.
   Qed.
 
   End COMBINE.
 
-  Lemma xcombine_lr :
-    forall (A B: Type) (f g : option A -> option A -> option B) (m : t A),
-    (forall (i j : option A), f i j = g j i) ->
-    xcombine_l f m = xcombine_r g m.
-    Proof.
-      induction m; intros; simpl; auto.
-      rewrite IHm1; auto.
-      rewrite IHm2; auto.
-      rewrite H; auto.
-    Qed.
-
   Theorem combine_commut:
     forall (A B: Type) (f g: option A -> option A -> option B),
+    f None None = None -> g None None = None ->
     (forall (i j: option A), f i j = g j i) ->
     forall (m1 m2: t A),
     combine f m1 m2 = combine g m2 m1.
   Proof.
-    intros A B f g EQ1.
-    assert (EQ2: forall (i j: option A), g i j = f j i).
-      intros; auto.
-    induction m1; intros; destruct m2; simpl;
-      try rewrite EQ1;
-      repeat rewrite (xcombine_lr f g);
-      repeat rewrite (xcombine_lr g f);
-      auto.
-     rewrite IHm1_1.
-     rewrite IHm1_2.
-     auto.
+    intros. apply extensionality; intros i. rewrite ! gcombine by auto. auto.
   Qed.
 
-  Section COMBINE_NULL.
+(** ** List of all bindings *)
 
-  Variables A B C: Type.
-  Variable f: A -> B -> option C.
-
-  
-  Fixpoint combine_null (m1: t A) (m2: t B) {struct m1} : t C :=
-    match m1, m2 with
-    | (Node l1 o1 r1), (Node l2 o2 r2) =>
-      Node' (combine_null l1 l2)
-            (match o1, o2 with
-             | (Some x1), (Some x2) => f x1 x2
-             | _, _ => None
-             end)
-            (combine_null r1 r2)
-    | _, _ => Leaf
+  Fixpoint xelements' {A} (m : tree' A) (i: positive) (k: list (positive * A))
+                     {struct m} : list (positive * A) :=
+    match m with
+    | Node001 r => xelements' r (xI i) k
+    | Node010 x => (prev i, x) :: k
+    | Node011 x r => (prev i, x) :: xelements' r (xI i) k
+    | Node100 l => xelements' l (xO i) k
+    | Node101 l r => xelements' l (xO i) (xelements' r (xI i) k)
+    | Node110 l x => xelements' l (xO i) ((prev i, x)::k)
+    | Node111 l x r => xelements' l (xO i) ((prev i, x):: (xelements' r (xI i) k))
     end.
 
-  Theorem gcombine_null:
-      forall (m1: t A) (m2: t B) (i: positive),
-        get i (combine_null m1 m2) =
-        match (get i m1), (get i m2) with
-        | (Some x1), (Some x2) => f x1 x2
-        | _, _ => None
-        end.
-  Proof.
-    induction m1; intros; simpl.
-    - rewrite gleaf. rewrite gleaf.
-      reflexivity.
-    - destruct m2; simpl.
-      + rewrite gleaf. rewrite gleaf.
-        destruct get; reflexivity.
-      + rewrite gnode'.
-        destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial.
-  Qed.
-
-  End COMBINE_NULL.
-
-  Section REMOVE_TREE.
+  Definition elements {A} (m : t A) : list (positive * A) := 
+    match m with Empty => nil | Nodes m' => xelements' m' xH nil end.
 
-  Variables A B: Type.
+  Definition xelements {A} (m : t A) (i: positive) : list (positive * A) := 
+    match m with Empty => nil | Nodes m' => xelements' m' i nil end.
 
-  Fixpoint remove_t (m1: t A) (m2: t B) {struct m1} : t A :=
-    match m1, m2 with
-    | Leaf, _ | _, Leaf => m1
-    | (Node l1 o1 r1), (Node l2 o2 r2) =>
-      Node' (remove_t l1 l2)
-            (match o2 with
-             | Some _ => None
-             | None => o1
-             end)
-            (remove_t r1 r2)
-    end.
-
-  Theorem gremove_t:
-    forall m1 : t A,
-    forall m2 : t B,
-    forall i : positive,
-      get i (remove_t m1 m2) = match get i m2 with
-                               | None => get i m1
-                               | Some _ => None
-                               end.
-  Proof.
-    induction m1; intros; simpl.
-    - rewrite gleaf.
-      destruct get; reflexivity.
-    - destruct m2; simpl.
-      + rewrite gleaf.
-        reflexivity.
-      + rewrite gnode'.
-        destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial.
-  Qed.      
-  End REMOVE_TREE.
-  
-  Fixpoint xelements (A : Type) (m : t A) (i : positive)
-                       (k: list (positive * A)) {struct m}
-                       : list (positive * A) :=
-      match m with
-      | Leaf => k
-      | Node l None r =>
-          xelements l (xO i) (xelements r (xI i) k)
-      | Node l (Some x) r =>
-          xelements l (xO i)
-            ((prev i, x) :: xelements r (xI i) k)
-      end.
-
-  Definition elements (A: Type) (m : t A) := xelements m xH nil.
-
-  Remark xelements_append:
-    forall A (m: t A) i k1 k2,
-    xelements m i (k1 ++ k2) = xelements m i k1 ++ k2.
+  Lemma xelements'_append:
+    forall A (m: tree' A) i k1 k2,
+    xelements' m i (k1 ++ k2) = xelements' m i k1 ++ k2.
   Proof.
-    induction m; intros; simpl.
-  - auto.
-  - destruct o; rewrite IHm2; rewrite <- IHm1; auto.
+    induction m; intros; simpl; auto.
+  - f_equal; auto.
+  - rewrite IHm2, IHm1. auto.
+  - rewrite <- IHm. auto.
+  - rewrite IHm2, <- IHm1. auto.
   Qed.
 
-  Remark xelements_leaf:
-    forall A i, xelements (@Leaf A) i nil = nil.
+  Lemma xelements_Node:
+    forall A (l: tree A) (o: option A) (r: tree A) i,
+    xelements (Node l o r) i =
+       xelements l (xO i)
+    ++ match o with None => nil | Some v => (prev i, v) :: nil end
+    ++ xelements r (xI i).
   Proof.
-    intros; reflexivity.
+    Local Transparent Node.
+    intros; destruct l, o, r; simpl; rewrite <- ? xelements'_append; auto.
   Qed.
 
-  Remark xelements_node:
-    forall A (m1: t A) o (m2: t A) i,
-    xelements (Node m1 o m2) i nil =
-       xelements m1 (xO i) nil
-    ++ match o with None => nil | Some v => (prev i, v) :: nil end
-    ++ xelements m2 (xI i) nil.
+  Lemma xelements_correct:
+    forall A (m: tree A) i j v,
+    get i m = Some v -> In (prev (prev_append i j), v) (xelements m j).
   Proof.
-    intros. simpl. destruct o; simpl; rewrite <- xelements_append; auto.
+    intros A. induction m using tree_ind; intros.
+  - discriminate.
+  - rewrite xelements_Node, ! in_app. rewrite gNode in H0. destruct i.
+    + right; right. apply (IHm2 i (xI j)); auto.
+    + left. apply (IHm1 i (xO j)); auto.
+    + right; left. subst o. rewrite prev_append_prev. auto with coqlib.
   Qed.
 
-    Lemma xelements_incl:
-      forall (A: Type) (m: t A) (i : positive) k x,
-      In x k -> In x (xelements m i k).
-    Proof.
-      induction m; intros; simpl.
-      auto.
-      destruct o.
-      apply IHm1. simpl; right; auto.
-      auto.
-    Qed.
-
-    Lemma xelements_correct:
-      forall (A: Type) (m: t A) (i j : positive) (v: A) k,
-      get i m = Some v -> In (prev (prev_append i j), v) (xelements m j k).
-    Proof.
-      induction m; intros.
-       rewrite (gleaf A i) in H; congruence.
-       destruct o; destruct i; simpl; simpl in H.
-        apply xelements_incl. right. auto.
-        auto.
-        inv H. apply xelements_incl. left. reflexivity.
-        apply xelements_incl. auto.
-        auto.
-        inv H.
-    Qed.
-
   Theorem elements_correct:
-    forall (A: Type) (m: t A) (i: positive) (v: A),
+    forall A (m: t A) (i: positive) (v: A),
     get i m = Some v -> In (i, v) (elements m).
   Proof.
     intros A m i v H.
-    generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id.
+    generalize (xelements_correct m i xH H). rewrite prev_append_prev. auto.
   Qed.
 
   Lemma in_xelements:
-    forall (A: Type) (m: t A) (i k: positive) (v: A) ,
-    In (k, v) (xelements m i nil) ->
+    forall A (m: tree A) (i k: positive) (v: A) ,
+    In (k, v) (xelements m i) ->
     exists j, k = prev (prev_append j i) /\ get j m = Some v.
   Proof.
-    induction m; intros.
-  - rewrite xelements_leaf in H. contradiction.
-  - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]].
-    + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); auto.
-    + destruct o; simpl in P; intuition auto. inv H. exists xH; auto.
-    + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); auto.
+    intros A. induction m using tree_ind; intros.
+  - elim H.
+  - rewrite xelements_Node, ! in_app in H0. destruct H0 as [P | [P | P]].
+    + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); rewrite gNode; auto.
+    + destruct o; simpl in P; intuition auto. inv H0. exists xH; rewrite gNode; auto.
+    + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); rewrite gNode; auto.
   Qed.
 
   Theorem elements_complete:
-    forall (A: Type) (m: t A) (i: positive) (v: A),
+    forall A (m: t A) (i: positive) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
   Proof.
-    unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q).
+    intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q).
     rewrite prev_append_prev in P. change i with (prev_append 1 i) in P.
     exploit prev_append_inj; eauto. intros; congruence.
   Qed.
 
-  Definition xkeys (A: Type) (m: t A) (i: positive) :=
-    List.map (@fst positive A) (xelements m i nil).
+  Definition xkeys {A} (m: t A) (i: positive) := List.map fst (xelements m i).
 
-  Remark xkeys_leaf:
-    forall A i, xkeys (@Leaf A) i = nil.
-  Proof.
-    intros; reflexivity.
-  Qed.
-
-  Remark xkeys_node:
+  Lemma xkeys_Node:
     forall A (m1: t A) o (m2: t A) i,
     xkeys (Node m1 o m2) i =
        xkeys m1 (xO i)
     ++ match o with None => nil | Some v => prev i :: nil end
     ++ xkeys m2 (xI i).
   Proof.
-    intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto.
+    intros. unfold xkeys. rewrite xelements_Node, ! map_app. destruct o; auto.
   Qed.
 
   Lemma in_xkeys:
@@ -862,40 +1030,36 @@ Module PTree <: TREE.
     forall (A: Type) (m: t A) (i: positive),
     list_norepet (xkeys m i).
   Proof.
-    induction m; intros.
-  - rewrite xkeys_leaf; constructor.
-  - assert (NOTIN1: ~ In (prev i) (xkeys m1 (xO i))).
+    intros A; induction m using tree_ind; intros.
+  - constructor.
+  - assert (NOTIN1: ~ In (prev i) (xkeys l (xO i))).
     { red; intros. exploit in_xkeys; eauto. intros (j & EQ).
       rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. }
-    assert (NOTIN2: ~ In (prev i) (xkeys m2 (xI i))).
+    assert (NOTIN2: ~ In (prev i) (xkeys r (xI i))).
     { red; intros. exploit in_xkeys; eauto. intros (j & EQ).
       rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. }
-    assert (DISJ: forall x, In x (xkeys m1 (xO i)) -> In x (xkeys m2 (xI i)) -> False).
-    { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1).
-      exploit in_xkeys. eexact H0. intros (j2 & EQ2).
+    assert (DISJ: forall x, In x (xkeys l (xO i)) -> In x (xkeys r (xI i)) -> False).
+    { intros. exploit in_xkeys. eexact H0. intros (j1 & EQ1).
+      exploit in_xkeys. eexact H1. intros (j2 & EQ2).
       rewrite prev_append_prev in *. simpl in *. rewrite EQ2 in EQ1. apply prev_append_inj in EQ1. discriminate. }
-    rewrite xkeys_node. apply list_norepet_append. auto.
+    rewrite xkeys_Node. apply list_norepet_append. auto.
     destruct o; simpl; auto. constructor; auto.
-    red; intros. red; intros; subst y. destruct o; simpl in H0.
-    destruct H0. subst x. tauto. eauto. eauto.
+    red; intros. red; intros; subst y. destruct o; simpl in H1.
+    destruct H1. subst x. tauto. eauto. eauto.
   Qed.
 
   Theorem elements_keys_norepet:
-    forall (A: Type) (m: t A),
+    forall A (m: t A),
     list_norepet (List.map (@fst elt A) (elements m)).
   Proof.
     intros. apply (xelements_keys_norepet m xH).
   Qed.
 
   Remark xelements_empty:
-    forall (A: Type) (m: t A) i, (forall i, get i m = None) -> xelements m i nil = nil.
+    forall A (m: t A) i, (forall i, get i m = None) -> xelements m i = nil.
   Proof.
-    induction m; intros.
-    auto.
-    rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto.
-    generalize (H xH); simpl; congruence.
-    intros. apply (H (xI i0)).
-    intros. apply (H (xO i0)).
+    intros. replace m with (@Empty A). auto.
+    apply extensionality; intros. symmetry; auto.
   Qed.
 
   Theorem elements_canonical_order':
@@ -905,19 +1069,18 @@ Module PTree <: TREE.
       (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
       (elements m) (elements n).
   Proof.
-    intros until n. unfold elements. generalize 1%positive. revert m n.
-    induction m; intros.
-  - simpl. rewrite xelements_empty. constructor.
-    intros. specialize (H i). rewrite gempty in H. inv H; auto.
-  - destruct n as [ | n1 o' n2 ].
-  + rewrite (xelements_empty (Node m1 o m2)). simpl; constructor.
-    intros. specialize (H i). rewrite gempty in H. inv H; auto.
-  + rewrite ! xelements_node. repeat apply list_forall2_app.
-    apply IHm1. intros. apply (H (xO i)).
-    generalize (H xH); simpl; intros OR; inv OR.
-    constructor.
-    constructor. auto. constructor.
-    apply IHm2. intros. apply (H (xI i)).
+    intros until n.
+    change (elements m) with (xelements m xH). change (elements n) with (xelements n xH).
+    generalize 1%positive. revert m n.
+    induction m using tree_ind; [ | induction n using tree_ind]; intros until p; intros REL.
+  - replace n with (@Empty B). constructor.
+    apply extensionality; intros. specialize (REL i). simpl in *. inv REL; auto.
+  - replace (Node l o r) with (@Empty A). constructor.
+    apply extensionality; intros. specialize (REL i). simpl in *. inv REL; auto.
+  - rewrite ! xelements_Node. repeat apply list_forall2_app.
+    + apply IHm. intros. specialize (REL (xO i)). rewrite ! gNode in REL; auto.
+    + specialize (REL xH). rewrite ! gNode in REL. inv REL; constructor; auto using list_forall2_nil.
+    + apply IHm0. intros. specialize (REL (xI i)). rewrite ! gNode in REL; auto.
   Qed.
 
   Theorem elements_canonical_order:
@@ -941,57 +1104,48 @@ Module PTree <: TREE.
     (forall i, get i m = get i n) ->
     elements m = elements n.
   Proof.
-    intros.
-    exploit (@elements_canonical_order' _ _ (fun (x y: A) => x = y) m n).
-    intros. rewrite H. destruct (get i n); constructor; auto.
-    induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *.
-    destruct H0. congruence.
+    intros. replace n with m; auto. apply extensionality; auto.
   Qed.
 
   Lemma xelements_remove:
-    forall (A: Type) v (m: t A) i j,
+    forall A v (m: t A) i j,
     get i m = Some v ->
     exists l1 l2,
-    xelements m j nil = l1 ++ (prev (prev_append i j), v) :: l2
-    /\ xelements (remove i m) j nil = l1 ++ l2.
-  Proof.
-    induction m; intros.
-  - rewrite gleaf in H; discriminate.
-  - assert (REMOVE: xelements (remove i (Node m1 o m2)) j nil =
-                    xelements (match i with
-                               | xH => Node m1 None m2
-                               | xO ii => Node (remove ii m1) o m2
-                               | xI ii => Node m1 o (remove ii m2) end)
-                              j nil).
-    {
-      destruct i; simpl remove.
-      destruct m1; auto. destruct o; auto. destruct (remove i m2); auto.
-      destruct o; auto. destruct m2; auto. destruct (remove i m1); auto.
-      destruct m1; auto. destruct m2; auto.
-    }
-    rewrite REMOVE. destruct i; simpl in H.
-    + destruct (IHm2 i (xI j) H) as (l1 & l2 & EQ & EQ').
-      exists (xelements m1 (xO j) nil ++
+    xelements m j = l1 ++ (prev (prev_append i j), v) :: l2
+    /\ xelements (remove i m) j = l1 ++ l2.
+  Proof.
+    intros A; induction m using tree_ind; intros.
+  - discriminate.
+  - assert (REMOVE: remove i (Node l o r) =
+                    match i with
+                    | xH => Node l None r
+                    | xO ii => Node (remove ii l) o r
+                    | xI ii => Node l o (remove ii r)
+                    end).
+    { destruct l, o, r, i; reflexivity. }
+    rewrite gNode in H0. rewrite REMOVE. destruct i; rewrite ! xelements_Node.
+    + destruct (IHm0 i (xI j) H0) as (l1 & l2 & EQ & EQ').
+      exists (xelements l (xO j) ++
               match o with None => nil | Some x => (prev j, x) :: nil end ++
               l1);
       exists l2; split.
-      rewrite xelements_node, EQ, ! app_ass. auto.
-      rewrite xelements_node, EQ', ! app_ass. auto.
-    + destruct (IHm1 i (xO j) H) as (l1 & l2 & EQ & EQ').
+      rewrite EQ, ! app_ass. auto.
+      rewrite EQ', ! app_ass. auto.
+    + destruct (IHm i (xO j) H0) as (l1 & l2 & EQ & EQ').
       exists l1;
       exists (l2 ++
               match o with None => nil | Some x => (prev j, x) :: nil end ++
-              xelements m2 (xI j) nil);
+              xelements r (xI j));
       split.
-      rewrite xelements_node, EQ, ! app_ass. auto.
-      rewrite xelements_node, EQ', ! app_ass. auto.
-    + subst o. exists (xelements m1 (xO j) nil); exists (xelements m2 (xI j) nil); split.
-      rewrite xelements_node. rewrite prev_append_prev. auto.
-      rewrite xelements_node; auto.
+      rewrite EQ, ! app_ass. auto.
+      rewrite EQ', ! app_ass. auto.
+    + subst o. exists (xelements l (xO j)); exists (xelements r (xI j)); split.
+      rewrite prev_append_prev. auto.
+      auto.
   Qed.
 
   Theorem elements_remove:
-    forall (A: Type) i v (m: t A),
+    forall A i v (m: t A),
     get i m = Some v ->
     exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2.
   Proof.
@@ -999,72 +1153,75 @@ Module PTree <: TREE.
     rewrite prev_append_prev. auto.
   Qed.
 
-  Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B)
-                 (i: positive) (m: t A) (v: B) {struct m} : B :=
+(** ** Folding over a tree *)
+
+  Fixpoint fold' {A B} (f: B -> positive -> A -> B)
+                 (i: positive) (m: tree' A) (v: B) {struct m} : B :=
     match m with
-    | Leaf => v
-    | Node l None r =>
-        let v1 := xfold f (xO i) l v in
-        xfold f (xI i) r v1
-    | Node l (Some x) r =>
-        let v1 := xfold f (xO i) l v in
-        let v2 := f v1 (prev i) x in
-        xfold f (xI i) r v2
+    | Node001 r => fold' f (xI i) r v
+    | Node010 x => f v (prev i) x
+    | Node011 x r => fold' f (xI i) r (f v (prev i) x)
+    | Node100 l => fold' f (xO i) l v
+    | Node101 l r => fold' f (xI i) r (fold' f (xO i) l v)
+    | Node110 l x => f (fold' f (xO i) l v) (prev i) x
+    | Node111 l x r => fold' f (xI i) r (f (fold' f (xO i) l v) (prev i) x)
     end.
 
-  Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) :=
-    xfold f xH m v.
+  Definition fold {A B} (f: B -> positive -> A -> B) (m: t A) (v: B) :=
+   match m with Empty => v | Nodes m' => fold' f xH m' v end.
 
-  Lemma xfold_xelements:
-    forall (A B: Type) (f: B -> positive -> A -> B) m i v l,
-    List.fold_left (fun a p => f a (fst p) (snd p)) l (xfold f i m v) =
-    List.fold_left (fun a p => f a (fst p) (snd p)) (xelements m i l) v.
+  Lemma fold'_xelements':
+    forall A B (f: B -> positive -> A -> B) m i v l,
+    List.fold_left (fun a p => f a (fst p) (snd p)) l (fold' f i m v) =
+    List.fold_left (fun a p => f a (fst p) (snd p)) (xelements' m i l) v.
   Proof.
-    induction m; intros.
-    simpl. auto.
-    destruct o; simpl.
-    rewrite <- IHm1. simpl. rewrite <- IHm2. auto.
-    rewrite <- IHm1. rewrite <- IHm2. auto.
+    induction m; intros; simpl; auto.
+    rewrite <- IHm1, <- IHm2; auto.
+    rewrite <- IHm; auto.
+    rewrite <- IHm1. simpl. rewrite <- IHm2; auto.
   Qed.
 
   Theorem fold_spec:
-    forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A),
+    forall A B (f: B -> positive -> A -> B) (v: B) (m: t A),
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
   Proof.
-    intros. unfold fold, elements. rewrite <- xfold_xelements. auto.
+    intros. unfold fold, elements. destruct m; auto. rewrite <- fold'_xelements'. auto.
   Qed.
 
-  Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B :=
+  Fixpoint fold1' {A B} (f: B -> A -> B) (m: tree' A) (v: B) {struct m} : B :=
     match m with
-    | Leaf => v
-    | Node l None r =>
-        let v1 := fold1 f l v in
-        fold1 f r v1
-    | Node l (Some x) r =>
-        let v1 := fold1 f l v in
-        let v2 := f v1 x in
-        fold1 f r v2
+    | Node001 r => fold1' f r v
+    | Node010 x => f v x
+    | Node011 x r => fold1' f r (f v x)
+    | Node100 l => fold1' f l v
+    | Node101 l r => fold1' f r (fold1' f l v)
+    | Node110 l x => f (fold1' f l v) x
+    | Node111 l x r => fold1' f r (f (fold1' f l v) x)
     end.
 
-  Lemma fold1_xelements:
-    forall (A B: Type) (f: B -> A -> B) m i v l,
-    List.fold_left (fun a p => f a (snd p)) l (fold1 f m v) =
-    List.fold_left (fun a p => f a (snd p)) (xelements m i l) v.
+
+  Definition fold1 {A B} (f: B -> A -> B) (m: t A) (v: B) : B :=
+    match m with Empty => v | Nodes m' => fold1' f m' v end.
+
+  Lemma fold1'_xelements':
+    forall A B (f: B -> A -> B) m i v l,
+    List.fold_left (fun a p => f a (snd p)) l (fold1' f m v) =
+    List.fold_left (fun a p => f a (snd p)) (xelements' m i l) v.
   Proof.
-    induction m; intros.
-    simpl. auto.
-    destruct o; simpl.
-    rewrite <- IHm1. simpl. rewrite <- IHm2. auto.
+    induction m; simpl; intros; auto.
     rewrite <- IHm1. rewrite <- IHm2. auto.
+    rewrite <- IHm. auto. 
+    rewrite <- IHm1. simpl. rewrite <- IHm2. auto.
   Qed.
 
   Theorem fold1_spec:
-    forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A),
+    forall A B (f: B -> A -> B) (v: B) (m: t A),
     fold1 f m v =
     List.fold_left (fun a p => f a (snd p)) (elements m) v.
   Proof.
-    intros. apply fold1_xelements with (l := @nil (positive * A)).
+    intros. destruct m as [|m]. reflexivity.
+    apply fold1'_xelements' with (l := @nil (positive * A)).
   Qed.
 
   Local Open Scope positive.
@@ -1072,8 +1229,23 @@ Module PTree <: TREE.
     forall (A: Type)(i d : elt) (m: t A)  (x y: A),
       set (i + d) y (set i x m) = set i x (set (i + d) y m).
   Proof.
-    induction i; destruct d; destruct m; intro; simpl; trivial;
-      intro; congruence.
+    intros.
+    apply extensionality.
+    intro j.
+    destruct (peq j i) as [EQ_i_j | NEQ_j_i].
+    - subst i.
+      rewrite gss.
+      rewrite gso by lia.
+      apply gss.
+    - rewrite (gso _ _ NEQ_j_i).
+      destruct (peq j (i + d)) as [EQ | NEQ].
+      + subst j.
+        rewrite gss.
+        rewrite gss.
+        reflexivity.
+      + rewrite (gso _ _ NEQ).
+        rewrite (gso _ _ NEQ).
+        apply (gso _ _ NEQ_j_i).
   Qed.
   
   Local Open Scope positive.
@@ -1097,6 +1269,11 @@ Module PTree <: TREE.
       symmetry.
       apply set_disjoint1.
   Qed.
+
+  Arguments empty A : simpl never.
+  Arguments get {A} p m : simpl never.
+  Arguments set {A} p x m : simpl never.
+  Arguments remove {A} p m : simpl never.
 End PTree.
 
 (** * An implementation of maps over type [positive] *)
@@ -1122,7 +1299,7 @@ Module PMap <: MAP.
   Theorem gi:
     forall (A: Type) (i: positive) (x: A), get i (init x) = x.
   Proof.
-    intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto.
+    intros. reflexivity.
   Qed.
 
   Theorem gss:
@@ -1441,6 +1618,8 @@ Module ZTree := ITree(ZIndexed).
 
 (** * Additional properties over trees *)
 
+Require Import Equivalence EquivDec.
+
 Module Tree_Properties(T: TREE).
 
 (** Two induction principles over [fold]. *)
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index c10b8ac2..b3895768 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -419,8 +419,7 @@ Lemma transfer_regs_dead inputs rs r:
   ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef.
 Proof.
   unfold transfer_regs; induction inputs; simpl; intuition subst.
-  - rewrite Regmap.gi; auto.
-  - rewrite Regmap.gso; auto.
+  rewrite Regmap.gso; auto.
 Qed.
 
 Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t :=
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index cf35abad..9b48c7d2 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -380,7 +380,7 @@ Global Opaque hSstore.
 Local Hint Resolve hSstore_correct: wlp.
 
 Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
-   match PTree.get r hrs with
+   match PTree.get r (ris_sreg hrs) with
    | None => if ris_input_init hrs then hSinput r else hSundef
    | Some sv => RET sv
    end.
@@ -629,15 +629,15 @@ Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval :=
   match (ris_input_init hrs), sv with
   | true, Sinput r' _ =>
       if Pos.eq_dec r r' 
-      then PTree.remove r' hrs
-      else PTree.set r sv hrs
+      then PTree.remove r' (ris_sreg hrs)
+      else PTree.set r sv (ris_sreg hrs)
   | false, Sundef _ =>
-      PTree.remove r hrs
-  | _, _ => PTree.set r sv hrs
+      PTree.remove r (ris_sreg hrs)
+  | _, _ => PTree.set r sv (ris_sreg hrs)
   end.
 
 Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx:
-  sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0).
+  sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv (ris_sreg hrs))) r0).
 Proof.
   unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl.
   destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto.
@@ -703,10 +703,8 @@ Lemma hrs_init_correct:
 Proof.
   unfold hrs_init, sis_init; wlp_simplify.
   econstructor; simpl in *; eauto.
-  + split; destruct 1; econstructor; simpl in *;
+  split; destruct 1; econstructor; simpl in *;
     try rewrite H; try congruence; trivial.
-  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
-    intros; rewrite PTree.gempty; eauto.
 Qed.
 Local Hint Resolve hrs_init_correct: wlp.
 Global Opaque hrs_init.
@@ -879,8 +877,7 @@ Proof.
       - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption.
       - rewrite OK_EQUIV; constructor; inv X; assumption.
     * intros X; inv X; simpl; apply MEM_EQ; constructor; auto.
-    * simpl. unfold ris_sreg_get.
-      intros;rewrite PTree.gempty. simpl; auto.
+    * simpl. unfold ris_sreg_get. auto.
   + constructor.
     * erewrite ok_hrset_red_sreg; eauto.
       inv H2. rewrite <- OK_EQUIV.
@@ -1244,23 +1241,63 @@ Qed.
 Global Opaque option_eq_check.
 Hint Resolve option_eq_check_correct:wlp.
 
-Import PTree.
+Import PTree.                           
+
+Fixpoint PTree_eq_check' {A} (d1 d2: PTree.tree' A): ?? unit :=
+  DO phy <~ phys_eq d1 d2;;
+  if phy
+  then
+    RET tt
+  else
+    match d1, d2 with
+    | Node001 r1, Node001 r2 => PTree_eq_check' r1 r2
+    | Node010 x1, Node010 x2 =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ"
+    | Node011 x1 r1, Node011 x2 r2 =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
+        PTree_eq_check' r1 r2
+    | Node100 l1, Node100 l2 => PTree_eq_check' l1 l2
+    | Node101 l1 r1, Node101 l2 r2 =>
+        PTree_eq_check' l1 l2 ;;
+        PTree_eq_check' r1 r2
+    | Node110 l1 x1, Node110 l2 x2 =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
+        PTree_eq_check' l1 l2
+    | Node111 l1 x1 r1, Node111 l2 x2 r2  =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
+        PTree_eq_check' l1 l2 ;;
+        PTree_eq_check' r1 r2
+    | _, _ => FAILWITH "PTree_eq_check': different shapes"
+    end.
 
-Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
+Lemma PTree_eq_check'_correct A : forall (d1 d2: PTree.tree' A),
+    WHEN PTree_eq_check' d1 d2 ~> _ THEN d1 = d2.
+Proof.
+  induction d1; destruct d2; cbn; wlp_simplify; try congruence.
+Qed.
+                                    
+Definition PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
   match d1, d2 with
-  | Leaf, Leaf => RET tt
-  | Node l1 o1 r1, Node l2 o2 r2 =>
-      option_eq_check o1 o2;;
-      PTree_eq_check l1 l2;;
-      PTree_eq_check r1 r2
-  | _, _ => FAILWITH "PTree_eq_check: some key is absent"
+  | Empty, Empty => RET tt
+  | Nodes m1, Nodes m2 => PTree_eq_check' m1 m2
+  | _, _ => FAILWITH "PTree_eq_check: empty vs nonempty"
   end.
 
+Lemma PTree_eq_check_correct' A : forall (d1 d2: PTree.tree A),
+    WHEN PTree_eq_check d1 d2 ~> _ THEN d1 = d2.
+Proof.
+  Local Hint Resolve PTree_eq_check'_correct: wlp.
+  destruct d1 as [ | m1]; destruct d2 as [ | m2]; cbn; wlp_simplify.
+  congruence.
+Qed.                                    
+
 Lemma PTree_eq_check_correct A d1: forall (d2: t A),
  WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2.
 Proof.
-  induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; 
-  wlp_simplify. destruct x; simpl; auto.
+  Local Hint Resolve PTree_eq_check_correct': wlp.
+  intros.
+  wlp_simplify.
+  congruence.
 Qed.
 Global Opaque PTree_eq_check.
 Local Hint Resolve PTree_eq_check_correct: wlp.
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index d47e53b8..51b562c7 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -32,10 +32,11 @@ Record ristate :=
   }.
 
 Definition ris_sreg_get (ris: ristate) r: sval :=
-   match PTree.get r ris with
+   match PTree.get r (ris_sreg ris) with
    | None => if ris_input_init ris then fSinput r else fSundef
    | Some sv => sv
    end.
+
 Coercion ris_sreg_get: ristate >-> Funclass.
 
 Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate :=
@@ -479,10 +480,8 @@ Lemma ris_init_correct ctx:
   ris_refines ctx ris_init sis_init.
 Proof.
   unfold ris_init, sis_init; econstructor; simpl in *; eauto.
-  + split; destruct 1; econstructor; simpl in *; eauto.
+  split; destruct 1; econstructor; simpl in *; eauto.
     congruence.
-  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
-    intros; rewrite PTree.gempty; eauto.
 Qed.
 
 Definition rset_smem rm (ris:ristate): ristate :=
@@ -655,8 +654,6 @@ Proof.
   + econstructor; eauto.
     * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
     * erewrite ok_transfer_ris; eauto.
-    * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto.
-      intros; rewrite PTree.gempty. simpl; auto.
   + econstructor; eauto.
     * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
     * erewrite ok_transfer_ris; simpl.
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 55afc19a..b0765f09 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -122,9 +122,9 @@ with eval_smem ctx (sm: smem): option mem :=
 
 (** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. 
     Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block
-   (their semantics only depends on the initial memory of the block).
+    (their semantics only depends on the initial memory of the block).
 
-   The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq].
+    The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq].
 *)
 Lemma valid_pointer_preserv ctx sm:
   forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs.
@@ -308,31 +308,31 @@ Proof.
 Qed.
 
 Lemma eval_builtin_sval_arg ctx bs:
-   forall ba m v, 
-   eval_builtin_sval ctx bs = Some ba ->
-   eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
-   eval_builtin_sarg ctx m bs v.
+  forall ba m v, 
+  eval_builtin_sval ctx bs = Some ba ->
+  eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
+  eval_builtin_sarg ctx m bs v.
 Proof.
-   induction bs; simpl; 
-   try (intros ba m v H; inversion H; subst; clear H;
-        intros H; inversion H; subst;
-        econstructor; auto; fail).
-   - intros ba m v; destruct (eval_sval _ _) eqn: SV;
-     intros H; inversion H; subst; clear H.
-     intros H; inversion H; subst.
-     econstructor; auto.
-   - intros ba m v. 
-     destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence.
-     destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence.
-     intros H; inversion H; subst; clear H.
-     intros H; inversion H; subst.
-     econstructor; eauto.
-   - intros ba m v. 
-     destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence.
-     destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence.
-     intros H; inversion H; subst; clear H.
-     intros H; inversion H; subst.
-     econstructor; eauto.
+  induction bs; simpl; 
+  try (intros ba m v H; inversion H; subst; clear H;
+       intros H; inversion H; subst;
+       econstructor; auto; fail).
+  - intros ba m v; destruct (eval_sval _ _) eqn: SV;
+    intros H; inversion H; subst; clear H.
+    intros H; inversion H; subst.
+    econstructor; auto.
+  - intros ba m v. 
+    destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence.
+    destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence.
+    intros H; inversion H; subst; clear H.
+    intros H; inversion H; subst.
+    econstructor; eauto.
+  - intros ba m v. 
+    destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence.
+    destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence.
+    intros H; inversion H; subst; clear H.
+    intros H; inversion H; subst.
+    econstructor; eauto.
 Qed.
 
 Lemma eval_builtin_sarg_sval ctx m v: forall bs,