Skip to content

Commit

Permalink
Fix pcofix bug #41
Browse files Browse the repository at this point in the history
  • Loading branch information
@minkiminki
minkiminki committed Mar 18, 2021
1 parent c00ada4 commit 5a38bcf
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 15 deletions.
2 changes: 1 addition & 1 deletion metasrc/pacotac_internal.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -309,7 +309,7 @@
print (' assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;')
print (' first [')
print (' (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;')
print (' try (reflexivity);')
print (' [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];')
print (' first [eassumption|apply _paco_foo_cons]); fail')
print (' | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;')
print (' (try unfold _paco_id); eauto using _paco_foo_cons)]);')
Expand Down
28 changes: 14 additions & 14 deletions src/pacotac_internal.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1377,7 +1377,7 @@ Ltac paco_simp_hyp1 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -1483,7 +1483,7 @@ Ltac paco_simp_hyp2 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -1595,7 +1595,7 @@ Ltac paco_simp_hyp3 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -1713,7 +1713,7 @@ Ltac paco_simp_hyp4 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -1837,7 +1837,7 @@ Ltac paco_simp_hyp5 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -1967,7 +1967,7 @@ Ltac paco_simp_hyp6 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -2103,7 +2103,7 @@ Ltac paco_simp_hyp7 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -2245,7 +2245,7 @@ Ltac paco_simp_hyp8 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -2393,7 +2393,7 @@ Ltac paco_simp_hyp9 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -2547,7 +2547,7 @@ Ltac paco_simp_hyp10 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -2707,7 +2707,7 @@ Ltac paco_simp_hyp11 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -2873,7 +2873,7 @@ Ltac paco_simp_hyp12 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -3045,7 +3045,7 @@ Ltac paco_simp_hyp13 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down Expand Up @@ -3223,7 +3223,7 @@ Ltac paco_simp_hyp14 CIH :=
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
first [
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
try (reflexivity);
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
first [eassumption|apply _paco_foo_cons]); fail
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
(try unfold _paco_id); eauto using _paco_foo_cons)]);
Expand Down

0 comments on commit 5a38bcf

Please sign in to comment.