aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-25 16:46:41 +0000
committerGitHub2021-02-25 16:46:41 +0000
commit24e94b3dac66510e6d57b9f55f9a4e3e84fd6e54 (patch)
tree5befd0a43d5973f3c0707c65a90265121db8047c /test-suite
parent6ef58b0e9348d49ccf456d9fd475368c3dc1aafa (diff)
parent0772562f1ef66ee69677456963187d6ff736b0bf (diff)
Merge PR #13202: Infrastructure for fine-grained debug flags
Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/DebugFlags.out44
-rw-r--r--test-suite/output/DebugFlags.v5
2 files changed, 49 insertions, 0 deletions
diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out
new file mode 100644
index 0000000000..0385413937
--- /dev/null
+++ b/test-suite/output/DebugFlags.out
@@ -0,0 +1,44 @@
+File "stdin", line 1, characters 0-16:
+Warning: There is no debug flag "cbn". [unknown-debug-flag,option]
+Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<?A -> ?A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<?A -> ?A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> Prop|>>
+Debug: [RAKAM] <><><><><>
+2 + 3 = 0
+ : Prop
diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v
new file mode 100644
index 0000000000..32c0f2d24b
--- /dev/null
+++ b/test-suite/output/DebugFlags.v
@@ -0,0 +1,5 @@
+Set Debug "cbn".
+
+Set Debug "RAKAM".
+
+Check 2 + 3 = 0.