diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations.out | 14 | ||||
| -rw-r--r-- | test-suite/output/Quote.v | 36 |
2 files changed, 8 insertions, 42 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index b60b1ee863..94b86fc222 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -125,13 +125,15 @@ s : nat fun _ : nat => 9 : nat -> nat -fun (x : nat) (p : x = x) => match p with - | ONE => ONE - end = p +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| ONE => ONE +end = p : forall x : nat, x = x -> Prop -fun (x : nat) (p : x = x) => match p with - | 1 => 1 - end = p +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| 1 => 1 +end = p : forall x : nat, x = x -> Prop bar 0 : nat diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v deleted file mode 100644 index 2c373d5052..0000000000 --- a/test-suite/output/Quote.v +++ /dev/null @@ -1,36 +0,0 @@ -Require Import Quote. - -Parameter A B : Prop. - -Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula - | f_const : Prop -> formula. - -Fixpoint interp_f (vm: - varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - | f_const c => c - end. - -Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B). -intro H. -match goal with - | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H) -end. -match goal with - |- ?g => quote interp_f [ A ] in g using (fun x => idtac x) -end. -quote interp_f. -Show. -simpl; quote interp_f [ A ]. -Show. -Admitted. |