Mercurial > cpdt > repo
diff src/Reflection.v @ 554:93471096cdd4
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 Aug 2017 12:14:40 -0400 |
parents | 2c8c693ddaba |
children | a913f19955e2 |
line wrap: on
line diff
--- a/src/Reflection.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/Reflection.v Sat Aug 19 12:14:40 2017 -0400 @@ -673,7 +673,7 @@ let b := inList x xs in match b with | true => xs - | false => constr:(x, xs) + | false => constr:((x, xs)) end. (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *) @@ -718,8 +718,8 @@ Ltac reifyTerm xs e := match e with - | True => constr:Truth' - | False => constr:Falsehood' + | True => Truth' + | False => Falsehood' | ?e1 /\ ?e2 => let p1 := reifyTerm xs e1 in let p2 := reifyTerm xs e2 in