## Mercurial > cpdt > repo

### comparison 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 |

comparison

equal
deleted
inserted
replaced

546:306539f29eea | 547:2c8c693ddaba |
---|---|

671 | 671 |

672 Ltac addToList x xs := | 672 Ltac addToList x xs := |

673 let b := inList x xs in | 673 let b := inList x xs in |

674 match b with | 674 match b with |

675 | true => xs | 675 | true => xs |

676 | false => constr:(x, xs) | 676 | false => constr:((x, xs)) |

677 end. | 677 end. |

678 | 678 |

679 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *) | 679 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *) |

680 | 680 |

681 Ltac allVars xs e := | 681 Ltac allVars xs e := |

716 | 716 |

717 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) | 717 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) |

718 | 718 |

719 Ltac reifyTerm xs e := | 719 Ltac reifyTerm xs e := |

720 match e with | 720 match e with |

721 | True => constr:Truth' | 721 | True => Truth' |

722 | False => constr:Falsehood' | 722 | False => Falsehood' |

723 | ?e1 /\ ?e2 => | 723 | ?e1 /\ ?e2 => |

724 let p1 := reifyTerm xs e1 in | 724 let p1 := reifyTerm xs e1 in |

725 let p2 := reifyTerm xs e2 in | 725 let p2 := reifyTerm xs e2 in |

726 constr:(And' p1 p2) | 726 constr:(And' p1 p2) |

727 | ?e1 \/ ?e2 => | 727 | ?e1 \/ ?e2 => |