From 2cccb81243c5b2f45085634ffe070adc1ebb0c1b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 11:43:40 +0200 Subject: Do not use "Declare Scope", introduced in Coq 8.10 only --- MenhirLib/Interpreter.v | 1 - 1 file changed, 1 deletion(-) diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v index c36ca614..07aeae5a 100644 --- a/MenhirLib/Interpreter.v +++ b/MenhirLib/Interpreter.v @@ -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. -- cgit