Mercurial > cpdt > repo
changeset 572:a913f19955e2
Update for Coq 8.11
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 02 Feb 2020 10:46:14 -0500 |
| parents | 3fc43e261f67 |
| children | c3d77f2bb92c |
| files | .hgignore src/DataStruct.v src/GeneralRec.v src/Reflection.v |
| diffstat | 4 files changed, 9 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- 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
--- 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
--- 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.
--- 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 *)