Skip to content
Snippets Groups Projects
Commit ba9e2688 authored by Enrico Tassi's avatar Enrico Tassi
Browse files

adapt to coq/coq#13840

parent 7b4a04ce
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 10 additions and 10 deletions
tests/proofmode_ascii.v
+ 10
− 10
View file @ ba9e2688
...@@ -301,57 +301,57 @@ Proof. naive_solver. Qed. ...@@ -301,57 +301,57 @@ Proof. naive_solver. Qed.
Check "p1". Check "p1".
Lemma p1 : forall P, True -> P |- P. Lemma p1 : forall P, True -> P |- P.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p2". Check "p2".
Lemma p2 : forall P, True /\ (P |- P). Lemma p2 : forall P, True /\ (P |- P).
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p3". Check "p3".
Lemma p3 : exists P, P |- P. Lemma p3 : exists P, P |- P.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p4". Check "p4".
Lemma p4 : |-@{PROP} exists (x : nat), ⌜x = 0⌝. Lemma p4 : |-@{PROP} exists (x : nat), ⌜x = 0⌝.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p5". Check "p5".
Lemma p5 : |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝. Lemma p5 : |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p6". Check "p6".
Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝. Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p7". Check "p7".
Lemma p7 : forall (a : nat), a = 0 -> forall y, True |-@{PROP} ⌜y >= 0⌝. Lemma p7 : forall (a : nat), a = 0 -> forall y, True |-@{PROP} ⌜y >= 0⌝.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p8". Check "p8".
Lemma p8 : forall (a : nat), a = 0 -> forall y, |-@{PROP} ⌜y >= 0⌝. Lemma p8 : forall (a : nat), a = 0 -> forall y, |-@{PROP} ⌜y >= 0⌝.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Check "p9". Check "p9".
Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, ⌜z >= 0⌝. Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, ⌜z >= 0⌝.
Proof. Proof.
Unset Printing Notations. Show. Set Printing Notations. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Set Printing Notations. Set Printing Notations. Unset Printing Raw Literals.
End parsing_tests. End parsing_tests.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment