diff options
| author | Pierre-Marie Pédrot | 2015-01-21 00:26:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-21 00:46:06 +0100 |
| commit | c2d053c6f38a54e3083c8726eccb3e73942107b7 (patch) | |
| tree | 2eef9978ece47590799ab97acfe9043e213b8d40 /tactics | |
| parent | 9cc95f5a34b9050fe5a869f0fb96da562b45353d (diff) | |
Embedding the index of the ML tactic entry in the Tacexpr AST.
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 1 |
3 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index cb20fc9308..9d8b9a9d54 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -58,7 +58,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = in tac_tab := MLTacMap.add s t !tac_tab -let interp_ml_tactic s = +let interp_ml_tactic { mltac_name = s } = try MLTacMap.find s !tac_tab with Not_found -> diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4ca..72b1ca90ff 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -51,5 +51,5 @@ type ml_tactic = val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit (** Register an external tactic. *) -val interp_ml_tactic : ml_tactic_name -> ml_tactic +val interp_ml_tactic : ml_tactic_entry -> ml_tactic (** Get the named tactic. Raises a user error if it does not exist. *) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 4b03ff249f..8de804d6dc 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -159,6 +159,7 @@ let flatten_contravariant_conj flags ist = let constructor i = let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in + let name = { Tacexpr.mltac_name = name; mltac_index = 0 } in let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in Tacexpr.TacML (Loc.ghost, name, [i]) |