aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_class.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg12
-rw-r--r--plugins/ltac/leminv.ml17
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/profile_ltac_tactics.mlg4
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacinterp.ml3
10 files changed, 24 insertions, 30 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index cb226de586..f1f538ab39 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -263,7 +263,7 @@ END
(** Double induction *)
-TACTIC EXTEND double_induction
+TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
{ Elim.h_double_induction h1 h2 }
END
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 66c72a30a2..4f20e5a800 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin"
(**********************************************************************)
(* replace, discriminate, injection, simplify_eq *)
-(* cutrewrite, dependent rewrite *)
+(* dependent rewrite *)
let with_delayed_uconstr ist c tac =
let flags = {
@@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite
-> { rewriteInHyp b c id }
END
-TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn }
-| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
- -> { cutRewriteInHyp b eqn id }
-END
-
(**********************************************************************)
(* Decompose *)
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 35c90444b1..8d197e6056 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 114acaa412..78cde2cde8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram
message_token:
[ [ id = identref -> { MsgIdent id }
| s = STRING -> { MsgString s }
- | n = integer -> { MsgInt n } ] ]
+ | n = natural -> { MsgInt n } ] ]
;
ltac_def_kind:
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fa176482bf..a6673699af 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" natural(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
@@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
-| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 0024d1a4ba..47df3ec34f 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -228,14 +228,15 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let p = EConstr.to_constr sigma invProof in
- p, sigma
+ invProof, sigma
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
- let univs = Evd.univ_entry ~poly sigma in
- let entry = Declare.definition_entry ~univs invProof in
- let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+ let cinfo = Declare.CInfo.make ~name ~typ:None () in
+ let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in
+ let _ : Names.GlobRef.t =
+ Declare.declare_definition ~cinfo ~info ~opaque:false ~body:invProof sigma
+ in
()
(* inv_op = Inv (derives de complete inv. lemma)
@@ -246,11 +247,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
let sigma = Evd.from_env env in
let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
- try
- add_inversion_lemma ~poly na env sigma c sort bool tac
- with
- | UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
- user_err ~hdr:"Inv needs Nodep Prop Set" s
+ add_inversion_lemma ~poly na env sigma c sort bool tac
(* ================================= *)
(* Applying a given inversion lemma *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6233807016..f69fe064a7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s =
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
| TacChange (check,op,c,h) ->
- let name = if check then "change_no_check" else "change" in
+ let name = if check then "change" else "change_no_check" in
hov 1 (
primitive name ++ brk (1,1)
++ (
diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg
index eb9d9cbdce..e5309ea441 100644
--- a/plugins/ltac/profile_ltac_tactics.mlg
+++ b/plugins/ltac/profile_ltac_tactics.mlg
@@ -55,7 +55,7 @@ END
TACTIC EXTEND show_ltac_profile
| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
+| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s }
END
@@ -74,7 +74,7 @@ END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) }
+| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) }
END
VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fb149071c9..a1dbf9a439 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -546,7 +546,7 @@ let rewrite_core_unif_flags = {
Unification.check_applied_meta_types = true;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.allowed_evars = Unification.AllowAll;
+ Unification.allowed_evars = Evarsolve.AllowedEvars.all;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 88480194c8..2258201c22 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2028,6 +2028,9 @@ let () =
declare_uniform wit_int
let () =
+ declare_uniform wit_nat
+
+let () =
declare_uniform wit_bool
let () =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 08:16:55 +0000