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