From d8231d65c2714c682ab68dad4c1a540f875c60b9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Nov 2019 12:23:31 +0100
Subject: [PATCH] No longer use `Declare Scope` since it does not work in Coq
8.9.
---
_CoqProject | 2 ++
theories/logic/model.v | 1 -
theories/typing/types.v | 1 -
3 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 271fa04..50b5c06 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,8 @@
-arg -w -arg -convert_concl_no_check
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
+# "Declare Scope" does not exist yet in 8.9.
+-arg -w -arg -undeclared-scope
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
diff --git a/theories/logic/model.v b/theories/logic/model.v
index ffa2377..057ce90 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -18,7 +18,6 @@ Record lrel Σ := LRel {
}.
Arguments LRel {_} _%I {_}.
Arguments lrel_car {_} _ _ _ : simpl never.
-Declare Scope lrel_scope.
Bind Scope lrel_scope with lrel.
Delimit Scope lrel_scope with lrel.
Existing Instance lrel_persistent.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index d5722e9..ecc67ba 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -51,7 +51,6 @@ Fixpoint binop_bool_res_type (op : bin_op) : option type :=
| _ => None
end.
-Declare Scope FType_scope.
Delimit Scope FType_scope with ty.
Bind Scope FType_scope with type.
Infix "*" := TProd : FType_scope.
--
GitLab