Commit d3d60c41 authored by Heiko Becker's avatar Heiko Becker

Update development to Coq 8.6

parent 7f633e09
......@@ -29,10 +29,10 @@ fi
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
8.5pl2)
;;
8.6)
;;
*)
echo "Error: Need Coq 8.5pl2"
echo "Error: Need 8.6"
exit 1
esac
echo "Found Coq version $coq_ver."
......
......@@ -136,8 +136,8 @@ Proof.
case_eq (n =? y); try auto.
intros n_eq_y.
rewrite Nat.eqb_eq in n_eq_y.
subst.
rewrite n_eq_y in H5.
rewrite n_eq_x in n_eq_y.
rewrite <- n_eq_y in y_free.
rewrite <- NatSet.mem_spec in y_free.
rewrite y_free in H5. inversion H5.
- intros n_neq_x.
......
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