Commit 64df895f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Declare scope is not supported in Coq < 8.10.

parent 53f94fa4
......@@ -83,7 +83,6 @@ Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
CoInductive buffer : Type :=
Buf_cons { buf_head : token; buf_tail : buffer }.
Declare Scope buffer_scope.
Delimit Scope buffer_scope with buf.
Bind Scope buffer_scope with buffer.
......
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