Commit dbeafa69 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix more warnings

parent 30506849
Pipeline #9214 passed with stage
in 12 minutes and 45 seconds
......@@ -13,6 +13,7 @@
From Coq Require Import Wf_nat Omega.
From stdpp Require Export tactics base relations list collections.
From stdpp Require set.
(** * Definitions *)
Section definitions.
......@@ -979,7 +980,7 @@ Section cofair.
Lemma co_se_trace_valid {x1} {e: trace R1 x1} {x2} (ST: co_se_trace e x2):
co_se e (co_se_trace_extract ST).
Proof.
revert x1 e x2 ST; cofix; intros.
revert x1 e x2 ST; cofix COFIX; intros.
destruct ST; subst.
unfold co_se_trace_extract.
rewrite trace_aux_id; simpl.
......@@ -1336,7 +1337,7 @@ Section cofair.
End erasure.
Section block.
From stdpp Require Export set.
Import stdpp.set.
Context (flatten: A B * (nat set nat)).
Context (flatten_spec_step:
i a a', R1 i a a'
......
......@@ -2,6 +2,8 @@ From Coq.ssr Require Export ssreflect.
From fri.prelude Require Export list compact.
From stdpp Require Export prelude mapset.
From stdpp Require Export set natmap fin_collections collections fin_maps.
From stdpp Require set.
From Coq Require Classical_Pred_Type.
Lemma subseteq_union_decompose:
(A B C: natset), A B C B' C', B' B C' C A B' C'.
......@@ -131,8 +133,7 @@ Qed.
Section compact_setoid.
From stdpp Require Import set.
From Coq Require Import Classical_Pred_Type.
Import stdpp.set Classical_Pred_Type.
Definition set_finite_setoid `{Equiv A} {B} {H : ElemOf A B} (X : B) : Prop :=
l : list A, x : A, x X x' : A, x x' x' l.
......
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