Skip to content
Snippets Groups Projects
Commit d5a2f2c7 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

minor fix: remove erroneous coqdoc formatting syntax

parent 19120a32
No related branches found
No related tags found
No related merge requests found
......@@ -71,8 +71,8 @@ Section CompletionFacts.
Qed.
(** Consequently, if we have a have processor model where scheduled jobs
* necessarily receive service, we can conclude that scheduled jobs have
* remaining positive cost. *)
necessarily receive service, we can conclude that scheduled jobs have
remaining positive cost. *)
(** Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment