Mercurial > cpdt > repo
changeset 547:2c8c693ddaba
Fixes for Coq 8.6
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 12 Jul 2017 13:08:24 -0400 |
parents | 306539f29eea |
children | a43fd2ba7ad3 |
files | src/GeneralRec.v src/Match.v src/Reflection.v src/Universes.v |
diffstat | 4 files changed, 7 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/src/GeneralRec.v Thu May 12 18:09:36 2016 -0500 +++ b/src/GeneralRec.v Wed Jul 12 13:08:24 2017 -0400 @@ -822,10 +822,6 @@ match goal with | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst end. - move H3 after A. - generalize dependent B0. - do 2 intro. - subst. crush. inversion H; clear H; crush. eauto. @@ -839,10 +835,6 @@ match goal with | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst end. - move H3 after B. - generalize dependent B0. - do 2 intro. - subst. crush. inversion H0; clear H0; crush. eauto.
--- a/src/Match.v Thu May 12 18:09:36 2016 -0500 +++ b/src/Match.v Wed Jul 12 13:08:24 2017 -0400 @@ -444,7 +444,7 @@ Sometimes we need to employ the opposite direction of "nonterminal escape," when we want to pass a complicated tactic expression as an argument to another tactic, as we might want to do in invoking %\coqdocvar{%#<tt>#map#</tt>#%}%. *) Goal False. - let ls := map (nat * nat)%type ltac:(fun x => constr:(x, x)) (1 :: 2 :: 3 :: nil) in + let ls := map (nat * nat)%type ltac:(fun x => constr:((x, x))) (1 :: 2 :: 3 :: nil) in pose ls. (** [[ l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)
--- 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
--- a/src/Universes.v Thu May 12 18:09:36 2016 -0500 +++ b/src/Universes.v Wed Jul 12 13:08:24 2017 -0400 @@ -1068,7 +1068,9 @@ The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) - discriminate. + try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically! + * This line left here to keep everything working in + * 8.4, 8.5, and 8.6. *) (** %\vspace{-.15in}%[[ H : proof p H1 : And p q = And p0 q0