aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh12
-rw-r--r--intf/misctypes.ml13
-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--tactics/equality.mli10
-rw-r--r--tactics/inv.ml5
-rw-r--r--tactics/inv.mli5
-rw-r--r--tactics/tactics.ml7
-rw-r--r--tactics/tactics.mli8
13 files changed, 70 insertions, 38 deletions
diff --git a/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh
new file mode 100644
index 000000000..cf2af9ae9
--- /dev/null
+++ b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "6960" ] || [ "$CI_BRANCH" = "ltac+tacdepr" ]; then
+
+ # Equations_CI_BRANCH=ssr+correct_packing
+ # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ ltac2_CI_BRANCH=ltac+tacdepr
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ # Elpi_CI_BRANCH=ssr+correct_packing
+ # Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 9eb6f62cc..72db3b31c 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -142,19 +142,6 @@ type multi =
| RepeatStar
| RepeatPlus
-type 'a core_destruction_arg =
- | ElimOnConstr of 'a
- | ElimOnIdent of lident
- | ElimOnAnonHyp of int
-
-type 'a destruction_arg =
- clear_flag * 'a core_destruction_arg
-
-type inversion_kind =
- | SimpleInversion
- | FullInversion
- | FullInversionClear
-
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
univdecl_extensible_instance : bool; (* Can new universes be added *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2743a8a2f..ae84eaa93 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 6637de745..434feba95 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 5951f2b11..aea00c240 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 5347eda7d..59473a5e5 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 8b0c44041..3baa475ab 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 8b0c44041..3baa475ab 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/tactics/equality.mli b/tactics/equality.mli
index c0be917a0..ccf454c3e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -80,20 +80,20 @@ val discrConcl : unit Proofview.tactic
val discrHyp : Id.t -> unit Proofview.tactic
val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
(* Below, if flag is [None], it takes the value from the dynamic value of the option *)
val inj : inj_flags option -> intro_patterns option -> evars_flag ->
clear_flag -> constr with_bindings -> unit Proofview.tactic
val injClause : inj_flags option -> intro_patterns option -> evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic
val injConcl : inj_flags option -> unit Proofview.tactic
val simpleInjClause : inj_flags option -> evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
-val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
+val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 067fc8941..d76c9a697 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -64,6 +64,11 @@ let var_occurs_in_pf gl id =
type inversion_status = Dep of constr option | NoDep
+type inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
let compute_eqn env sigma n i ai =
(mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
diff --git a/tactics/inv.mli b/tactics/inv.mli
index c63d57af5..9d4ffdd7b 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -15,6 +15,11 @@ open Tactypes
type inversion_status = Dep of constr option | NoDep
+type inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
val inv_clause :
inversion_kind -> or_and_intro_pattern option -> Id.t list ->
quantified_hypothesis -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0d9f3d821..d0ec3358a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1159,6 +1159,13 @@ let tactic_infer_flags with_evar = {
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
+type 'a core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
let onOpenInductionArg env sigma tac = function
| clear_flag,ElimOnConstr f ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 079baa3ef..7809dbf48 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -95,6 +95,14 @@ val try_intros_until :
(** Apply a tactic on a quantified hypothesis, an hypothesis in context
or a term with bindings *)
+type 'a core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
+
val onInductionArg :
(clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
constr with_bindings destruction_arg -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 12:49:23 +0000