diff options
Diffstat (limited to 'x86_64/Archi.v')
| -rw-r--r-- | x86_64/Archi.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/x86_64/Archi.v b/x86_64/Archi.v index 7b1136c8..7b5301df 100644 --- a/x86_64/Archi.v +++ b/x86_64/Archi.v @@ -31,7 +31,7 @@ Definition splitlong := negb ptr64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. Proof. - unfold splitlong. destruct ptr64; simpl; congruence. + unfold splitlong. destruct ptr64; simpl; congruence. Qed. Program Definition default_pl_64 : bool * nan_pl 53 := |