diff options
30 files changed, 185 insertions, 192 deletions
diff --git a/doc/changelog/08-tools/10577-extraction-dependent-projections.rst b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst new file mode 100644 index 0000000000..4d52355542 --- /dev/null +++ b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst @@ -0,0 +1,9 @@ +- Fix a printing bug of OCaml extraction on dependent record projections, which + produced improper `assert false`. This change makes the OCaml extractor + internally inline record projections by default; thus the monolithic OCaml + extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not + produce record projection constants anymore except for record projections + explicitly instructed to extract, and records declared in opaque modules + (`#10577 <https://github.com/coq/coq/pull/10577>`_, + fixes `#7348 <https://github.com/coq/coq/issues/7348>`_, + by Kazuhiko Sakaguchi). diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index e3a5676942..3c383b2e00 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -107,7 +107,7 @@ struct Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Feedback.msg_info s) + let print_debug s = make (fun _ -> Feedback.msg_debug s) let print_info s = make (fun _ -> Feedback.msg_info s) let print_warning s = make (fun _ -> Feedback.msg_warning s) let print_notice s = make (fun _ -> Feedback.msg_notice s) diff --git a/lib/feedback.mli b/lib/feedback.mli index dc8449ed71..5375d97d57 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -74,13 +74,8 @@ val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_conte (** [set_id_for_feedback route id] Set the defaults for feedback *) val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit -(** {6 output functions} +(** {6 output functions} *) -[msg_notice] do not put any decoration on output by default. If -possible don't mix it with goal output (prefer msg_info or -msg_warning) so that interfaces can dispatch outputs easily. Once all -interfaces use the xml-like protocol this constraint can be -relaxed. *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) diff --git a/lib/system.ml b/lib/system.ml index b1a9efccfc..8c333ec267 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -300,13 +300,13 @@ let with_time ~batch ~header f x = let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) diff --git a/library/goptions.ml b/library/goptions.ml index c7024ca81d..0973944fb5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -398,9 +398,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index de23f05a9e..7f0d768d3f 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -436,7 +436,7 @@ let comment_stop ep = let bp = match !comment_begin with Some bp -> bp | None -> - Feedback.msg_notice + Feedback.msg_debug (str "No begin location for comment '" ++ str current_s ++str"' ending at " ++ int ep); 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 ()) } diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index be21a3a60d..288a349b8b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -773,7 +773,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in + Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> @@ -1569,7 +1569,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ + Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7362955eb7..df161b747a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -918,7 +918,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let () = if !debug_RAKAM then let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_notice + Feedback.msg_debug (h 0 (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ @@ -927,7 +927,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let c0 = EConstr.kind sigma x in let fold () = let () = if !debug_RAKAM then - let open Pp in Feedback.msg_notice (str "<><><><><>") in + let open Pp in Feedback.msg_debug (str "<><><><><>") in ((EConstr.of_kind c0, stack),cst_l) in match c0 with diff --git a/tactics/auto.ml b/tactics/auto.ml index 67f49f0074..0b465418f2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -220,13 +220,13 @@ let tclLOG (dbg,_,depth,trace) pp tac = tac >>= fun v -> tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*success*)"); + Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*success*)"); tclUNIT v ) tclUNIT (fun (exn, info) -> tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)"); + Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)"); tclZERO ~info exn)) | Info -> (* For "info (trivial/auto)", we store a log trace *) @@ -260,19 +260,19 @@ let pr_info_atom env sigma (d,pp) = let pr_info_trace env sigma = function | (Info,_,_,{contents=(d,Some pp)::l}) -> - Feedback.msg_info (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l)) + Feedback.msg_notice (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l)) | _ -> () let pr_info_nop = function - | (Info,_,_,_) -> Feedback.msg_info (str "idtac.") + | (Info,_,_,_) -> Feedback.msg_notice (str "idtac.") | _ -> () let pr_dbg_header = function | (Off,_,_,_) -> () - | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)") - | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") - | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)") - | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)") + | (Debug,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* debug trivial: *)") + | (Debug,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* debug auto: *)") + | (Info,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* info trivial: *)") + | (Info,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* info auto: *)") let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index d4e4322bef..2ce32b309a 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -351,13 +351,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> Feedback.msg_info (str "idtac.") + | Info -> Feedback.msg_notice (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () - | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") - | Info -> Feedback.msg_info (str "(* info eauto: *)") + | Debug -> Feedback.msg_notice (str "(* debug eauto: *)") + | Info -> Feedback.msg_notice (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () @@ -368,7 +368,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_notice (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out index 2761b87b02..5e81b43504 100644 --- a/test-suite/output/auto.out +++ b/test-suite/output/auto.out @@ -2,18 +2,18 @@ simple apply or_intror (in core). intro. assumption. -Debug: (* debug auto: *) -Debug: * assumption. (*fail*) -Debug: * intro. (*fail*) -Debug: * simple apply or_intror (in core). (*success*) -Debug: ** assumption. (*fail*) -Debug: ** intro. (*success*) -Debug: ** assumption. (*success*) +(* debug auto: *) +* assumption. (*fail*) +* intro. (*fail*) +* simple apply or_intror (in core). (*success*) +** assumption. (*fail*) +** intro. (*success*) +** assumption. (*success*) (* info eauto: *) simple apply or_intror. intro. exact H. -Debug: (* debug eauto: *) +(* debug eauto: *) Debug: 1 depth=5 Debug: 1.1 depth=4 simple apply or_intror Debug: 1.1.1 depth=4 intro diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out new file mode 100644 index 0000000000..325ee95ae2 --- /dev/null +++ b/test-suite/output/bug7348.out @@ -0,0 +1,45 @@ +Extracted code successfully compiled + +type __ = Obj.t + +type unit0 = +| Tt + +type bool = +| True +| False + +module Case1 = + struct + type coq_rec = { f : bool } + + (** val f : bool -> coq_rec -> bool **) + + let f _ r = + r.f + + (** val silly : bool -> coq_rec -> __ **) + + let silly x b = + match x with + | True -> Obj.magic b.f + | False -> Obj.magic Tt + end + +module Case2 = + struct + type coq_rec = { f : (bool -> bool) } + + (** val f : bool -> coq_rec -> bool -> bool **) + + let f _ r = + r.f + + (** val silly : bool -> coq_rec -> __ **) + + let silly x b = + match x with + | True -> Obj.magic b.f False + | False -> Obj.magic Tt + end + diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v new file mode 100644 index 0000000000..782b27ce96 --- /dev/null +++ b/test-suite/output/bug7348.v @@ -0,0 +1,25 @@ +Require Extraction. + +Extraction Language OCaml. +Set Extraction KeepSingleton. + +Module Case1. + +Record rec (x : bool) := { f : bool }. + +Definition silly x (b : rec x) := + if x return (if x then bool else unit) then f x b else tt. + +End Case1. + +Module Case2. + +Record rec (x : bool) := { f : bool -> bool }. + +Definition silly x (b : rec x) := + if x return (if x then bool else unit) then f x b false else tt. + +End Case2. + +Extraction TestCompile Case1.silly Case2.silly. +Recursive Extraction Case1.silly Case2.silly. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 33a95e7b30..eded9f4bcd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,7 +30,7 @@ let get_version_date () = let print_header () = let (ver,rev) = get_version_date () in - Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); + Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () let print_memory_stat () = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 90b7610750..3d14e8d510 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2285,7 +2285,7 @@ let with_fail ~st f = user_err ~hdr:"Fail" (str "The command has not failed!") | Ok msg -> if not !Flags.quiet || !test_mode - then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) + then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg) let locate_if_not_already ?loc (e, info) = match Loc.get_loc info with |