Commit aae110fd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix Coq 8.5 build.

parent 3eec2de1
......@@ -937,7 +937,7 @@ Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
Proof.
split.
- induction 1; simpl; auto.
- induction l; intros []; subst; constructor; auto.
- induction l; destruct 1; subst; constructor; auto.
Qed.
Inductive NoDup {A} : list A Prop :=
......
Supports Markdown
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