aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg6
-rw-r--r--plugins/ltac/g_tactic.mlg21
-rw-r--r--plugins/ltac/pptactic.ml3
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacarg.ml2
-rw-r--r--plugins/ltac/taccoerce.ml7
-rw-r--r--plugins/ltac/tacsubst.ml10
-rw-r--r--plugins/ltac/tauto.ml27
12 files changed, 38 insertions, 50 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 2654729652..e6e6e29d4f 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
let local_test_lpar_id_colon =
let err () = raise Stream.Failure in
Pcoq.Entry.of_parser "lpar_id_colon"
- (fun strm ->
+ (fun _ strm ->
match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" ->
(match Util.stream_nth 1 strm with
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 21d61d1f97..f7215a9d13 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1100,7 +1100,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) }
+| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5c84b35f1b..cab8ed0a55 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -64,7 +64,7 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
Pcoq.Entry.of_parser "test_bracket_ident"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "[" ->
(match stream_nth 1 strm with
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 455c8ab003..61cc77c42a 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -145,7 +145,7 @@ open Pp
VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> {
- Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) }
+ Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
END
VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
@@ -154,8 +154,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
END
VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_info (show_term None) }
+| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
+| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
END
{
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 945a2dd613..1b00a93834 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -24,7 +24,6 @@ open Tactypes
open Tactics
open Inv
open Locus
-open Decl_kinds
open Pcoq
@@ -40,7 +39,7 @@ let err () = raise Stream.Failure
(* admissible notation "(x t)" *)
let test_lpar_id_coloneq =
Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -54,7 +53,7 @@ let test_lpar_id_coloneq =
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -68,7 +67,7 @@ let test_lpar_id_rpar =
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -85,7 +84,7 @@ open Extraargs
(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
Pcoq.Entry.of_parser "lpar_id_colon"
- (fun strm ->
+ (fun _ strm ->
let rec skip_to_rpar p n =
match List.last (Stream.npeek n strm) with
| KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
@@ -109,7 +108,7 @@ let check_for_coloneq =
let lookup_at_as_comma =
Pcoq.Entry.of_parser "lookup_at_as_comma"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD (","|"at"|"as") -> ()
| _ -> err ())
@@ -183,10 +182,6 @@ let mkCLambdaN_simple bl c = match bl with
let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc
-let map_int_or_var f = function
- | ArgArg x -> ArgArg (f x)
- | ArgVar _ as y -> y
-
let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
let merge_occurrences loc cl = function
@@ -270,7 +265,7 @@ GRAMMAR EXTEND Gram
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
| "-"; n = nat_or_var; nl = LIST0 int_or_var ->
(* have used int_or_var instead of nat_or_var for compatibility *)
- { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ]
+ { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
;
occs:
[ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
@@ -450,9 +445,9 @@ GRAMMAR EXTEND Gram
| -> { true } ] ]
;
simple_binder:
- [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@
+ [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@
CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) }
- | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) }
+ | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) }
] ]
;
fixdecl:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 0e38ce575b..6df068883c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -20,7 +20,6 @@ open Stdarg
open Notation_gram
open Tactypes
open Locus
-open Decl_kinds
open Genredexpr
open Ppconstr
open Pputils
@@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s =
let rec strip_ty acc n ty =
if Int.equal n 0 then (List.rev acc, (ty,None)) else
match DAst.get ty with
- Glob_term.GProd(na,Explicit,a,b) ->
+ Glob_term.GProd(na,Glob_term.Explicit,a,b) ->
strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9d46bbc74e..fe5ebf1172 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -417,7 +417,7 @@ let get_timer name =
let finish_timing ~prefix name =
let tend = System.get_time () in
let tstart = get_timer name in
- Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+ Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
System.fmt_time_difference tstart tend)
(* ******************** *)
@@ -431,7 +431,7 @@ let print_results_filter ~cutoff ~filter =
let results =
SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
let results = merge_roots results Local.(CList.last !stack) in
- Feedback.msg_info (to_string ~cutoff ~filter results)
+ Feedback.msg_notice (to_string ~cutoff ~filter results)
;;
let print_results ~cutoff =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 726752a2bf..1493092f2f 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.frozen_evars = Evar.Set.empty;
+ Unification.allowed_evars = Unification.AllowAll;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 9e8e86d4fc..252c15478d 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -20,7 +20,7 @@ let make0 ?dyn name =
wit
let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *)
-let wit_simple_intropattern = make0 "simple_intropattern"
+let wit_simple_intropattern = make0 ~dyn:(val_tag (topwit wit_intropattern)) "simple_intropattern"
let wit_quant_hyp = make0 "quant_hyp"
let wit_constr_with_bindings = make0 "constr_with_bindings"
let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index e64129d204..da89a027e2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -145,11 +145,8 @@ let coerce_to_constr_context v =
else raise (CannotCoerceTo "a term context")
let is_intro_pattern v =
- if has_type v (topwit wit_intropattern [@warning "-3"]) then
- Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v
- else
- if has_type v (topwit wit_simple_intropattern) then
- Some (out_gen (topwit wit_simple_intropattern) v).CAst.v
+ if has_type v (topwit wit_intro_pattern) then
+ Some (out_gen (topwit wit_intro_pattern) v).CAst.v
else
None
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b6e7dd64b0..bf5d49f678 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -76,25 +76,21 @@ let subst_and_short_name f (c,n) =
(* assert (n=None); *)(* since tacdef are strictly globalized *)
(f c,None)
-let subst_or_var f = let open Locus in function
- | ArgVar _ as x -> x
- | ArgArg x -> ArgArg (f x)
-
let subst_located f = Loc.map f
let subst_reference subst =
- subst_or_var (subst_located (subst_kn subst))
+ Locusops.or_var_map (subst_located (subst_kn subst))
(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
to the syntactic non-terminals "global", used in commands such as
Print. It is also used for non-evaluable references. *)
let subst_global_reference subst =
- subst_or_var (subst_located (subst_global_reference subst))
+ Locusops.or_var_map (subst_located (subst_global_reference subst))
let subst_evaluable subst =
let subst_eval_ref = subst_evaluable_reference subst in
- subst_or_var (subst_and_short_name subst_eval_ref)
+ Locusops.or_var_map (subst_and_short_name subst_eval_ref)
let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 94af4a3151..ba759441e5 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -189,31 +189,32 @@ let flatten_contravariant_disj _ ist =
tclTHEN (tclTHENLIST tacs) tac0
| _ -> fail
-let make_unfold name =
- let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
- let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
- Locus.(AllOccurrences, ArgArg (EvalConstRef const, None))
+let evalglobref_of_globref =
+ function
+ | GlobRef.VarRef v -> EvalVarRef v
+ | GlobRef.ConstRef c -> EvalConstRef c
+ | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> assert false
-let u_not = make_unfold "not"
+let make_unfold name =
+ let const = evalglobref_of_globref (Coqlib.lib_ref name) in
+ Locus.(AllOccurrences, ArgArg (const, None))
let reduction_not_iff _ ist =
let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
let tac = match !negation_unfolding with
- | true -> make_reduce [u_not]
+ | true -> make_reduce [make_unfold "core.not.type"]
| false -> TacId []
in
eval_tactic_ist ist tac
-let coq_nnpp_path =
- let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in
- Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP")
-
let apply_nnpp _ ist =
+ let nnpp = "core.nnpp.type" in
Proofview.tclBIND
(Proofview.tclUNIT ())
- begin fun () -> try
- Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply
- with Not_found -> tclFAIL 0 (Pp.mt ())
+ begin fun () ->
+ if Coqlib.has_ref nnpp
+ then Tacticals.New.pf_constr_of_global (Coqlib.lib_ref nnpp) >>= apply
+ else tclFAIL 0 (Pp.mt ())
end
(* This is the uniform mode dealing with ->, not, iff and types isomorphic to
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 17:02:12 +0000