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/ssrcommon.ml | 4 ++-- plugins/ssr/ssrparser.ml4 | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/ssr') diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cf5fdf318..d37c676e3 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -814,8 +814,8 @@ let ssr_n_tac seed n gl = let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in let tacname = - try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) - with Not_found -> try Nametab.locate_tactic (ssrqid name) + try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) + with Not_found -> try Tacenv.locate_tactic (ssrqid name) with Not_found -> if n = -1 then fail "The ssreflect library was not loaded" else fail ("The tactic "^name^" was not found") in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 1e1a986da..7b591fead 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