aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorMaxime Dénès2020-10-15 15:31:51 +0200
committerGaëtan Gilbert2021-02-24 15:09:15 +0100
commit068031ff7da092c1e2d35db27d713b9606960c42 (patch)
tree2a3e2ae6a82e60a76ef31659ff305d70a4b2ea39 /test-suite
parent264aba2484312a2172cd36dd9b89ed66e4f38864 (diff)
Infrastructure for fine-grained debug flags
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.