aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/ltac/pltac.mli2
-rw-r--r--plugins/ltac/pptactic.mli2
-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/tactic_debug.ml7
-rw-r--r--plugins/micromega/Tauto.v4
-rw-r--r--plugins/ssr/ssripats.ml10
-rw-r--r--plugins/ssr/ssrparser.ml413
11 files changed, 44 insertions, 42 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 49f7aae435..319b410df0 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1512,7 +1512,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1527,7 +1527,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2743a8a2f9..ae84eaa93e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -969,7 +969,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
- Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
+ Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
(fun g ->
let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
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/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/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index e55b49fb4e..57a11d9477 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -391,13 +391,10 @@ 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))
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 31f55ae9c3..458844e1b9 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -211,7 +211,7 @@ Set Implicit Arguments.
(* BC *)
simpl.
case_eq (deduce t t) ; auto.
- intros until 0.
+ intros *.
case_eq (unsat t0) ; auto.
unfold eval_clause.
rewrite make_conj_cons.
@@ -263,7 +263,7 @@ Set Implicit Arguments.
Proof.
induction cl.
simpl. tauto.
- intros until 0.
+ intros *.
simpl.
assert (HH := add_term_correct env a cl').
case_eq (add_term a cl').
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 42566575c0..7897cb1700 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -133,6 +133,12 @@ let intro_clear ids future_ipats =
isCLR_PUSHL clear_ids
end
+let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
+ let ctx = Goal.hyps gl in
+ List.iter (Ssrcommon.check_hyp_exists ctx) hyps;
+ tclUNIT ()
+end
+
(** [=> []] *****************************************************************)
let tac_case t =
Goal.enter begin fun _ ->
@@ -229,7 +235,9 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatNoop -> tclUNIT ()
| IPatSimpl Nop -> tclUNIT ()
- | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+ | IPatClear ids ->
+ tacCHECK_HYPS_EXIST ids <*>
+ intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
| IPatSimpl (Simpl n) ->
V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 0d82a9f096..5f39674407 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -585,21 +585,10 @@ let pr_ssripat _ _ _ = pr_ipat
let pr_ssripats _ _ _ = pr_ipats
let pr_ssriorpat _ _ _ = pr_iorpat
-(*
-let intern_ipat ist ipat =
- let rec check_pat = function
- | IPatClear clr -> ignore (List.map (intern_hyp ist) clr)
- | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat
- | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat
- | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat
- | _ -> () in
- check_pat ipat; ipat
-*)
-
let intern_ipat ist =
map_ipat
(fun id -> id)
- (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *)
+ (intern_hyp ist)
(glob_ast_closure_term ist)
let intern_ipats ist = List.map (intern_ipat ist)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:07:21 +0000