From 1a6a26d29252da54b86bf663a66ddd909905d1cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 Oct 2017 14:06:29 +0200
Subject: Moving the Ltac-specific part of the nametab to the Ltac plugin.

For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
---
 plugins/ssr/ssrparser.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr/ssrparser.ml4')

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 1e1a986daa..7b591feada 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1554,8 +1554,8 @@ END
 let ssrautoprop gl =
   try 
     let tacname = 
-      try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
-      with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in
+      try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
+      with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
     let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
     Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
   with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl
-- 
cgit v1.2.3