Commit 5a4efb25 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix compilation on Coq 8.3.

parent 8b5baf03
......@@ -19,7 +19,7 @@ Proof.
intros a a_WT l.
induction l.
easy.
change (1 + length l = Z.of_nat (S (List.length l)))%Z.
change (1 + length l = Z_of_nat (S (List.length l)))%Z.
now rewrite inj_S, Zplus_comm, IHl.
Qed.
......@@ -39,6 +39,7 @@ Proof.
intros a a_WT [|h t] ; split ; try easy.
unfold length. fold length.
intros H.
exfalso.
generalize (Length_nonnegative t).
omega.
Qed.
......
......@@ -19,6 +19,8 @@ easy.
simpl.
generalize (Zeq_bool_if (i + 1) 0).
case Zeq_bool.
intro H.
exfalso.
omega.
intros _.
simpl in h1.
......
......@@ -41,6 +41,7 @@ generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros H'.
rewrite H' in H.
exfalso.
generalize (Length.Length_nonnegative q).
omega.
intros _.
......
......@@ -49,6 +49,7 @@ simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros Hi'.
exfalso.
generalize (Length.Length_nonnegative l1).
omega.
intros _.
......
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