Merge branch 'master' of github.com:achlipala/frap

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.

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.

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,

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.

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.

Interpreters.v

@@ -97,7 +97,8 @@ Proof.
 
   equality.
 
-  linear_arithmetic.
+  rewrite IHe1, IHe2.
+  ring.
 Qed.
 (* Well, that's a relief! ;-) *)
 
@@ -309,7 +310,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.

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.

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.

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.

_CoqProject

@@ -1,4 +1,5 @@
 -R . Frap
+-arg -w -arg -undeclared-scope
 Map.v
 Var.v
 Sets.v

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.