Skip to content
Snippets Groups Projects
Verified Commit de8e08df authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Fix ssreflect warning on Coq 8.10

Since Coq 8.10, `move => {}e` means `move => {e}e`.
For the backward-compatible syntax and discussion, see
https://github.com/coq/coq/issues/10550#issuecomment-542397265.
parent 4f3eb1ac
No related branches found
No related tags found
No related merge requests found
...@@ -81,7 +81,7 @@ Module bi_reflection. Section bi_reflection. ...@@ -81,7 +81,7 @@ Module bi_reflection. Section bi_reflection.
Lemma flatten_cancel e e' ns : Lemma flatten_cancel e e' ns :
cancel ns e = Some e' flatten e ns ++ flatten e'. cancel ns e = Some e' flatten e ns ++ flatten e'.
Proof. Proof.
rewrite /cancel fmap_Some=> -[{e'}e' [He ->]]; rewrite flatten_prune. rewrite /cancel fmap_Some=> -[{e'}-e' [He ->]]; rewrite flatten_prune.
revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto. revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto.
rewrite Permutation_middle -flatten_cancel_go //; eauto. rewrite Permutation_middle -flatten_cancel_go //; eauto.
Qed. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment