Commit efd82c63 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove FIXME, it is due to a Set Printing all above.

parent 15c368d5
......@@ -9,14 +9,10 @@ Module LangTests.
Proof. intros; do_step done. Qed.
Definition rec_app : expr := (rec:: #0 #1) (Lit 0).
Goal σ, prim_step rec_app σ rec_app σ None.
Proof. Set Printing All. intros; do_step done. Qed.
Proof. intros; do_step done. Qed.
Definition lam : expr := λ: #0 + Lit 21.
Goal σ, prim_step (lam (Lit 21)) σ add σ None.
Proof.
(* FIXME WTF why does it print all the "S (S (S..."?? *)
rewrite /lam /Lam.
intros; do_step done.
Qed.
Proof. rewrite /lam /Lam. intros; do_step done. Qed.
End LangTests.
Module LiftingTests.
......
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