From 078e29f8a9460d2355ca61661f98b3b67cd63e09 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 6 Mar 2018 20:29:57 -0500 Subject: [PATCH] ProofByReflection: some copyediting --- ProofByReflection.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ProofByReflection.v b/ProofByReflection.v index 0eac1cd..7bee89c 100644 --- a/ProofByReflection.v +++ b/ProofByReflection.v @@ -163,7 +163,7 @@ Print true_galore. * * To write a reflective procedure for this class of goals, we will need to get * into the actual "reflection" part of "proof by reflection." It is impossible - * to case-analyze a [Prop] in any way in Gallina. We must_reify_ [Prop] into + * to case-analyze a [Prop] in any way in Gallina. We must _reify_ [Prop] into * some type that we _can_ analyze. This inductive type is a good candidate: *) (* begin thide *) @@ -484,7 +484,7 @@ Ltac reify_set E := let e1 := reify_set E1 in let e2 := reify_set E2 in constr:(Union e1 e2) - | _ => let pf := constr:(eq_refl : E = {}) in constr:(Literal []) + | _ => let pf := constr:(E = {}) in constr:(Literal []) (* The twist is in this case: we instantiate all unification variables with * the empty set. It's a sound proof step, and it so happens that we only * call this tactic in spots where this heuristic makes sense. *) @@ -596,10 +596,10 @@ Section my_tauto. Require Import ListSet. (* The [eq_nat_dec] below is a richly typed equality test on [nat]s. We'll - * get to the ideas behind it next week. *) + * get to the ideas behind it in a later class. *) Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. - (* We define what it means for all members of an variable set to represent + (* We define what it means for all members of a variable set to represent * true propositions, and we prove some lemmas about this notion. *) Fixpoint allTrue (s : set propvar) : Prop :=