Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.

6 files changed, 36 insertions, 39 deletions

diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 26953479..a8d79c3f 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -168,8 +168,7 @@ Proof.
 + subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto.
   intros. destruct H5. eapply ma_memval; eauto.
   eapply Mem.perm_storebytes_2; eauto.
-  apply H1; auto.
-+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. apply H1; auto.
++ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
 - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0).
   rewrite (Mem.nextblock_storebytes _ _ _ _ _ ST2).
   eapply ma_nextblock; eauto.
@@ -551,7 +550,7 @@ Proof.
   intros. exploit analyze_successors; eauto. rewrite ANPC; simpl. intros [A B].
   econstructor; eauto.
   eapply eagree_ge; eauto.
-  eapply magree_monotone; eauto. intros; apply B; auto.
+  eapply magree_monotone; eauto.
 Qed.
 
 (** Builtin arguments and results *)
@@ -1134,5 +1133,3 @@ Proof.
 Qed.
 
 End PRESERVATION.
-
-
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 23770cb7..f56d6d18 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -512,7 +512,7 @@ Proof.
     assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega.
     omega.
     intros. simpl in H. rewrite S1.
-    transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
+    transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega.
     eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega.
   red; simpl. subst s2; simpl in *. xomega.
   red; simpl. split. auto. apply align_le. apply min_alignment_pos.
@@ -542,7 +542,7 @@ Proof.
     assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega.
     omega.
     intros. simpl in H. rewrite S1.
-    transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
+    transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
     eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega.
   red; simpl.
 subst s2; simpl in *; xomega.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index 87090f5d..a2b49d56 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -74,7 +74,7 @@ Module Type DATAFLOW_SOLVER.
     point. [transf] is the transfer function, [ep] the entry point,
     and [ev] the minimal abstract value for [ep]. *)
 
-  Variable fixpoint:
+  Parameter fixpoint:
     forall {A: Type} (code: PTree.t A) (successors: A -> list positive)
            (transf: positive -> L.t -> L.t)
            (ep: positive) (ev: L.t),
@@ -83,7 +83,7 @@ Module Type DATAFLOW_SOLVER.
   (** The [fixpoint_solution] theorem shows that the returned solution,
     if any, satisfies the dataflow inequations. *)
 
-  Hypothesis fixpoint_solution:
+  Axiom fixpoint_solution:
     forall A (code: PTree.t A) successors transf ep ev res n instr s,
     fixpoint code successors transf ep ev = Some res ->
     code!n = Some instr -> In s (successors instr) ->
@@ -93,7 +93,7 @@ Module Type DATAFLOW_SOLVER.
   (** The [fixpoint_entry] theorem shows that the returned solution,
     if any, satisfies the additional constraint over the entry point. *)
 
-  Hypothesis fixpoint_entry:
+  Axiom fixpoint_entry:
     forall A (code: PTree.t A) successors transf ep ev res,
     fixpoint code successors transf ep ev = Some res ->
     L.ge res!!ep ev.
@@ -102,7 +102,7 @@ Module Type DATAFLOW_SOLVER.
       and that holds for [L.bot] also holds for the results of
       the analysis. *)
 
-  Hypothesis fixpoint_invariant:
+  Axiom fixpoint_invariant:
     forall A (code: PTree.t A) successors transf ep ev
            (P: L.t -> Prop),
     P L.bot ->
@@ -124,23 +124,23 @@ End DATAFLOW_SOLVER.
 
 Module Type NODE_SET.
 
-  Variable t: Type.
-  Variable empty: t.
-  Variable add: positive -> t -> t.
-  Variable pick: t -> option (positive * t).
-  Variable all_nodes: forall {A: Type}, PTree.t A -> t.
+  Parameter t: Type.
+  Parameter empty: t.
+  Parameter add: positive -> t -> t.
+  Parameter pick: t -> option (positive * t).
+  Parameter all_nodes: forall {A: Type}, PTree.t A -> t.
 
-  Variable In: positive -> t -> Prop.
-  Hypothesis empty_spec:
+  Parameter In: positive -> t -> Prop.
+  Axiom empty_spec:
     forall n, ~In n empty.
-  Hypothesis add_spec:
+  Axiom add_spec:
     forall n n' s, In n' (add n s) <-> n = n' \/ In n' s.
-  Hypothesis pick_none:
+  Axiom pick_none:
     forall s n, pick s = None -> ~In n s.
-  Hypothesis pick_some:
+  Axiom pick_some:
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
-  Hypothesis all_nodes_spec:
+  Axiom all_nodes_spec:
     forall A (code: PTree.t A) n instr,
     code!n = Some instr -> In n (all_nodes code).
 
@@ -900,7 +900,7 @@ Module Type BACKWARD_DATAFLOW_SOLVER.
     is a finite map returning the list of successors of the given program
     point. [transf] is the transfer function. *)
 
-  Variable fixpoint:
+  Parameter fixpoint:
     forall {A: Type} (code: PTree.t A) (successors: A -> list positive)
            (transf: positive -> L.t -> L.t),
     option (PMap.t L.t).
@@ -908,7 +908,7 @@ Module Type BACKWARD_DATAFLOW_SOLVER.
   (** The [fixpoint_solution] theorem shows that the returned solution,
     if any, satisfies the backward dataflow inequations. *)
 
-  Hypothesis fixpoint_solution:
+  Axiom fixpoint_solution:
     forall A (code: PTree.t A) successors transf res n instr s,
     fixpoint code successors transf = Some res ->
     code!n = Some instr -> In s (successors instr) ->
@@ -918,12 +918,12 @@ Module Type BACKWARD_DATAFLOW_SOLVER.
   (** [fixpoint_allnodes] is a variant of [fixpoint], less algorithmically
     efficient, but correct without any hypothesis on the transfer function. *)
 
-  Variable fixpoint_allnodes:
+  Parameter fixpoint_allnodes:
     forall {A: Type} (code: PTree.t A) (successors: A -> list positive)
            (transf: positive -> L.t -> L.t),
     option (PMap.t L.t).
 
-  Hypothesis fixpoint_allnodes_solution:
+  Axiom fixpoint_allnodes_solution:
     forall A (code: PTree.t A) successors transf res n instr s,
     fixpoint_allnodes code successors transf = Some res ->
     code!n = Some instr -> In s (successors instr) ->
@@ -1089,11 +1089,11 @@ End Backward_Dataflow_Solver.
 
 Module Type ORDERED_TYPE_WITH_TOP.
 
-  Variable t: Type.
-  Variable ge: t -> t -> Prop.
-  Variable top: t.
-  Hypothesis top_ge: forall x, ge top x.
-  Hypothesis refl_ge: forall x, ge x x.
+  Parameter t: Type.
+  Parameter ge: t -> t -> Prop.
+  Parameter top: t.
+  Axiom top_ge: forall x, ge top x.
+  Axiom refl_ge: forall x, ge x x.
 
 End ORDERED_TYPE_WITH_TOP.
 
@@ -1105,24 +1105,24 @@ Module Type BBLOCK_SOLVER.
 
   Declare Module L: ORDERED_TYPE_WITH_TOP.
 
-  Variable fixpoint:
+  Parameter fixpoint:
     forall {A: Type} (code: PTree.t A) (successors: A -> list positive)
            (transf: positive -> L.t -> L.t)
            (entrypoint: positive),
     option (PMap.t L.t).
 
-  Hypothesis fixpoint_solution:
+  Axiom fixpoint_solution:
     forall A (code: PTree.t A) successors transf entrypoint res n instr s,
     fixpoint code successors transf entrypoint = Some res ->
     code!n = Some instr -> In s (successors instr) ->
     L.ge res!!s (transf n res!!n).
 
-  Hypothesis fixpoint_entry:
+  Axiom fixpoint_entry:
     forall A (code: PTree.t A) successors transf entrypoint res,
     fixpoint code successors transf entrypoint = Some res ->
     res!!entrypoint = L.top.
 
-  Hypothesis fixpoint_invariant:
+  Axiom fixpoint_invariant:
     forall A (code: PTree.t A) successors transf entrypoint
            (P: L.t -> Prop),
     P L.top ->
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index aad3add4..a57e5ea6 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -865,9 +865,9 @@ Qed.
 Remark match_call_cont_cont:
   forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'.
 Proof.
-  intros. refine (let cunit : Cminor.program := _ in _). 
+  intros. simple refine (let cunit : Cminor.program := _ in _).
   econstructor. apply nil. apply nil. apply xH.
-  refine (let hf : helper_functions := _ in _).
+  simple refine (let hf : helper_functions := _ in _).
   econstructor; apply xH.
   exists cunit, hf; auto.
 Qed.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index da024a25..0e9c58b3 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1585,7 +1585,7 @@ Lemma find_function_translated:
   /\ Genv.find_funct_ptr tge bf = Some tf
   /\ transf_fundef f = OK tf.
 Proof.
-  intros until f; intros AG [bound [_ []]] FF.
+  intros until f; intros AG [bound [_ [?????]]] FF.
   destruct ros; simpl in FF.
 - exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF.
   rewrite Genv.find_funct_find_funct_ptr in FF.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 3c80d733..bc09c3dc 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -3739,7 +3739,7 @@ Proof.
 - (* contents *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
   rewrite Zplus_0_r.
-  set (mv := ZMap.get ofs (Mem.mem_contents m)#b1).
+  set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))).
   assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)).
   {
     Local Transparent Mem.loadbytes.