From d80e854d6827252676c2c504bb3108152a94d629 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Sep 2017 15:24:33 +0200
Subject: Quick-and-dirty backtrace mechanism for the interpreter.

---
 doc/ltac2.md | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc')

diff --git a/doc/ltac2.md b/doc/ltac2.md
index dd0dc391c6..c1216d8f89 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -703,6 +703,11 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0)
 Note that abbreviations are not typechecked at all, and may result in typing
 errors after expansion.
 
+# Debug
+
+When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with
+a backtrace.
+
 # Compatibility layer with Ltac1
 
 ## Ltac1 from Ltac2
-- 
cgit v1.2.3