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 940aa6d1c..d31908114 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -186,6 +186,7 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg = | TacFreshId of string or_var list | Tacexp of ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr | TacPretype of 'trm + | TacNumgoals (** Generic ltac expressions. 't : terms, 'p : patterns, 'c : constants, 'i : inductive, diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 1ebfe9d97..dd7687f43 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -137,7 +137,8 @@ GEXTEND Gram TacGeneric (genarg_of_ipattern ipat) | c = constr_eval -> ConstrMayEval c | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l - | IDENT "type_term"; c=Constr.constr -> TacPretype c ] ] + | IDENT "type_term"; c=Constr.constr -> TacPretype c + | IDENT "numgoals" -> TacNumgoals ] ] ; fresh_id: [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ] diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e812086d9..2aadde7c1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -941,6 +941,7 @@ and pr_tacarg = function | UConstr c -> str"uconstr:" ++ pr_constr c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacPretype c -> str "type_term" ++ pr_constr c + | TacNumgoals -> str "numgoals" | 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 a651d298f..324ea2f04 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 _ | TacPretype _ as a -> + | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) | MetaIdArg _ -> assert false @@ -663,6 +663,7 @@ 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) | TacPretype c -> TacPretype (intern_constr ist c) + | TacNumgoals -> TacNumgoals | 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 a6f7ff9af..1eecb9497 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -971,6 +971,9 @@ struct bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l)) (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + let lift (type a) (t:a Proofview.tactic) : a t = + Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) + (** If the tactic returns unit, we can focus on the goals if necessary. *) let run m k = m >>= function | Uniform v -> k v @@ -1144,6 +1147,12 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t = Proofview.V82.tclEVARS sigma <*> GTac.return (Value.of_constr c_interp) end + | TacNumgoals -> + GTac.lift begin + let open Proofview.Notations in + Proofview.numgoals >>= fun i -> + Proofview.tclUNIT (Value.of_int i) + 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 c0b81e90d..ecadfca59 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -262,6 +262,7 @@ and subst_tacarg subst = function TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) + | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (subst_tactic subst t) | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> |