From d19b7d235be035d7aa0f948365c6285f275d7796 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sat, 5 Sep 2020 11:02:45 +0200 Subject: [PATCH] test Coq 8.12.0 and deny warnings --- .gitlab-ci.yml | 4 ++-- README.md | 2 +- theories/typing/lft_contexts.v | 1 + theories/typing/type.v | 1 + 4 files changed, 5 insertions(+), 3 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 26e177f0..1dad2e95 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -27,10 +27,10 @@ variables: ## Build jobs -build-coq.8.12.dev: +build-coq.8.12.0: <<: *template variables: - OPAM_PINS: "coq version 8.12.dev" + OPAM_PINS: "coq version 8.12.0" build-coq.8.11.2: <<: *template diff --git a/README.md b/README.md index d566a24e..9c3f4160 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ This is the Coq development accompanying RBrlx. This version is known to compile with: - - Coq 8.11.2 + - Coq 8.11.2 / 8.12.0 - A development version of [GPFSL]. The easiest way to install the correct versions of the dependencies is through diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v index 055af496..73c7c8df 100644 --- a/theories/typing/lft_contexts.v +++ b/theories/typing/lft_contexts.v @@ -8,6 +8,7 @@ Set Default Proof Using "Type". Definition elctx_elt : Type := lft * lft. Notation elctx := (list elctx_elt). +Declare Scope lrust_elctx_scope. Delimit Scope lrust_elctx_scope with EL. (* We need to define [elctx] and [llctx] as notations to make eauto work. But then, Coq is not able to bind them to their diff --git a/theories/typing/type.v b/theories/typing/type.v index b4fe9a2d..b3699565 100644 --- a/theories/typing/type.v +++ b/theories/typing/type.v @@ -147,6 +147,7 @@ Qed. Coercion ty_of_st : simple_type >-> type. +Declare Scope lrust_type_scope. Delimit Scope lrust_type_scope with T. Bind Scope lrust_type_scope with type. -- GitLab