From 126dc656963a7feb589b2a3574f0c55ad84d5f69 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Aug 2017 00:52:39 +0200
Subject: Allowing to insert calls to Ltac1 references in Ltac2.

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

(limited to 'doc')

diff --git a/doc/ltac2.md b/doc/ltac2.md
index a645331e2d..51e3ab664d 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -692,6 +692,17 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0)
 Note that abbreviations are not typechecked at all, and may result in typing
 errors after expansion.
 
+# Compatibility layer with Ltac1
+
+## Ltac1 from Ltac2
+
+One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses
+a Ltac1 expression, and semantics of this quotation is the evaluation of the
+corresponding code for its side effects.
+
+Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
+to the use of standalone function calls.
+
 # Transition from Ltac1
 
 Owing to the use of a bunch of notations, the transition shouldn't be
-- 
cgit v1.2.3