aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_coqast.ml410
-rw-r--r--intf/tacexpr.mli6
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--printing/pptactic.ml7
-rw-r--r--tactics/coretactics.ml461
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml26
-rw-r--r--tactics/tacsubst.ml6
8 files changed, 61 insertions, 67 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index abc0d31a93..6a413ca313 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -310,23 +310,15 @@ let rec mlexpr_of_atomic_tactic = function
<:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
| Tacexpr.TacExact c ->
<:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
- | Tacexpr.TacExactNoCheck c ->
- <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
- | Tacexpr.TacVmCastNoCheck c ->
- <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
| Tacexpr.TacApply (b,false,cb,None) ->
<:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
| Tacexpr.TacElim (false,cb,cbo) ->
let cb = mlexpr_of_constr_with_binding cb in
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
<:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
- | Tacexpr.TacElimType c ->
- <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >>
| Tacexpr.TacCase (false,cb) ->
let cb = mlexpr_of_constr_with_binding cb in
<:expr< Tacexpr.TacCase False $cb$ >>
- | Tacexpr.TacCaseType c ->
- <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >>
| Tacexpr.TacFix (ido,n) ->
let ido = mlexpr_of_ident_option ido in
let n = mlexpr_of_int n in
@@ -346,8 +338,6 @@ let rec mlexpr_of_atomic_tactic = function
let l = mlexpr_of_list f l in
<:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
- | Tacexpr.TacCut c ->
- <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
| Tacexpr.TacAssert (t,ipat,c) ->
let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
<:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 532786fd37..5a7a20ef63 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -106,19 +106,14 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacIntrosUntil of quantified_hypothesis
| TacIntroMove of Id.t option * 'nam move_location
| TacExact of 'trm
- | TacExactNoCheck of 'trm
- | TacVmCastNoCheck of 'trm
| TacApply of advanced_flag * evars_flag * 'trm with_bindings list *
('nam * intro_pattern_expr located option) option
| TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option
- | TacElimType of 'trm
| TacCase of evars_flag * 'trm with_bindings
- | TacCaseType of 'trm
| TacFix of Id.t option * int
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
| TacCofix of Id.t option
| TacMutualCofix of Id.t * (Id.t * 'trm) list
- | TacCut of 'trm
| TacAssert of
('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
intro_pattern_expr located option * 'trm
@@ -136,7 +131,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacDecomposeOr of 'trm
| TacDecompose of 'ind list * 'trm
| TacSpecialize of int option * 'trm with_bindings
- | TacLApply of 'trm
(* Automation tactics *)
| TacTrivial of debug * 'trm list * string list option
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d1620ca8a7..4ac7a5bffe 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -533,8 +533,6 @@ GEXTEND Gram
| IDENT "intro" -> TacIntroMove (None, MoveLast)
| IDENT "exact"; c = constr -> TacExact c
- | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
- | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
| IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
@@ -548,10 +546,8 @@ GEXTEND Gram
TacElim (false,cl,el)
| IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
TacElim (true,cl,el)
- | IDENT "elimtype"; c = constr -> TacElimType c
| IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
| IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
- | IDENT "casetype"; c = constr -> TacCaseType c
| "fix"; n = natural -> TacFix (None,n)
| "fix"; id = ident; n = natural -> TacFix (Some id,n)
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
@@ -587,7 +583,6 @@ GEXTEND Gram
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
TacAssert (None,ipat,c)
- | IDENT "cut"; c = constr -> TacCut c
| IDENT "generalize"; c = constr ->
TacGeneralize [((AllOccurrences,c),Names.Anonymous)]
| IDENT "generalize"; c = constr; l = LIST1 constr ->
@@ -601,7 +596,6 @@ GEXTEND Gram
| IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
- | IDENT "lapply"; c = constr -> TacLApply c
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c7644f8c60..0ea8b4048c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -650,8 +650,6 @@ and pr_atom1 = function
hov 1 (str"intro" ++ pr_opt pr_id ido ++
Miscprint.pr_move_location pr_ident hto)
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
- | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
- | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
| TacApply (a,ev,cb,inhyp) ->
hov 1 ((if a then mt() else str "simple ") ++
str (with_evars ev "apply") ++ spc () ++
@@ -660,10 +658,8 @@ and pr_atom1 = function
| TacElim (ev,cb,cbo) ->
hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
pr_opt pr_eliminator cbo)
- | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
| TacCase (ev,cb) ->
hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
- | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
| TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
| TacMutualFix (id,n,l) ->
hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
@@ -672,7 +668,6 @@ and pr_atom1 = function
| TacMutualCofix (id,l) ->
hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
str"with " ++ prlist_with_sep spc pr_cofix_tac l)
- | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
| TacAssert (Some tac,ipat,c) ->
hov 1 (str "assert" ++
pr_assumption pr_lconstr pr_constr ipat c ++
@@ -734,8 +729,6 @@ and pr_atom1 = function
| TacSpecialize (n,c) ->
hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++
pr_with_bindings c)
- | TacLApply c ->
- hov 1 (str "lapply" ++ pr_constrarg c)
(* Automation tactics *)
| TacTrivial (_,[],Some []) as x -> pr_atom0 x
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 0170b68014..2434d3f453 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -8,6 +8,11 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+open Util
+open Names
+open Tacexpr
+open Tacinterp
+
DECLARE PLUGIN "coretactics"
TACTIC EXTEND reflexivity
@@ -17,3 +22,59 @@ END
TACTIC EXTEND assumption
[ "assumption" ] -> [ Tactics.assumption ]
END
+
+let make_vars len =
+ List.init len (fun i -> Id.of_string (Printf.sprintf "_%i" i))
+
+let dummy_id = Id.of_string "_"
+
+(** Add a tactic that only uses constrs arguments. Such tactics actually do
+ not need to define grammar rules, because tactic arguments are already
+ parsed as constrs. So we add them manually. *)
+(** TODO: do this automagically in TACTIC EXTEND and use it in this file *)
+let add_constr_tactic name len tac =
+ let vars = make_vars len in
+ (** We pass the arguments through the environment rather than through the
+ tactic, to overcome the way tactics arguments are interpreted. *)
+ let tac _ ist = Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let map id =
+ let c = Id.Map.find id ist.lfun in
+ try Taccoerce.coerce_to_closed_constr env c
+ with Taccoerce.CannotCoerceTo ty ->
+ error_ltac_variable Loc.ghost dummy_id (Some env) c ty
+ in
+ let args = List.map map vars in
+ tac args ist
+ end in
+ let () = Tacenv.register_ml_tactic name tac in
+ let ref = Libnames.Ident (Loc.ghost, Id.of_string name) in
+ let args = List.map (fun id -> Some id) vars in
+ let body = TacExtend (Loc.ghost, name, []) in
+ let body = TacFun (args, TacAtom (Loc.ghost, body)) in
+ let obj () = Tacenv.register_ltac false false [ref, false, body] in
+ Mltop.declare_cache_obj obj "coretactics"
+
+let () =
+ let tac args _ = match args with [c] _ -> Tactics.cut c | _ -> assert false in
+ add_constr_tactic "cut" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.exact_no_check c) | _ -> assert false in
+ add_constr_tactic "exact_no_check" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.vm_cast_no_check c) | _ -> assert false in
+ add_constr_tactic "vm_cast_no_check" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.case_type c) | _ -> assert false in
+ add_constr_tactic "casetype" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.elim_type c) | _ -> assert false in
+ add_constr_tactic "elimtype" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Tactics.cut_and_apply c | _ -> assert false in
+ add_constr_tactic "lapply" 1 tac
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ea3e346853..22ea274cb7 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -456,17 +456,13 @@ let rec intern_atomic lf ist x =
TacIntroMove (Option.map (intern_ident lf ist) ido,
intern_move_location ist hto)
| TacExact c -> TacExact (intern_constr ist c)
- | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
- | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
| TacApply (a,ev,cb,inhyp) ->
TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
Option.map (intern_in_hyp_as ist lf) inhyp)
| TacElim (ev,cb,cbo) ->
TacElim (ev,intern_constr_with_bindings ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
- | TacElimType c -> TacElimType (intern_type ist c)
| TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
- | TacCaseType c -> TacCaseType (intern_type ist c)
| TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
| TacMutualFix (id,n,l) ->
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
@@ -475,7 +471,6 @@ let rec intern_atomic lf ist x =
| TacMutualCofix (id,l) ->
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
TacMutualCofix (intern_ident lf ist id, List.map f l)
- | TacCut c -> TacCut (intern_type ist c)
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_pure_tactic ist) otac,
Option.map (intern_intro_pattern lf ist) ipat,
@@ -516,7 +511,6 @@ let rec intern_atomic lf ist x =
| TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
TacDecompose (l,intern_constr ist c)
| TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
- | TacLApply c -> TacLApply (intern_constr ist c)
(* Context management *)
| TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d72a37d33e..4333c5696d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1455,12 +1455,6 @@ and interp_atomic ist tac =
(Tactics.exact_no_check c_interp)
gl
end
- | TacExactNoCheck c ->
- (new_interp_constr ist c)
- (fun c -> Proofview.V82.tactic (Tactics.exact_no_check c))
- | TacVmCastNoCheck c ->
- (new_interp_constr ist c)
- (fun c -> Proofview.V82.tactic (Tactics.vm_cast_no_check c))
| TacApply (a,ev,cb,cl) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1487,14 +1481,6 @@ and interp_atomic ist tac =
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
end
- | TacElimType c ->
- Proofview.V82.tactic begin fun gl ->
- let (sigma,c_interp) = pf_interp_type ist gl c in
- tclTHEN
- (tclEVARS sigma)
- (Tactics.elim_type c_interp)
- gl
- end
| TacCase (ev,cb) ->
Proofview.Goal.raw_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
@@ -1502,14 +1488,6 @@ and interp_atomic ist tac =
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb
end
- | TacCaseType c ->
- Proofview.V82.tactic begin fun gl ->
- let (sigma,c_interp) = pf_interp_type ist gl c in
- tclTHEN
- (tclEVARS sigma)
- (Tactics.case_type c_interp)
- gl
- end
| TacFix (idopt,n) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1548,8 +1526,6 @@ and interp_atomic ist tac =
(Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0)
gl
end
- | TacCut c ->
- new_interp_type ist c Tactics.cut
| TacAssert (t,ipat,c) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1670,8 +1646,6 @@ and interp_atomic ist tac =
tclWITHHOLES false (Tactics.specialize n) sigma cb gl
end
end
- | TacLApply c ->
- new_interp_constr ist c Tactics.cut_and_apply
(* Context management *)
| TacClear (b,l) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 31a1b57bc0..4d0b595690 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -135,23 +135,18 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Basic tactics *)
| TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
| TacExact c -> TacExact (subst_glob_constr subst c)
- | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
- | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
| TacApply (a,ev,cb,cl) ->
TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
| TacElim (ev,cb,cbo) ->
TacElim (ev,subst_glob_with_bindings subst cb,
Option.map (subst_glob_with_bindings subst) cbo)
- | TacElimType c -> TacElimType (subst_glob_constr subst c)
| TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
- | TacCaseType c -> TacCaseType (subst_glob_constr subst c)
| TacFix (idopt,n) as x -> x
| TacMutualFix (id,n,l) ->
TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
| TacCofix idopt as x -> x
| TacMutualCofix (id,l) ->
TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
- | TacCut c -> TacCut (subst_glob_constr subst c)
| TacAssert (b,na,c) ->
TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
| TacGeneralize cl ->
@@ -177,7 +172,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
let l = List.map (subst_or_var (subst_ind subst)) l in
TacDecompose (l,subst_glob_constr subst c)
| TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l)
- | TacLApply c -> TacLApply (subst_glob_constr subst c)
(* Context management *)
| TacClear _ as x -> x
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:42:11 +0000