Commit d34bd413 authored by Pierre Roux's avatar Pierre Roux

Remove superfluous variable

parent b9d255ec
......@@ -15,7 +15,7 @@ Module Job.
Variable j: Job.
(* The job cost must be positive. *)
Definition job_cost_positive (j: Job) := job_cost j > 0.
Definition job_cost_positive := job_cost j > 0.
End ValidJob.
......@@ -90,4 +90,4 @@ Module Job.
End ValidTaskJob.
End Job.
\ No newline at end of file
End Job.
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