## Mercurial > cpdt > repo

### diff src/Reflection.v @ 547:2c8c693ddaba

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Fixes for Coq 8.6

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 12 Jul 2017 13:08:24 -0400 |

parents | ed829eaa91b2 |

children |

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