aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml43
-rw-r--r--plugins/extraction/extraction.ml12
-rw-r--r--plugins/extraction/g_extraction.mlg4
-rw-r--r--plugins/extraction/mlutil.ml5
-rw-r--r--plugins/extraction/ocaml.ml26
-rw-r--r--plugins/firstorder/g_ground.mlg2
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg6
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/micromega/micromega.ml8
-rw-r--r--plugins/micromega/micromega.mli4
-rw-r--r--plugins/setoid_ring/newring.ml91
-rw-r--r--plugins/setoid_ring/newring_ast.ml6
-rw-r--r--plugins/setoid_ring/newring_ast.mli6
-rw-r--r--plugins/ssr/ssrvernac.mlg8
15 files changed, 73 insertions, 154 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 3ed843649e..b5be1cdd89 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -437,30 +437,25 @@ let cc_tactic depth additionnal_terms =
let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
discriminate_tac cstr p
| Incomplete ->
- let open Glob_term in
- let env = Proofview.Goal.env gl in
- let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
- let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
- let pr_missing (c, missing) =
- let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
- let holes = List.init missing (fun _ -> hole) in
- Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
- in
- Feedback.msg_info
- (Pp.str "Goal is solvable by congruence but some arguments are missing.");
- Feedback.msg_info
- (Pp.str " Try " ++
- hov 8
- begin
- str "\"congruence with (" ++
- prlist_with_sep
- (fun () -> str ")" ++ spc () ++ str "(")
- pr_missing
- terms_to_complete ++
- str ")\","
- end ++
- Pp.str " replacing metavariables by arbitrary terms.");
- Tacticals.New.tclFAIL 0 (str "Incomplete")
+ let open Glob_term in
+ let env = Proofview.Goal.env gl in
+ let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+ let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
+ let pr_missing (c, missing) =
+ let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+ let holes = List.init missing (fun _ -> hole) in
+ Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+ in
+ let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
+ ++ fnl () ++
+ str " Try " ++
+ hov 8
+ begin
+ str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
+ pr_missing terms_to_complete ++ str ")\","
+ end ++
+ str " replacing metavariables by arbitrary terms.") in
+ Tacticals.New.tclFAIL 0 msg
| Contradiction dis ->
let env = Proofview.Goal.env gl in
let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 78c6255c1e..cca212f332 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -754,18 +754,6 @@ and extract_cst_app env sg mle mlt kn args =
let la = List.length args in
(* The ml arguments, already expunged from known logical ones *)
let mla = make_mlargs env sg mle s args metas in
- let mla =
- if magic1 || lang () != Ocaml then mla
- else
- try
- (* for better optimisations later, we discard dependent args
- of projections and replace them by fake args that will be
- removed during final pretty-print. *)
- let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in
- if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
- else mla
- with e when CErrors.noncritical e -> mla
- in
(* For strict languages, purely logical signatures lead to a dummy lam
(except when [Kill Ktype] everywhere). So a [MLdummy] is left
accordingly. *)
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index e222fbc808..4f077b08b6 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -128,7 +128,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Inline" ]
- -> {Feedback. msg_info (print_extraction_inline ()) }
+ -> {Feedback.msg_notice (print_extraction_inline ()) }
END
VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -150,7 +150,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Blacklist" ]
- -> { Feedback.msg_info (print_extraction_blacklist ()) }
+ -> { Feedback.msg_notice (print_extraction_blacklist ()) }
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index c57daf0047..000df26858 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1547,6 +1547,7 @@ let inline r t =
not (to_keep r) (* The user DOES want to keep it *)
&& not (is_inline_custom r)
&& (to_inline r (* The user DOES want to inline it *)
- || (lang () != Haskell && not (is_projection r) &&
- (is_recursor r || manual_inline r || inline_test r t)))
+ || (lang () != Haskell &&
+ (is_projection r || is_recursor r ||
+ manual_inline r || inline_test r t)))
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 75fb35192b..e7004fe9af 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -229,12 +229,7 @@ let rec pp_expr par env args =
and pp_a1 = pp_expr false env [] a1
and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
- | MLglob r ->
- (try
- let args = List.skipn (projection_arity r) args in
- let record = List.hd args in
- pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
- with e when CErrors.noncritical e -> apply (pp_global Term r))
+ | MLglob r -> apply (pp_global Term r)
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -324,10 +319,14 @@ and pp_record_proj par env typ t pv args =
let n = List.length ids in
let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
let rel_i,a = match body with
- | MLrel i when i <= n -> i,[]
- | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a
+ | MLrel i | MLmagic(MLrel i) when i <= n -> i,[]
+ | MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a))
+ | MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a
| _ -> raise Impossible
in
+ let magic =
+ match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false
+ in
let rec lookup_rel i idx = function
| Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l
| Pwild :: l -> lookup_rel i (idx+1) l
@@ -343,7 +342,10 @@ and pp_record_proj par env typ t pv args =
let pp_args = (List.map (pp_expr true env' []) a) @ args in
let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx
in
- pp_apply pp_head par pp_args
+ if magic then
+ pp_apply (str "Obj.magic") par (pp_head :: pp_args)
+ else
+ pp_apply pp_head par pp_args
and pp_record_pat (fields, args) =
str "{ " ++
@@ -579,14 +581,10 @@ let pp_decl = function
| Dterm (r, a, t) ->
let def =
if is_custom r then str (" = " ^ find_custom r)
- else if is_projection r then
- (prvect str (Array.make (projection_arity r) " _")) ++
- str " x = x."
else pp_function (empty_env ()) a
in
let name = pp_global Term r in
- let postdef = if is_projection r then name else mt () in
- pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
+ pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
| Dfix (rv,defs,typs) ->
pp_Dfix (rv,defs,typs)
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8a5c32b8b5..35cd10a1ff 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -83,7 +83,7 @@ END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> {
- Feedback.msg_info
+ Feedback.msg_notice
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
END
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_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/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/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 2e97dfea19..cd620bd4a9 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1568,14 +1568,6 @@ module PositiveSet =
type q = { qnum : z; qden : positive }
-(** val qnum : q -> z **)
-
-let qnum x = x.qnum
-
-(** val qden : q -> positive **)
-
-let qden x = x.qden
-
(** val qeq_bool : q -> q -> bool **)
let qeq_bool x y =
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 64cb3a8355..6da0c754f4 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -446,10 +446,6 @@ module PositiveSet :
type q = { qnum : z; qden : positive }
-val qnum : q -> z
-
-val qden : q -> positive
-
val qeq_bool : q -> q -> bool
val qle_bool : q -> q -> bool
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b456d2eed2..76c393450b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -18,7 +18,6 @@ open EConstr
open Vars
open CClosure
open Environ
-open Libnames
open Globnames
open Glob_term
open Locus
@@ -326,19 +325,18 @@ let _ = add_map "ring"
module Cmap = Map.Make(Constr)
let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
-let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
let print_rings () =
Feedback.msg_notice (strbrk "The following ring structures have been declared:");
- Spmap.iter (fun fn fi ->
+ Cmap.iter (fun _carrier ring ->
let env = Global.env () in
let sigma = Evd.from_env env in
Feedback.msg_notice
(hov 2
- (Ppconstr.pr_id (Libnames.basename fn)++spc()++
- str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
- str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
- ) !from_name
+ (Ppconstr.pr_id ring.ring_name ++ spc() ++
+ str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++
+ str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req))
+ ) !from_carrier
let ring_for_carrier r = Cmap.find r !from_carrier
@@ -361,9 +359,7 @@ let find_ring_structure env sigma l =
| [] -> assert false
let add_entry (sp,_kn) e =
- from_carrier := Cmap.add e.ring_carrier e !from_carrier;
- from_name := Spmap.add sp e !from_name
-
+ from_carrier := Cmap.add e.ring_carrier e !from_carrier
let subst_th (subst,th) =
let c' = subst_mps subst th.ring_carrier in
@@ -391,7 +387,8 @@ let subst_th (subst,th) =
pretac' == th.ring_pre_tac &&
posttac' == th.ring_post_tac then th
else
- { ring_carrier = c';
+ { ring_name = th.ring_name;
+ ring_carrier = c';
ring_req = eq';
ring_setoid = set';
ring_ext = ext';
@@ -428,59 +425,6 @@ let op_morph r add mul opp req m1 m2 m3 =
let op_smorph r add mul req m1 m2 =
lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
-(* let default_ring_equality (r,add,mul,opp,req) = *)
-(* let is_setoid = function *)
-(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
-(* | _ -> false in *)
-(* match default_relation_for_carrier ~filter:is_setoid r with *)
-(* Leibniz _ -> *)
-(* let setoid = lapp coq_eq_setoid [|r|] in *)
-(* let op_morph = *)
-(* match opp with *)
-(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
-(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
-(* (setoid,op_morph) *)
-(* | Relation rel -> *)
-(* let setoid = setoid_of_relation rel in *)
-(* let is_endomorphism = function *)
-(* { args=args } -> List.for_all *)
-(* (function (var,Relation rel) -> *)
-(* var=None && eq_constr_nounivs req rel *)
-(* | _ -> false) args in *)
-(* let add_m = *)
-(* try default_morphism ~filter:is_endomorphism add *)
-(* with Not_found -> *)
-(* error "ring addition should be declared as a morphism" in *)
-(* let mul_m = *)
-(* try default_morphism ~filter:is_endomorphism mul *)
-(* with Not_found -> *)
-(* error "ring multiplication should be declared as a morphism" in *)
-(* let op_morph = *)
-(* match opp with *)
-(* | Some opp -> *)
-(* (let opp_m = *)
-(* try default_morphism ~filter:is_endomorphism opp *)
-(* with Not_found -> *)
-(* error "ring opposite should be declared as a morphism" in *)
-(* let op_morph = *)
-(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *)
-(* msgnl *)
-(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *)
-(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
-(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
-(* str"\""); *)
-(* op_morph) *)
-(* | None -> *)
-(* (msgnl *)
-(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *)
-(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(* str"\""++spc()++str"and \""++ *)
-(* pr_constr mul_m.morphism_theory++str"\""); *)
-(* op_smorph r add mul req add_m.lem mul_m.lem) in *)
-(* (setoid,op_morph) *)
-
let ring_equality env evd (r,add,mul,opp,req) =
match EConstr.kind !evd req with
| App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
@@ -657,7 +601,8 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
let _ =
Lib.add_leaf name
(theory_to_obj
- { ring_carrier = r;
+ { ring_name = name;
+ ring_carrier = r;
ring_req = req;
ring_setoid = sth;
ring_ext = params.(1);
@@ -835,19 +780,18 @@ let dest_field env evd th_spec =
| _ -> error "bad field structure"
let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
-let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
let print_fields () =
Feedback.msg_notice (strbrk "The following field structures have been declared:");
- Spmap.iter (fun fn fi ->
+ Cmap.iter (fun _carrier fi ->
let env = Global.env () in
let sigma = Evd.from_env env in
Feedback.msg_notice
(hov 2
- (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+ (Id.print fi.field_name ++ spc() ++
str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
- ) !field_from_name
+ ) !field_from_carrier
let field_for_carrier r = Cmap.find r !field_from_carrier
@@ -871,8 +815,7 @@ let find_field_structure env sigma l =
| [] -> assert false
let add_field_entry (sp,_kn) e =
- field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier;
- field_from_name := Spmap.add sp e !field_from_name
+ field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier
let subst_th (subst,th) =
let c' = subst_mps subst th.field_carrier in
@@ -898,7 +841,8 @@ let subst_th (subst,th) =
pretac' == th.field_pre_tac &&
posttac' == th.field_post_tac then th
else
- { field_carrier = c';
+ { field_name = th.field_name;
+ field_carrier = c';
field_req = eq';
field_cst_tac = tac';
field_pow_tac = pow_tac';
@@ -983,7 +927,8 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
let _ =
Lib.add_leaf name
(ftheory_to_obj
- { field_carrier = r;
+ { field_name = name;
+ field_carrier = r;
field_req = req;
field_cst_tac = cst_tac;
field_pow_tac = pow_tac;
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml
index 0a3e7bd9ca..b81f5f7d14 100644
--- a/plugins/setoid_ring/newring_ast.ml
+++ b/plugins/setoid_ring/newring_ast.ml
@@ -40,7 +40,8 @@ type 'constr field_mod =
| Inject of constr_expr
type ring_info =
- { ring_carrier : types;
+ { ring_name : Names.Id.t;
+ ring_carrier : types;
ring_req : constr;
ring_setoid : constr;
ring_ext : constr;
@@ -54,7 +55,8 @@ type ring_info =
ring_post_tac : glob_tactic_expr }
type field_info =
- { field_carrier : types;
+ { field_name : Names.Id.t;
+ field_carrier : types;
field_req : constr;
field_cst_tac : glob_tactic_expr;
field_pow_tac : glob_tactic_expr;
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 0a3e7bd9ca..b81f5f7d14 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -40,7 +40,8 @@ type 'constr field_mod =
| Inject of constr_expr
type ring_info =
- { ring_carrier : types;
+ { ring_name : Names.Id.t;
+ ring_carrier : types;
ring_req : constr;
ring_setoid : constr;
ring_ext : constr;
@@ -54,7 +55,8 @@ type ring_info =
ring_post_tac : glob_tactic_expr }
type field_info =
- { field_carrier : types;
+ { field_name : Names.Id.t;
+ field_carrier : types;
field_req : constr;
field_cst_tac : glob_tactic_expr;
field_pow_tac : glob_tactic_expr;
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index f3f1d713e9..064ea0a3e3 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -279,7 +279,7 @@ let interp_search_notation ?loc tag okey =
Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
end; ntn
| [ntn] ->
- Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
+ Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
| ntns' ->
let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
@@ -297,7 +297,7 @@ let interp_search_notation ?loc tag okey =
let rbody = glob_constr_of_notation_constr ?loc body in
let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
- Feedback.msg_info (hov 0 m) in
+ Feedback.msg_notice (hov 0 m) in
if List.length !scs > 1 then
let scs' = List.remove (=) sc !scs in
let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
@@ -464,7 +464,7 @@ let interp_modloc mr =
let ssrdisplaysearch gr env t =
let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
- Feedback.msg_info (hov 2 pr_res ++ fnl ())
+ Feedback.msg_notice (hov 2 pr_res ++ fnl ())
}
@@ -559,7 +559,7 @@ END
let print_view_hints env sigma kind l =
let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
- Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
+ Feedback.msg_notice (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:33:16 +0000