Commit f7b4fa56 authored by Ralf Jung's avatar Ralf Jung

fix Proof Using warnings

parent 17eb4ec8
...@@ -442,13 +442,11 @@ End fixpointK. ...@@ -442,13 +442,11 @@ End fixpointK.
(** Mutual fixpoints *) (** Mutual fixpoints *)
Section fixpointAB. Section fixpointAB.
Local Unset Default Proof Using.
Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}. Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
Context (fA : A B A). Context (fA : A B A).
Context (fB : A B B). Context (fB : A B B).
Context `{ n, Proper (dist_later n ==> dist n ==> dist n) fA}. Context {fA_contractive : n, Proper (dist_later n ==> dist n ==> dist n) fA}.
Context `{ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}. Context {fB_contractive : n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x). Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB. Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
...@@ -459,7 +457,7 @@ Section fixpointAB. ...@@ -459,7 +457,7 @@ Section fixpointAB.
Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x). Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x).
Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA. Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
Proof. solve_contractive. Qed. Proof using fA_contractive. solve_contractive. Qed.
Definition fixpoint_A : A := fixpoint fixpoint_AA. Definition fixpoint_A : A := fixpoint fixpoint_AA.
Definition fixpoint_B : B := fixpoint_AB fixpoint_A. Definition fixpoint_B : B := fixpoint_AB fixpoint_A.
...@@ -470,11 +468,11 @@ Section fixpointAB. ...@@ -470,11 +468,11 @@ Section fixpointAB.
Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed. Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.
Instance: Proper (() ==> () ==> ()) fA. Instance: Proper (() ==> () ==> ()) fA.
Proof. Proof using fA_contractive.
apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S. apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
Qed. Qed.
Instance: Proper (() ==> () ==> ()) fB. Instance: Proper (() ==> () ==> ()) fB.
Proof. Proof using fB_contractive.
apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S. apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
Qed. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment