Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 1adddd7c authored by POTTIER Francois's avatar POTTIER Francois
Browse files

coq-menhirlib: Add a comment about compatibility with Coq 8.12.0.

parent a03be248
No related branches found
No related tags found
No related merge requests found
Pipeline #192416 passed
......@@ -83,6 +83,9 @@ Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
CoInductive buffer : Type :=
Buf_cons { buf_head : token; buf_tail : buffer }.
(* Note: Coq 8.12.0 wants a Declare Scope command,
but this breaks compatibility with Coq < 8.10.
Declare Scope buffer_scope. *)
Delimit Scope buffer_scope with buf.
Bind Scope buffer_scope with buffer.
......
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