diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacenv.ml | 3 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 7 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 19 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
5 files changed, 21 insertions, 12 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index d7ab2d71ec..c7339acea7 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -15,9 +15,10 @@ open Tacexpr (** Tactic notations (TacAlias) *) type alias = KerName.t +type alias_tactic = Id.t list * glob_tactic_expr let alias_map = Summary.ref ~name:"tactic-alias" - (KNmap.empty : glob_tactic_expr KNmap.t) + (KNmap.empty : alias_tactic KNmap.t) let register_alias key tac = alias_map := KNmap.add key tac !alias_map diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 28fb138817..65fd693435 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -17,10 +17,13 @@ open Tacexpr type alias = KerName.t (** Type of tactic alias, used in the [TacAlias] node. *) -val register_alias : alias -> glob_tactic_expr -> unit +type alias_tactic = Id.t list * glob_tactic_expr +(** Contents of a tactic notation *) + +val register_alias : alias -> alias_tactic -> unit (** Register a tactic alias. *) -val interp_alias : alias -> glob_tactic_expr +val interp_alias : alias -> alias_tactic (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) val check_alias : alias -> bool diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 93d64f686d..e6273401dd 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -656,7 +656,7 @@ and intern_tactic_seq onlytac ist = function (* For extensions *) | TacAlias (loc,s,l) -> - let l = List.map (fun (id,a) -> (id,intern_tacarg !strict_check false ist a)) l in + let l = List.map (intern_tacarg !strict_check false ist) l in ist.ltacvars, TacAlias (loc,s,l) | TacML (loc,opn,l) -> let _ignore = Tacenv.interp_ml_tactic opn in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1596406c9a..a871815881 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) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 45b2d317c2..754c886205 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -245,7 +245,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with (* For extensions *) | TacAlias (_,s,l) -> let s = subst_kn subst s in - TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_tacarg subst a)) l) + TacAlias (dloc,s,List.map (subst_tacarg subst) l) | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l) and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) |