diff options
| -rw-r--r-- | intf/tacexpr.mli | 1 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 3 | ||||
| -rw-r--r-- | printing/pptactic.ml | 1 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 9 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
6 files changed, 16 insertions, 2 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 99e151e38..940aa6d1c 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -185,6 +185,7 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg = ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list | TacFreshId of string or_var list | Tacexp of ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr + | TacPretype of 'trm (** Generic ltac expressions. 't : terms, 'p : patterns, 'c : constants, 'i : inductive, diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 8b1a1979f..4be4aa4ae 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -138,7 +138,8 @@ GEXTEND Gram ; may_eval_arg: [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ] + | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l + | IDENT "type_term"; c=Constr.constr -> TacPretype c ] ] ; fresh_id: [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ] diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7fc214304..2b7f2babd 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -940,6 +940,7 @@ and pr_tacarg = function | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c | UConstr c -> str"uconstr:" ++ pr_constr c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l + | TacPretype c -> str "fresh" ++ pr_constr c | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 44b695e21..a651d298f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -631,7 +631,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a - | ConstrMayEval _ | UConstr _ | TacFreshId _ as a -> + | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) | MetaIdArg _ -> assert false @@ -662,6 +662,7 @@ and intern_tacarg strict onlytac ist = function | TacExternal (loc,com,req,la) -> TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) + | TacPretype c -> TacPretype (intern_constr ist c) | Tacexp t -> Tacexp (intern_tactic onlytac ist t) | TacGeneric arg -> let (_, arg) = Genintern.generic_intern ist arg in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cb63d53dd..a6f7ff9af 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1135,6 +1135,15 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t = let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)) end + | TacPretype c -> + GTac.raw_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let c_glob = interp_uconstr ist env c in + let (sigma,c_interp) = Pretyping.understand_tcc sigma env c_glob in + Proofview.V82.tclEVARS sigma <*> + GTac.return (Value.of_constr c_interp) + end | Tacexp t -> val_interp ist t | TacDynamic(_,t) -> let tg = (Dyn.tag t) in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 0872f8bbf..c0b81e90d 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -261,6 +261,7 @@ and subst_tacarg subst = function | TacExternal (_loc,com,req,la) -> TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | TacFreshId _ as x -> x + | TacPretype c -> TacPretype (subst_glob_constr subst c) | Tacexp t -> Tacexp (subst_tactic subst t) | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> |