Port to Coq 8.5pl2

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

1 files changed, 28 insertions, 28 deletions

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 ->