Commit b860d761 authored by Joachim Bard's avatar Joachim Bard

Removing unnecessary 'Admitted.'

parent 316bad71
......@@ -3074,7 +3074,7 @@ Proof.
- apply validErrorboundAA_sound_fma; auto.
- apply validErrorboundAA_sound_downcast; auto.
- admit.
Admitted.
Abort.
Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
(forall e' : FloverMap.key,
......@@ -3200,7 +3200,7 @@ Proof.
cbn in Hiv.
now rewrite Rabs_Rle_condition.
- admit.
Admitted.
Abort.
(*
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
......@@ -3817,4 +3817,4 @@ Proof.
cbn in H12.
now rewrite Rabs_Rle_condition.
Qed.
*)
\ No newline at end of file
*)
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