diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-30 15:22:27 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-30 15:22:27 +0000 |
| commit | 7bb6ca92a08f24c86f74a1bc134fe1f5b4930595 (patch) | |
| tree | a072c5b9edb67e2d5ac91a43b7b90704da16c394 /test-suite/output/Quote.out | |
| parent | 07c06e775953e52fe4f90b85d63479577b0c688a (diff) | |
Add tests for quote
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Quote.out')
| -rw-r--r-- | test-suite/output/Quote.out | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out new file mode 100644 index 000000000..ca7fc3624 --- /dev/null +++ b/test-suite/output/Quote.out @@ -0,0 +1,24 @@ +(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx)) +(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx)))))) +1 subgoal + + H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ + B + ============================ + interp_f + (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) + (f_and (f_atom (Left_idx End_idx)) + (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) + (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx))))) +1 subgoal + + H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ + B + ============================ + interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx))))) |