From 77f22213d893b3f63efa368fb22c8e350c55bf9a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 10 Feb 2020 13:44:35 -0500 Subject: [PATCH 1/2] Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working --- CompilerCorrectness.v | 2 +- CompilerCorrectness_template.v | 2 +- FrapWithoutSets.v | 2 +- HoareLogic.v | 4 ++-- Imp.v | 2 +- Interpreters.v | 2 +- Interpreters_template.v | 2 +- Polymorphism.v | 2 +- Polymorphism_template.v | 2 +- _CoqProject | 1 + 10 files changed, 11 insertions(+), 10 deletions(-) diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v index bf85744..c571e4b 100644 --- a/CompilerCorrectness.v +++ b/CompilerCorrectness.v @@ -40,7 +40,7 @@ Inductive cmd := Coercion Const : nat >-> arith. Coercion Var : var >-> arith. -Declare Scope arith_scope. +(*Declare Scope arith_scope.*) Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope. diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v index e357280..dcf571c 100644 --- a/CompilerCorrectness_template.v +++ b/CompilerCorrectness_template.v @@ -26,7 +26,7 @@ Inductive cmd := Coercion Const : nat >-> arith. Coercion Var : var >-> arith. -Declare Scope arith_scope. +(*Declare Scope arith_scope.*) Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope. diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v index fccc766..bd2ac72 100644 --- a/FrapWithoutSets.v +++ b/FrapWithoutSets.v @@ -101,7 +101,7 @@ Ltac instantiate_obviouses := (** * Interlude: special notations and induction principle for [N] *) (* Note: recurse is an identifier, but we will always use the name "recurse" by convention *) -Declare Scope N_recursion_scope. +(*Declare Scope N_recursion_scope.*) Notation "recurse 'by' 'cases' | 0 => A | n + 1 => B 'end'" := (N.recursion A (fun n recurse => B)) (at level 11, A at level 200, n at level 0, B at level 200, diff --git a/HoareLogic.v b/HoareLogic.v index e2ab5fd..2ddf399 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -170,7 +170,7 @@ Qed. (* BEGIN syntax macros that won't be explained *) Coercion Const : nat >-> exp. Coercion Var : string >-> exp. -Declare Scope cmd_scope. +(*Declare Scope cmd_scope.*) Notation "*[ e ]" := (Read e) : cmd_scope. Infix "+" := Plus : cmd_scope. Infix "-" := Minus : cmd_scope. @@ -190,7 +190,7 @@ Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 7 Notation "'assert' {{ I }}" := (Assert I) (at level 75). Delimit Scope cmd_scope with cmd. -Declare Scope reset_scope. +(*Declare Scope reset_scope.*) Infix "+" := plus : reset_scope. Infix "-" := Init.Nat.sub : reset_scope. Infix "*" := mult : reset_scope. diff --git a/Imp.v b/Imp.v index e349a8a..aec61ee 100644 --- a/Imp.v +++ b/Imp.v @@ -19,7 +19,7 @@ Inductive cmd := Coercion Const : nat >-> arith. Coercion Var : var >-> arith. -Declare Scope arith_scope. +(*Declare Scope arith_scope.*) Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope. diff --git a/Interpreters.v b/Interpreters.v index 50b7a85..1f09506 100644 --- a/Interpreters.v +++ b/Interpreters.v @@ -309,7 +309,7 @@ Example factorial_ugly := * them from our examples. *) Coercion Const : nat >-> arith. Coercion Var : var >-> arith. -Declare Scope arith_scope. +(*Declare Scope arith_scope.*) Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope. diff --git a/Interpreters_template.v b/Interpreters_template.v index d289bf9..bfb4b05 100644 --- a/Interpreters_template.v +++ b/Interpreters_template.v @@ -249,7 +249,7 @@ Example factorial_ugly := * them from our examples. *) Coercion Const : nat >-> arith. Coercion Var : var >-> arith. -Declare Scope arith_scope. +(*Declare Scope arith_scope.*) Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope. diff --git a/Polymorphism.v b/Polymorphism.v index 287acba..659de38 100644 --- a/Polymorphism.v +++ b/Polymorphism.v @@ -448,7 +448,7 @@ Inductive statement : Set := * almost-natural-looking embedded programs in Coq. *) Coercion Const : nat >-> expression. Coercion Var : string >-> expression. -Declare Scope embedded_scope. +(*Declare Scope embedded_scope.*) Infix "+" := Plus : embedded_scope. Infix "-" := Minus : embedded_scope. Infix "*" := Times : embedded_scope. diff --git a/Polymorphism_template.v b/Polymorphism_template.v index 2beb84b..9414ccc 100644 --- a/Polymorphism_template.v +++ b/Polymorphism_template.v @@ -291,7 +291,7 @@ Inductive statement : Set := * almost-natural-looking embedded programs in Coq. *) Coercion Const : nat >-> expression. Coercion Var : string >-> expression. -Declare Scope embedded_scope. +(*Declare Scope embedded_scope.*) Infix "+" := Plus : embedded_scope. Infix "-" := Minus : embedded_scope. Infix "*" := Times : embedded_scope. diff --git a/_CoqProject b/_CoqProject index 19d5cab..6b3e8f6 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ -R . Frap +-arg -w -arg -undeclared-scope Map.v Var.v Sets.v From 6ea006fccf265fed587d23487433137efa51066c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 10 Feb 2020 13:53:26 -0500 Subject: [PATCH 2/2] Truly building with Coq 8.9 again --- Interpreters.v | 3 ++- frap_book.tex | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Interpreters.v b/Interpreters.v index 1f09506..e06d7ed 100644 --- a/Interpreters.v +++ b/Interpreters.v @@ -97,7 +97,8 @@ Proof. equality. - linear_arithmetic. + rewrite IHe1, IHe2. + ring. Qed. (* Well, that's a relief! ;-) *) diff --git a/frap_book.tex b/frap_book.tex index a96a196..846bf71 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -5461,7 +5461,7 @@ The project home page is: \begin{center} \url{https://coq.inria.fr/} \end{center} -The code associated with this book is designed to work with Coq versions 8.10 and higher. +The code associated with this book is designed to work with Coq versions 8.9 and higher. The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common. We assume that readers have installed Coq by one of those means or another. It will also be almost essential to use some graphical interface for Coq editing.