Commit ff55c0a7 authored by Björn Brandenburg's avatar Björn Brandenburg

replace_at does not need decidable equality

parent e1426920
......@@ -9,7 +9,7 @@ Section ReplaceAtFacts.
Context {Job : JobType}.
(** ... and any given type of processor states, ... *)
Context {PState: eqType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(** ...consider any given reference schedule. *)
......
......@@ -9,7 +9,7 @@ Section SwappedFacts.
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... any given type of processor states: *)
Context {PState: eqType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(** ...consider any given reference schedule. *)
......
......@@ -9,7 +9,7 @@ Section ReplaceAt.
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... any given type of processor states, ... *)
Context {PState: eqType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(** ...consider any given reference schedule. *)
......@@ -35,7 +35,7 @@ Section Swapped.
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... any given type of processor states, ... *)
Context {PState: eqType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(** ...consider any given reference schedule. *)
......
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