diff options
| author | Pierre-Marie Pédrot | 2015-01-21 10:55:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-23 21:30:43 +0100 |
| commit | 43c6f29edde078726f10144c0d241a882ebdd13d (patch) | |
| tree | 822e23aa496c5d3284709c060bb56073536cc362 /tactics | |
| parent | 87106cd6a0e613fc61943959d8fc7d3ff025fc5d (diff) | |
Splitting ML tactics in one function per grammar entry.
Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacenv.ml | 8 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 3 |
3 files changed, 8 insertions, 5 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 9d8b9a9d54..1bffa9f60c 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -47,7 +47,7 @@ let pr_tacname t = let tac_tab = ref MLTacMap.empty -let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = +let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = let () = if MLTacMap.mem s !tac_tab then if overwrite then @@ -58,9 +58,11 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = in tac_tab := MLTacMap.add s t !tac_tab -let interp_ml_tactic { mltac_name = s } = +let interp_ml_tactic { mltac_name = s; mltac_index = i } = try - MLTacMap.find s !tac_tab + let tacs = MLTacMap.find s !tac_tab in + let () = if Array.length tacs <= i then raise Not_found in + tacs.(i) with Not_found -> Errors.errorlabstrm "" (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.") diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 72b1ca90ff..424bb142c7 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -48,7 +48,7 @@ type ml_tactic = typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic (** Type of external tactics, used by [TacML]. *) -val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit +val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit (** Register an external tactic. *) val interp_ml_tactic : ml_tactic_entry -> ml_tactic diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 8de804d6dc..e6f33a47be 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -159,7 +159,8 @@ 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 + (** Take care of the index: this is the second entry in constructor. *) + let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in Tacexpr.TacML (Loc.ghost, name, [i]) |