From 90285ff50290a49d20d60ffc59725bf87c6acd14 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 1 May 2020 13:22:42 +0200
Subject: Move essential vocabulary and syntax conventions to section on
 basics.

---
 doc/sphinx/proof-engine/ltac.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c1eb1f974c..8418e9c73d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -174,6 +174,14 @@ mode but it can also be used in toplevel definitions as shown below.
    ltac_def         : `ident` [`ident` ... `ident`] := `ltac_expr`
                     : `qualid` [`ident` ... `ident`] ::= `ltac_expr`
 
+Tactics in terms
+~~~~~~~~~~~~~~~~
+
+.. insertprodn term_ltac term_ltac
+
+.. prodn::
+   term_ltac ::= ltac : ( @ltac_expr )
+
 .. _ltac-semantics:
 
 Semantics
-- 
cgit v1.2.3