Add tests for quote

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12038 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 36 insertions, 0 deletions

diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v
new file mode 100644
index 000000000..2c373d505
--- /dev/null
+++ b/test-suite/output/Quote.v
@@ -0,0 +1,36 @@
+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.