Commit b847a459 authored by Heiko Becker's avatar Heiko Becker

Fix compilation of ErrorValidationAA

parent ba79642d
......@@ -3200,14 +3200,9 @@ Proof.
cbn in Hiv.
now rewrite Rabs_Rle_condition.
<<<<<<< HEAD
- (* FIXME *)
- admit.
>>>>>>> master
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
match c with
| Let m x e k =>
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