Mercurial > cpdt > repo
diff src/Reflection.v @ 547:2c8c693ddaba
Fixes for Coq 8.6
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 12 Jul 2017 13:08:24 -0400 |
parents | ed829eaa91b2 |
children | a913f19955e2 |
line wrap: on
line diff
--- a/src/Reflection.v Thu May 12 18:09:36 2016 -0500 +++ b/src/Reflection.v Wed Jul 12 13:08:24 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