diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12bfb4d09e..22b9abda20 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2019,7 +2019,7 @@ let hide_interp {global;ast} = hide_interp (Proofview.Goal.env gl) end -let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp +let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp (***************************************************************************) (** Register standard arguments *) |