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

missed another warning

parent dbeafa69
Pipeline #9215 passed with stage
in 12 minutes and 30 seconds
......@@ -14,6 +14,7 @@
From Coq Require Import Wf_nat Omega.
From stdpp Require Export tactics base relations list collections.
From stdpp Require set.
Require ClassicalEpsilon.
(** * Definitions *)
Section definitions.
......@@ -1000,7 +1001,7 @@ Section cofair.
Qed.
Section erasure.
Require Import ClassicalEpsilon.
Import ClassicalEpsilon.
Context (erasure: A B).
Context (enabled_reflecting: i a, enabled R2 (erasure a) i enabled R1 a i).
Context (estep_dec: `(HR: R1 i a b), {R2 i (erasure a) (erasure b)} +
......@@ -1337,7 +1338,7 @@ Section cofair.
End erasure.
Section block.
Import stdpp.set.
Import stdpp.set ClassicalEpsilon.
Context (flatten: A B * (nat set nat)).
Context (flatten_spec_step:
i a a', R1 i a a'
......
Supports Markdown
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