From 2eecd666a45a79241f0aadb9493ae8ef9cc9795e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Apr 2018 17:11:34 +0200
Subject: Documenting the deprecation.

---
 doc/sphinx/language/gallina-extensions.rst | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 6ea1c162f9..ff5d352c99 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2240,6 +2240,7 @@ This option (off by default) activates the full display of how the
 context of an existential variable is instantiated at each of the
 occurrences of the existential variable.
 
+.. _tactics-in-terms:
 
 Solving existential variables using tactics
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- 
cgit v1.2.3