diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 14:06:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 18:59:00 +0200 |
| commit | 1a6a26d29252da54b86bf663a66ddd909905d1cb (patch) | |
| tree | 2489daca9a966cf869025a535f98f5799ff13ceb /plugins/ssr | |
| parent | 2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff) | |
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.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 4 |
2 files changed, 4 insertions, 4 deletions
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 |