diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tacintern.ml | 11 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 7 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 3 | ||||
-rw-r--r-- | tactics/tauto.ml4 | 4 |
4 files changed, 16 insertions, 9 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index b1830523b..3f52de11c 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -688,10 +688,10 @@ and intern_tactic_seq onlytac ist = function and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with - | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a) + | TacCall _ | TacExternal _ | Reference _ + | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a - | TacVoid | IntroPattern _ | Integer _ - | ConstrMayEval _ | TacFreshId _ as a -> + | IntroPattern _ | ConstrMayEval _ | TacFreshId _ as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) | MetaIdArg _ -> assert false @@ -705,12 +705,10 @@ and intern_tactic_fun ist (var,body) = (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body) and intern_tacarg strict onlytac ist = function - | TacVoid -> TacVoid | Reference r -> intern_non_tactic_reference strict ist r | IntroPattern ipat -> let lf = ref([],[]) in (*How to know what names the intropattern binds?*) IntroPattern (intern_intro_pattern lf ist ipat) - | Integer n -> Integer n | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) | MetaIdArg (loc,istac,s) -> (* $id can occur in Grammar tactic... *) @@ -728,6 +726,9 @@ and intern_tacarg strict onlytac ist = function TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) | Tacexp t -> Tacexp (intern_tactic onlytac ist t) + | TacGeneric arg -> + let (_, arg) = Genintern.generic_intern ist arg in + TacGeneric arg | TacDynamic(loc,t) as x -> (match Dyn.tag t with | "tactic" | "value" -> x diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 09dcb49f4..de72f2b5c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1090,12 +1090,15 @@ and interp_ltac_reference loc' mustbetac ist gl = function and interp_tacarg ist gl arg = let evdref = ref (project gl) in let v = match arg with - | TacVoid -> in_gen (topwit wit_unit) () + | TacGeneric arg -> + let gl = { gl with sigma = !evdref } in + let (sigma, v) = Geninterp.generic_interp ist gl arg in + evdref := sigma; + v | Reference r -> let (sigma,v) = interp_ltac_reference dloc false ist gl r in evdref := sigma; v - | Integer n -> in_gen (topwit wit_int) n | IntroPattern ipat -> let ans = interp_intro_pattern ist gl ipat in in_gen (topwit wit_intro_pattern) ans diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index dcdaf9dbc..274c3b352 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -264,8 +264,9 @@ and subst_tacarg subst = function TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) | TacExternal (_loc,com,req,la) -> TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) - | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x + | (IntroPattern _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) + | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> (match Dyn.tag t with | "tactic" | "value" -> x diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index ab31b664d..587ea3311 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -13,6 +13,8 @@ open Hipattern open Names open Globnames open Pp +open Genarg +open Stdarg open Tacticals open Tacinterp open Tactics @@ -174,7 +176,7 @@ let flatten_contravariant_disj flags ist = let hyp = valueIn (Value.of_constr hyp) in iter_tac (List.map_i (fun i arg -> let typ = valueIn (Value.of_constr (mkArrow arg c)) in - let i = Tacexpr.Integer i in + let i = Tacexpr.TacGeneric (in_gen (rawwit wit_int) i) in <:tactic< let typ := $typ in let hyp := $hyp in |