# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1580658374 18000
# Node ID a913f19955e2680e130e340709f69a3b2eb0ad9e
# Parent  3fc43e261f672ea5e8a67b555daf37a10b56dccf
Update for Coq 8.11

diff -r 3fc43e261f67 -r a913f19955e2 .hgignore
--- a/.hgignore	Sun Apr 21 16:09:55 2019 -0400
+++ b/.hgignore	Sun Feb 02 10:46:14 2020 -0500
@@ -23,6 +23,9 @@
 
 *.glob
 *.v.d
+*.coq.d
+*.vok
+*.vos
 
 *.aux
 *.dvi
diff -r 3fc43e261f67 -r a913f19955e2 src/DataStruct.v
--- a/src/DataStruct.v	Sun Apr 21 16:09:55 2019 -0400
+++ b/src/DataStruct.v	Sun Feb 02 10:46:14 2020 -0500
@@ -294,7 +294,7 @@
 
 (** Now we can define a type family for expressions.  An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts].  We effectively use the de Bruijn index variable representation%~\cite{DeBruijn}%.  Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *)
 
-Inductive exp : list type -> type -> Set :=
+Inductive exp : list type -> type -> Type :=
 | Const : forall ts, exp ts Unit
 (* begin thide *)
 | Var : forall ts t, member t ts -> exp ts t
diff -r 3fc43e261f67 -r a913f19955e2 src/GeneralRec.v
--- a/src/GeneralRec.v	Sun Apr 21 16:09:55 2019 -0400
+++ b/src/GeneralRec.v	Sun Feb 02 10:46:14 2020 -0500
@@ -781,6 +781,8 @@
 
 I know no easy fix for this problem of [thunk], but we can define an alternate co-inductive monad that avoids the problem, based on a proposal by Megacz%~\cite{Megacz}%.  We ran into trouble because [TBind] was not a constructor of [thunk], so let us define a new type family where "bind" is a constructor. *)
 
+Set Universe Polymorphism.
+
 CoInductive comp (A : Type) : Type :=
 | Ret : A -> comp A
 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
diff -r 3fc43e261f67 -r a913f19955e2 src/Reflection.v
--- a/src/Reflection.v	Sun Apr 21 16:09:55 2019 -0400
+++ b/src/Reflection.v	Sun Feb 02 10:46:14 2020 -0500
@@ -386,9 +386,9 @@
 
 (** Now we are ready to revisit our earlier tautology solver example.  We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent.  We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example.  Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas.  For instance, we cannot prove [P -> P] by translating the formula into a value like [Imp (Var P) (Var P)], because a Gallina function has no way of comparing the two [P]s for equality.
 
-   To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library. *)
+   To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library.  (Actually, this tactic has apparently gone away in the most recent Coq versions, so this section is of historic interest only.) *)
 
-Require Import Quote.
+(*Require Import Quote.
 
 (* begin thide *)
 Inductive formula : Set :=
@@ -654,6 +654,7 @@
     ]]
 
 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *)
+*)
 
 (** ** Manual Reification of Terms with Variables *)