Make to_mach_int more precise.

f508c521 · Jacques-Henri Jourdan · c1b55ac7 · f508c521
Commit f508c521 authored Nov 16, 2018 by Jacques-Henri Jourdan
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

lang.v theories/heap_lang/lang.v +1 -1

No files found.
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -42,7 +42,7 @@ Definition mach_int :=
  {n : Z | bool_decide (mach_int_bounded n) }%Z.

 Definition to_mach_int (n : Z) : option mach_int :=
-  match decide _ with
+  match decide (bool_decide (mach_int_bounded n)) with
  | left H => Some (n ↾ H)
  | right _ => None
  end.