diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-21 10:55:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-23 21:30:43 +0100 |
| commit | 43c6f29edde078726f10144c0d241a882ebdd13d (patch) | |
| tree | 822e23aa496c5d3284709c060bb56073536cc362 /tactics/tacenv.ml | |
| 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/tacenv.ml')
| -rw-r--r-- | tactics/tacenv.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 9d8b9a9d5..1bffa9f60 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.") |