aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/pltac.mli2
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--plugins/ltac/tacarg.mli6
-rw-r--r--plugins/ltac/tacexpr.ml18
-rw-r--r--plugins/ltac/tacexpr.mli18
-rw-r--r--plugins/ltac/tacinterp.ml3
-rw-r--r--plugins/ltac/tactic_debug.ml13
9 files changed, 37 insertions, 35 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 2e90ce90cc..a5f8060aee 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -296,7 +296,6 @@ let project_hint ~poly pri l2r r =
let env = Global.env() in
let sigma = Evd.from_env env in
let sigma, c = Evd.fresh_global env sigma gr in
- let c = EConstr.of_constr c in
let t = Retyping.get_type_of env sigma c in
let t =
Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
@@ -307,7 +306,6 @@ let project_hint ~poly pri l2r r =
let p =
if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
let sigma, p = Evd.fresh_global env sigma p in
- let p = EConstr.of_constr p in
let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
let c = it_mkLambda_or_LetIn
(mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 6637de745e..434feba95c 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -25,7 +25,7 @@ val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eva
val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
val uconstr : constr_expr Gram.entry
val quantified_hypothesis : quantified_hypothesis Gram.entry
-val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
+val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
val int_or_var : int or_var Gram.entry
val simple_tactic : raw_tactic_expr Gram.entry
val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5951f2b119..aea00c240b 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -84,7 +84,7 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d32a2faefc..9eb55aa5e5 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -428,7 +428,8 @@ let split_head = function
| [] -> assert(false)
let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
- pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
+ let equal x y = Constr.equal (EConstr.Unsafe.to_constr x) (EConstr.Unsafe.to_constr y) in
+ pb == pb' || (ty == ty' && equal x x' && equal y y')
let problem_inclusion x y =
List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -626,9 +627,9 @@ let solve_remaining_by env sigma holes by =
(** Evar should not be defined, but just in case *)
| Some evi ->
let env = Environ.reset_with_named_context evi.evar_hyps env in
- let ty = EConstr.of_constr evi.evar_concl in
+ let ty = evi.evar_concl in
let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
- Evd.define evk c sigma
+ Evd.define evk (EConstr.of_constr c) sigma
in
List.fold_left solve sigma indep
@@ -1862,7 +1863,6 @@ let declare_projection n instance_id r =
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma,c = Evd.fresh_global env sigma r in
- let c = EConstr.of_constr c in
let ty = Retyping.get_type_of env sigma c in
let term = proper_projection sigma c ty in
let sigma, typ = Typing.type_of env sigma term in
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 5347eda7d7..59473a5e57 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -23,7 +23,7 @@ val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_typ
val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
val wit_destruction_arg :
- (constr_expr with_bindings Tacexpr.destruction_arg,
- glob_constr_and_expr with_bindings Tacexpr.destruction_arg,
- delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type
+ (constr_expr with_bindings Tactics.destruction_arg,
+ glob_constr_and_expr with_bindings Tactics.destruction_arg,
+ delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 8b0c44041f..3baa475aba 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector =
| SelectList of (int * int) list
| SelectId of Id.t
| SelectAll
+[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
-type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of lident
| ElimOnAnonHyp of int
+[@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
type 'a destruction_arg =
- clear_flag * 'a core_destruction_arg
+ clear_flag * 'a Tactics.core_destruction_arg
+[@@ocaml.deprecated "Use Tactics.destruction_arg"]
-type inversion_kind = Misctypes.inversion_kind =
+type inversion_kind = Inv.inversion_kind =
| SimpleInversion
| FullInversion
| FullInversionClear
+[@@ocaml.deprecated "Use Tactics.inversion_kind"]
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
- inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
+ Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
| DepInversion of
- inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
+ Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -69,7 +73,7 @@ type 'id message_token =
| MsgIdent of 'id
type ('dconstr,'id) induction_clause =
- 'dconstr with_bindings destruction_arg *
+ 'dconstr with_bindings Tactics.destruction_arg *
(intro_pattern_naming_expr CAst.t option (* eqn:... *)
* 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
* 'id clause_expr option (* in ... *)
@@ -265,7 +269,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of goal_selector * 'a gen_tactic_expr
+ | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8b0c44041f..3baa475aba 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector =
| SelectList of (int * int) list
| SelectId of Id.t
| SelectAll
+[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
-type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of lident
| ElimOnAnonHyp of int
+[@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
type 'a destruction_arg =
- clear_flag * 'a core_destruction_arg
+ clear_flag * 'a Tactics.core_destruction_arg
+[@@ocaml.deprecated "Use Tactics.destruction_arg"]
-type inversion_kind = Misctypes.inversion_kind =
+type inversion_kind = Inv.inversion_kind =
| SimpleInversion
| FullInversion
| FullInversionClear
+[@@ocaml.deprecated "Use Tactics.inversion_kind"]
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
- inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
+ Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
| DepInversion of
- inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
+ Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -69,7 +73,7 @@ type 'id message_token =
| MsgIdent of 'id
type ('dconstr,'id) induction_clause =
- 'dconstr with_bindings destruction_arg *
+ 'dconstr with_bindings Tactics.destruction_arg *
(intro_pattern_naming_expr CAst.t option (* eqn:... *)
* 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
* 'id clause_expr option (* in ... *)
@@ -265,7 +269,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of goal_selector * 'a gen_tactic_expr
+ | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6a4bf577b1..84049d4ed5 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2010,7 +2010,8 @@ let interp_redexp env sigma r =
let _ =
let eval lfun env sigma ty tac =
- let ist = { lfun = lfun; extra = TacStore.empty; } in
+ let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
+ let ist = { lfun = lfun; extra; } in
let tac = interp_tactic ist tac in
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index e55b49fb4e..105b5c59ae 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -391,19 +391,14 @@ let explain_ltac_call_trace last trace loc =
let skip_extensions trace =
let rec aux = function
- | (_,Tacexpr.LtacNameCall f as tac) :: _
- when Tacenv.is_ltac_for_ml_tactic f -> [tac]
- | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
+ | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: tail ->
(* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
(* see tacextend.mlp *)
- [tac]
- | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
+ tac :: aux tail
| t :: tail -> t :: aux tail
| [] -> [] in
List.rev (aux (List.rev trace))
-let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2
-
let extract_ltac_trace ?loc trace =
let trace = skip_extensions trace in
let (tloc,c),tail = List.sep_last trace in
@@ -411,7 +406,7 @@ let extract_ltac_trace ?loc trace =
(* We entered a user-defined tactic,
we display the trace with location of the call *)
let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in
- (if finer_loc loc tloc then loc else tloc), Some msg
+ (if Loc.finer loc tloc then loc else tloc), Some msg
else
(* We entered a primitive tactic, we don't display trace but
report on the finest location *)
@@ -420,7 +415,7 @@ let extract_ltac_trace ?loc trace =
let rec aux best_loc = function
| (loc,_)::tail ->
if Option.is_empty best_loc ||
- not (Option.is_empty loc) && finer_loc loc best_loc
+ not (Option.is_empty loc) && Loc.finer loc best_loc
then
aux loc tail
else
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:23:44 +0000