From 6a148b1b876906cdea6ed74dc80789f8a3ea16e6 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 22 Dec 2019 12:28:27 +0100
Subject: [refman] Mention Ltac2 in intro.

---
 doc/sphinx/proof-engine/ltac2.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index cfdc70d50e..dd80b29bda 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1,12 +1,12 @@
 .. _ltac2:
 
+Ltac2
+=====
+
 .. coqtop:: none
 
    From Ltac2 Require Import Ltac2.
 
-Ltac2
-=====
-
 The Ltac tactic language is probably one of the ingredients of the success of
 Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
 
-- 
cgit v1.2.3