diff options
| author | Emilio Jesus Gallego Arias | 2018-11-06 14:25:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-13 12:11:47 +0100 |
| commit | 4aa99307874c59f97570f624a06463aaa8115ec5 (patch) | |
| tree | 37c85d78a4b6f534a5d3df02f053d9472cbf567a /plugins | |
| parent | 76048d675212211b623616da7132826d1ee41870 (diff) | |
[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.
This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.
We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.
Note the beneficial effects on reducing the `.mli` API.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0f88734caf..1b212334ce 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -700,7 +700,7 @@ type ('b, 'c) argument_interp = (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { - arg_parsing : 'a Vernacentries.argument_rule; + arg_parsing : 'a Vernacextend.argument_rule; arg_tag : 'c Val.tag option; arg_intern : ('a, 'b) argument_intern; arg_subst : 'b argument_subst; @@ -751,10 +751,10 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = in let () = register_interp0 wit (interp_fun name arg tag) in let entry = match arg.arg_parsing with - | Vernacentries.Arg_alias e -> + | Vernacextend.Arg_alias e -> let () = Pcoq.register_grammar wit e in e - | Vernacentries.Arg_rules rules -> + | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in e diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index c93d6251e0..79f9e093fb 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -128,7 +128,7 @@ type ('b, 'c) argument_interp = (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { - arg_parsing : 'a Vernacentries.argument_rule; + arg_parsing : 'a Vernacextend.argument_rule; arg_tag : 'c Geninterp.Val.tag option; arg_intern : ('a, 'b) argument_intern; arg_subst : 'b argument_subst; |