diff options
| author | Pierre-Marie Pédrot | 2016-03-20 03:00:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 03:03:55 +0100 |
| commit | 25bbce0e0cb841a7ad9d5c3e7ce33711b27bf41b (patch) | |
| tree | 52f9d461a62164034bc21fed120ca8b153cf28a0 /grammar | |
| parent | 25d49062425ee080d3e8d06920d3073e7a81b603 (diff) | |
| parent | 5f703bbb8b4f439af9d76b1f6ef24162b67049c2 (diff) | |
Moving most of Ltac code to Hightactics.
This is a major step towards the pluginification of Ltac. The one important
file that is out of reach for now is Tacsubst, as it is used in an intricate way
to handle amongst other things auto hints.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index bbd3d8a62f..2ef30f299b 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -120,7 +120,7 @@ let declare_tactic loc s c cl = match cl with let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in - let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ >> in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in declare_str_items loc [ <:str_item< do { try do { |