diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1596406c9..a87181588 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1238,14 +1238,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with eval_tactic ist tac (* For extensions *) | TacAlias (loc,s,l) -> - let body = Tacenv.interp_alias s in + let (ids, body) = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in - let interp_vars = - Ftactic.List.map (fun (x,v) -> interp_tacarg ist v >>= fun v -> Ftactic.return (x,v)) l - in - let addvar (x, v) accu = Id.Map.add x v accu in + let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = - let lfun = List.fold_right addvar l ist.lfun in + let addvar x v accu = Id.Map.add x v accu in + let lfun = List.fold_right2 addvar ids l ist.lfun in let trace = push_trace (loc,LtacNotationCall s) ist in let ist = { lfun = lfun; @@ -1255,12 +1253,19 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> - let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s (List.map snd lr) in + let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in Proofview.Trace.name_tactic name (tac lr) (* spiwack: this use of name_tactic is not robust to a change of implementation of [Ftactic]. In such a situation, some more elaborate solution will have to be used. *) in + let tac = + let len1 = List.length ids in + let len2 = List.length l in + if len1 = len2 then tac + else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ + expected " ++ int len1 ++ str ", found " ++ int len2) + in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) -> |