Assorted cleanups, esp. to avoid generating _rec and _rect recursors in

submodules.  (Extraction does not remove them, then.)  
common/Switch: replaced use of FMaps by our own Maps.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 17 insertions, 12 deletions

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d426440..3d9f499 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -53,6 +53,23 @@ Local Open Scope error_monad_scope.
 
 Set Implicit Arguments.
 
+(** Auxiliary function for initialization of global variables. *)
+
+Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
+  if zle n 0 then Some m else
+    match Mem.store Mint8unsigned m b p Vzero with
+    | Some m' => store_zeros m' b (p + 1) (n - 1)
+    | None => None
+    end.
+Proof.
+  intros. red. omega.
+  apply Zwf_well_founded.
+Qed.
+
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Module Genv.
 
 (** * Global environments *)
@@ -486,18 +503,6 @@ Proof.
   destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega.
 Qed.
 
-Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
-  if zle n 0 then Some m else
-    let n' := n - 1 in
-    match Mem.store Mint8unsigned m b p Vzero with
-    | Some m' => store_zeros m' b (p + 1) n'
-    | None => None
-    end.
-Proof.
-  intros. red. omega.
-  apply Zwf_well_founded.
-Qed.
-
 Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
   match id with
   | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)