aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrbool.v2
-rw-r--r--plugins/ssr/ssrbwd.ml3
-rw-r--r--plugins/ssr/ssrcommon.ml78
-rw-r--r--plugins/ssr/ssrcommon.mli7
-rw-r--r--plugins/ssr/ssrequality.ml13
-rw-r--r--plugins/ssr/ssrfun.v2
-rw-r--r--plugins/ssr/ssrparser.mlg10
7 files changed, 8 insertions, 107 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index a618fc781f..3a7cf41d43 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr.
Lemma is_true_true : true. Proof. by []. Qed.
Lemma not_false_is_true : ~ false. Proof. by []. Qed.
Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
-Hint Resolve is_true_true not_false_is_true is_true_locked_true.
+Hint Resolve is_true_true not_false_is_true is_true_locked_true : core.
(** Shorter names. **)
Definition isT := is_true_true.
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 1c4508abf4..3e0fbc9a8c 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -104,8 +104,6 @@ let mkRAppView ist gl rv gv =
let nb_view_imps = interp_view_nbimps ist gl rv in
mkRApp rv (mkRHoles (abs nb_view_imps))
-let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";;
-
let refine_interp_apply_view dbl ist gl gv =
let pair i = List.map (fun x -> i, x) in
let rv = pf_intern_term ist gl gv in
@@ -113,7 +111,6 @@ let refine_interp_apply_view dbl ist gl gv =
let interp_with (dbl, hint) =
let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in
interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
- let interp_with x = prof_apply_interp_with.profile interp_with x in
let rec loop = function
| [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
| h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index be8f3603e4..fa58a1c39a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -242,7 +242,6 @@ let interp_refine ist gl rc =
let flags = {
Pretyping.use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = None;
fail_evar = false;
expand_evars = true }
in
@@ -860,7 +859,7 @@ let ssr_n_tac seed n gl =
with Not_found ->
if n = -1 then fail "The ssreflect library was not loaded"
else fail ("The tactic "^name^" was not found") in
- let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+ let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl
let donetac n gl = ssr_n_tac "done" n gl
@@ -1018,81 +1017,6 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
with e when CErrors.noncritical e -> raise dependent_apply_error
-(** Profiling *)(* {{{ *************************************************************)
-type profiler = {
- profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
- reset : unit -> unit;
- print : unit -> unit }
-let profile_now = ref false
-let something_profiled = ref false
-let profilers = ref []
-let add_profiler f = profilers := f :: !profilers;;
-let _ =
- Goptions.declare_bool_option
- { Goptions.optname = "ssreflect profiling";
- Goptions.optkey = ["SsrProfiling"];
- Goptions.optread = (fun _ -> !profile_now);
- Goptions.optdepr = false;
- Goptions.optwrite = (fun b ->
- Ssrmatching.profile b;
- profile_now := b;
- if b then List.iter (fun f -> f.reset ()) !profilers;
- if not b then List.iter (fun f -> f.print ()) !profilers) }
-let () =
- let prof_total =
- let init = ref 0.0 in {
- profile = (fun f x -> assert false);
- reset = (fun () -> init := Unix.gettimeofday ());
- print = (fun () -> if !something_profiled then
- prerr_endline
- (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
- "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in
- let prof_legenda = {
- profile = (fun f x -> assert false);
- reset = (fun () -> ());
- print = (fun () -> if !something_profiled then begin
- prerr_endline
- (Printf.sprintf "!! %39s ---------- --------- --------- ---------"
- (String.make 39 '-'));
- prerr_endline
- (Printf.sprintf "!! %-39s %10s %9s %9s %9s"
- "function" "#calls" "total" "max" "average") end) } in
- add_profiler prof_legenda;
- add_profiler prof_total
-;;
-
-let mk_profiler s =
- let total, calls, max = ref 0.0, ref 0, ref 0.0 in
- let reset () = total := 0.0; calls := 0; max := 0.0 in
- let profile f x =
- if not !profile_now then f x else
- let before = Unix.gettimeofday () in
- try
- incr calls;
- let res = f x in
- let after = Unix.gettimeofday () in
- let delta = after -. before in
- total := !total +. delta;
- if delta > !max then max := delta;
- res
- with exc ->
- let after = Unix.gettimeofday () in
- let delta = after -. before in
- total := !total +. delta;
- if delta > !max then max := delta;
- raise exc in
- let print () =
- if !calls <> 0 then begin
- something_profiled := true;
- prerr_endline
- (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
- s !calls !total !max (!total /. (float_of_int !calls))) end in
- let prof = { profile = profile; reset = reset; print = print } in
- add_profiler prof;
- prof
-;;
-(* }}} *)
-
(* We wipe out all the keywords generated by the grammar rules we defined. *)
(* The user is supposed to Require Import ssreflect or Require ssreflect *)
(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index cf4e4b354e..e92489e568 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -378,13 +378,6 @@ val pf_interp_gen_aux :
val is_name_in_ipats :
Id.t -> ssripats -> bool
-type profiler = {
- profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
- reset : unit -> unit;
- print : unit -> unit }
-
-val mk_profiler : string -> profiler
-
(** Basic tactics *)
val introid : ?orig:Name.t ref -> Id.t -> v82tac
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 2a69e3f23a..22475fef34 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -425,11 +425,6 @@ let rwcltac cl rdx dir sr gl =
in
tclTHEN cvtac' rwtac gl
-let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";;
-let rwcltac cl rdx dir sr gl =
- prof_rwcltac.profile (rwcltac cl rdx dir sr) gl
-;;
-
[@@@ocaml.warning "-3"]
let lz_coq_prod =
@@ -455,8 +450,6 @@ let ssr_is_setoid env =
Rewrite.is_applied_rewrite_relation env
sigma [] (EConstr.mkApp (r, args)) <> None
-let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";;
-
let closed0_check cl p gl =
if closed0 cl then
errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p)
@@ -556,7 +549,6 @@ let rwrxtac occ rdx_pat dir rule gl =
d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r)
with _ -> rwtac rs in
rwtac rules in
- let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in
let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
let find_R, conclude = match rdx_pat with
| Some (_, (In_T _ | In_X_In_T _)) | None ->
@@ -582,11 +574,6 @@ let rwrxtac occ rdx_pat dir rule gl =
rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
;;
-let prof_rwxrtac = mk_profiler "rwrxtac";;
-let rwrxtac occ rdx_pat dir rule gl =
- prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
-;;
-
let ssrinstancesofrule ist dir arg gl =
let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
let rule = interp_term ist gl arg in
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index e2c0ed7c8b..6535cad8b7 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -398,7 +398,7 @@ End ExtensionalEquality.
Typeclasses Opaque eqfun.
Typeclasses Opaque eqrel.
-Hint Resolve frefl rrefl.
+Hint Resolve frefl rrefl : core.
Notation "f1 =1 f2" := (eqfun f1 f2)
(at level 70, no associativity) : fun_scope.
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 52240f5896..7c91860228 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1545,9 +1545,9 @@ let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
let swaptacarg (loc, b) = (b, []), Some (TacId [])
let check_seqtacarg dir arg = match snd arg, dir with
- | ((true, []), Some (TacAtom (loc, _))), L2R ->
+ | ((true, []), Some (TacAtom { CAst.loc })), L2R ->
CErrors.user_err ?loc (str "expected \"last\"")
- | ((false, []), Some (TacAtom (loc, _))), R2L ->
+ | ((false, []), Some (TacAtom { CAst.loc })), R2L ->
CErrors.user_err ?loc (str "expected \"first\"")
| _, _ -> arg
@@ -1677,7 +1677,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
| ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
let tacname = ssrtac_name name in () *)
-let ssrtac_atom ?loc name args = TacML (Loc.tag ?loc (ssrtac_entry name 0, args))
+let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args))
let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args
let tclintros_expr ?loc tac ipats =
@@ -1704,7 +1704,7 @@ END
GRAMMAR EXTEND Gram
GLOBAL: tactic_expr;
- ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { Loc.tag ~loc (Tacexp tac) } ]];
+ ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
END
@@ -1724,7 +1724,7 @@ let ssrautoprop gl =
let tacname =
try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
- let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+ let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
with Not_found -> V82.of_tactic (Auto.full_trivial []) gl
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:15:50 +0000