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/ssrcommon.ml | |
| 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/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 |
1 files changed, 2 insertions, 2 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 |