diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | parsing/egrammar.ml | 2 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 2 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 20 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 2 |
6 files changed, 16 insertions, 14 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 5692f780d..31d59cab2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1039,7 +1039,7 @@ and xlate_tac = (out_gen (wit_list0 rawwit_constr) arg))) | TacExtend (_,id, l) -> CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l)) - | TacAlias (_, _, _) -> xlate_error "TODO LATER: aliases" + | TacAlias _ -> xlate_error "TODO LATER: aliases" and coerce_genarg_to_TARG x = match Genarg.genarg_tag x with diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index ef3919c81..c3b5d98f8 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -428,7 +428,7 @@ let make_vprod_item univ = function let add_tactic_entries gl = let univ = get_univ "tactic" in - let make_act s tac loc l = Tacexpr.TacAlias (s,l,tac) in + let make_act s tac loc l = Tacexpr.TacAlias (loc,s,l,tac) in let f (s,l,tac) = make_rule univ (make_act s tac) (make_vprod_item "tactic") l in let rules = List.map f gl in diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8560726fb..9b11b58ac 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -396,7 +396,7 @@ let rec pr_atom0 = function (* Main tactic printer *) and pr_atom1 = function | TacExtend (_,s,l) -> pr_extend pr_constr pr_tac s l - | TacAlias (s,l,_) -> pr_extend pr_constr pr_tac s (List.map snd l) + | TacAlias (_,s,l,_) -> pr_extend pr_constr pr_tac s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 0fd4130d2..bdc8f3367 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -165,7 +165,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExtend of loc * string * ('constr,'tac) generic_argument list (* For syntax extensions *) - | TacAlias of string * + | TacAlias of loc * string * (identifier * ('constr,'tac) generic_argument) list * 'tac diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a58220238..c2a1cf4ba 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -414,9 +414,10 @@ let intern_quantified_hypothesis ist x = x let intern_constr {ltacvars=lfun; metavars=lmatch; gsigma=sigma; genv=env} c = - let c' = - Constrintern.for_grammar (Constrintern.interp_rawconstr_gen false - sigma env [] (Some lmatch) (fst lfun,[])) c + let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in + let c' = + warn (Constrintern.interp_rawconstr_gen false sigma env [] + (Some lmatch) (fst lfun,[])) c in (c',if !strict_check then None else Some c) (* Globalize bindings *) @@ -652,11 +653,11 @@ let rec intern_atomic lf ist x = | TacExtend (_loc,opn,l) -> let _ = lookup_tactic opn in TacExtend (loc,opn,List.map (intern_genarg ist) l) - | TacAlias (s,l,body) -> + | TacAlias (loc,s,l,body) -> let (l1,l2) = ist.ltacvars in let ist' = { ist with ltacvars = ((List.map fst l)@l1,l2) } in TacAlias - (s,List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l, + (loc,s,List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l, intern_tactic ist' body) and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) @@ -1720,7 +1721,7 @@ and interp_atomic ist gl = function (* For extensions *) | TacExtend (loc,opn,l) -> fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl - | TacAlias (_,l,body) -> fun gl -> + | TacAlias (loc,_,l,body) -> fun gl -> let f x = match genarg_tag x with | IdentArgType -> let id = out_gen globwit_ident x in @@ -1737,7 +1738,8 @@ and interp_atomic ist gl = function | _ -> failwith "This generic type is not supported in alias" in let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in - tactic_of_value (val_interp { ist with lfun=lfun } gl body) gl + let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body) + in tactic_of_value v gl (* Initial call for interpretation *) let interp_tac_gen lfun lmatch debug t gl = @@ -1932,8 +1934,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* For extensions *) | TacExtend (_loc,opn,l) -> TacExtend (loc,opn,List.map (subst_genarg subst) l) - | TacAlias (s,l,body) -> - TacAlias (s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,subst_tactic subst body) + | TacAlias (_,s,l,body) -> + TacAlias (loc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,subst_tactic subst body) and subst_tactic subst (t:glob_tactic_expr) = match t with | TacAtom (_loc,t) -> TacAtom (loc, subst_atomic subst t) diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 44224227d..acff5e164 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -202,7 +202,7 @@ let rec pr_atom0 env = function and pr_atom1 env = function | TacExtend (_,s,l) -> pr_extend (pr_constr env) (pr_tac env) s l - | TacAlias (s,l,_) -> + | TacAlias (_,s,l,_) -> pr_extend (pr_constr env) (pr_tac env) s (List.map snd l) (* Basic tactics *) |