aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/himsg.ml38
-rw-r--r--vernac/ppvernac.ml123
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/vernacextend.ml4
-rw-r--r--vernac/vernacextend.mli2
5 files changed, 109 insertions, 62 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 1c58abc2fd..32754478a5 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -126,7 +126,7 @@ let display_eq ~flags env sigma t1 t2 =
let rec pr_explicit_aux env sigma t1 t2 = function
| [] ->
(* no specified flags: default. *)
- (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2))
+ Printer.pr_leconstr_env env sigma t1, Printer.pr_leconstr_env env sigma t2
| flags :: rem ->
let equal = display_eq ~flags env sigma t1 t2 in
if equal then
@@ -138,7 +138,7 @@ let rec pr_explicit_aux env sigma t1 t2 = function
in
let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
in
- quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2)
+ Ppconstr.pr_lconstr_expr env sigma ct1, Ppconstr.pr_lconstr_expr env sigma ct2
let explicit_flags =
let open Constrextern in
@@ -149,8 +149,25 @@ let explicit_flags =
[print_implicits; print_coercions; print_no_symbol]; (* Then more! *)
[print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]
+let with_diffs pm pn =
+ try
+ let tokenize_string = Proof_diffs.tokenize_string in
+ Pp_diff.diff_pp ~tokenize_string pm pn
+ with Pp_diff.Diff_Failure msg ->
+ begin
+ try ignore(Sys.getenv("HIDEDIFFFAILUREMSG"))
+ with Not_found ->
+ Feedback.msg_warning Pp.(
+ hov 0 (str ("Diff failure: " ^ msg) ++ spc () ++
+ hov 0 (str "Showing message without diff highlighting" ++ spc () ++
+ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."))))
+ end;
+ pm, pn
+
let pr_explicit env sigma t1 t2 =
- pr_explicit_aux env sigma t1 t2 explicit_flags
+ let p1, p2 = pr_explicit_aux env sigma t1 t2 explicit_flags in
+ let p1, p2 = with_diffs p1 p2 in
+ quote p1, quote p2
let pr_db env i =
try
@@ -1074,16 +1091,18 @@ let explain_unbound_method env sigma cid { CAst.v = id } =
str "Unbound method name " ++ Id.print (id) ++ spc () ++
str"of class" ++ spc () ++ pr_global cid ++ str "."
-let pr_constr_exprs exprs =
+let pr_constr_exprs env sigma exprs =
hv 0 (List.fold_right
- (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
+ (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps)
exprs (mt ()))
let explain_mismatched_contexts env c i j =
+ let sigma = Evd.from_env env in
+ let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
- hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++
+ hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++
fnl () ++ brk (1,1) ++
- hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
+ hov 1 (str"Found:" ++ brk (1, 1) ++ pn)
let explain_typeclass_error env sigma = function
| NotAClass c -> explain_not_a_class env sigma c
@@ -1092,10 +1111,11 @@ let explain_typeclass_error env sigma = function
(* Refiner errors *)
let explain_refiner_bad_type env sigma arg ty conclty =
+ let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in
str "Refiner was given an argument" ++ brk(1,1) ++
pr_lconstr_env env sigma arg ++ spc () ++
- str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++
- str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "."
+ str "of type" ++ brk(1,1) ++ pm ++ spc () ++
+ str "instead of" ++ brk(1,1) ++ pn ++ str "."
let explain_refiner_unresolved_bindings l =
str "Unable to find an instance for the " ++
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f705f347a3..506c3f9f49 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -33,7 +33,10 @@ open Pputils
let pr_constr = pr_constr_expr
let pr_lconstr = pr_lconstr_expr
- let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
+ let pr_spc_lconstr =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_sep_com spc @@ pr_lconstr_expr env sigma
let pr_uconstraint (l, d, r) =
pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
@@ -92,7 +95,10 @@ open Pputils
| VernacEndSubproof -> str""
| _ -> str"."
- let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t
+ let pr_gen t =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Pputils.pr_raw_generic env sigma t
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
@@ -142,7 +148,10 @@ open Pputils
let pr_search_about (b,c) =
(if b then str "-" else mt()) ++
match c with
- | SearchSubPattern p -> pr_constr_pattern_expr p
+ | SearchSubPattern p ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_constr_pattern_expr env sigma p
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
@@ -225,8 +234,10 @@ open Pputils
++ spc() ++ prlist_with_sep spc pr_qualid c
| HintsExtern (n,c,tac) ->
let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
- spc() ++ Pputils.pr_raw_generic (Global.env ()) tac
+ spc() ++ Pputils.pr_raw_generic env sigma tac
in
hov 2 (keyword "Hint "++ pph ++ opth)
@@ -298,7 +309,9 @@ open Pputils
pr_opt (fun sc -> str ": " ++ str sc) scopt
let pr_binders_arg =
- pr_non_empty_arg pr_binders
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_non_empty_arg @@ pr_binders env sigma
let pr_and_type_binders_arg bl =
pr_binders_arg bl
@@ -402,25 +415,35 @@ open Pputils
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
- let annot = pr_guard_annot pr_lconstr_expr bl ro in
+ let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in
pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot
- ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
- ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
- ++ prlist (pr_decl_notation pr_constr) ntn
+ ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_
+ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def
+ ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
let pr_statement head (idpl,(bl,c)) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
hov 2
(head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
- (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+ (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++
str":" ++ pr_spc_lconstr c)
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
- let pr_constrarg c = spc () ++ pr_constr c
- let pr_lconstrarg c = spc () ++ pr_lconstr c
+ let pr_constrarg c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ spc () ++ pr_constr env sigma c
+ let pr_lconstrarg c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ spc () ++ pr_lconstr env sigma c
let pr_intarg n = spc () ++ int n
let pr_oc = function
@@ -429,21 +452,23 @@ open Pputils
| Some false -> str" :>>"
let pr_record_field ((x, pri), ntn) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let prx = match x with
| (oc,AssumExpr (id,t)) ->
hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
- pr_lconstr_expr t)
+ pr_lconstr_expr env sigma t)
| (oc,DefExpr(id,b,opt)) -> (match opt with
| Some t ->
hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
- pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+ pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b)
| None ->
hov 1 (pr_lname id ++ str" :=" ++ spc() ++
- pr_lconstr b)) in
+ pr_lconstr env sigma b)) in
let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
- prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
+ prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
let pr_record_decl b c fs =
pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
@@ -566,6 +591,8 @@ open Pputils
let pr_vernac_expr v =
let return = tag_vernac v in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
match v with
| VernacLoad (f,s) ->
return (
@@ -700,7 +727,7 @@ open Pputils
| None -> mt()
| Some r ->
keyword "Eval" ++ spc() ++
- Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+ Ppred.pr_red_expr_env env sigma (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
keyword " in" ++ spc()
in
let pr_def_body = function
@@ -709,7 +736,7 @@ open Pputils
| None -> mt()
| Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
in
- (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
+ (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr env sigma body))
| ProveBody (bl,t) ->
let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
(pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
@@ -746,7 +773,7 @@ open Pputils
let n = List.length (List.flatten (List.map fst (List.map snd l))) in
let pr_params (c, (xl, t)) =
hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
- (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
+ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr env sigma t)) in
let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
@@ -771,9 +798,9 @@ open Pputils
str key ++ spc() ++
(if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
pr_and_type_binders_arg indpar ++
- pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
+ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
str" :=") ++ pr_constructor_list k lc ++
- prlist (pr_decl_notation pr_constr) ntn
+ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
in
let key =
let (_,_,_,k,_),_ = List.hd l in
@@ -814,10 +841,10 @@ open Pputils
| NoDischarge -> str ""
in
let pr_onecorec ((iddecl,bl,c,def),ntn) =
- pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
- spc() ++ pr_lconstr_expr c ++
- pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
- prlist (pr_decl_notation pr_constr) ntn
+ pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++
+ spc() ++ pr_lconstr_expr env sigma c ++
+ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++
+ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
in
return (
hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
@@ -897,11 +924,11 @@ open Pputils
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
+ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++
(match props with
| Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
| Some (true,_) -> assert false
- | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
+ | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr env sigma p
| None -> mt()))
)
@@ -912,7 +939,7 @@ open Pputils
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
+ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
)
| VernacContext l ->
@@ -922,8 +949,8 @@ open Pputils
)
| VernacExistingInstance insts ->
- let pr_inst (id, info) =
- pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
+ let pr_inst (id, info) =
+ pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info
in
return (
hov 1 (keyword "Existing" ++ spc () ++
@@ -938,25 +965,25 @@ open Pputils
(* Modules and Module Types *)
| VernacDefineModule (export,m,bl,tys,bd) ->
- let b = pr_module_binders bl pr_lconstr in
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
return (
hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
pr_lident m ++ b ++
- pr_of_module_type pr_lconstr tys ++
+ pr_of_module_type (pr_lconstr env sigma) tys ++
(if List.is_empty bd then mt () else str ":= ") ++
prlist_with_sep (fun () -> str " <+")
- (pr_module_ast_inl true pr_lconstr) bd)
+ (pr_module_ast_inl true (pr_lconstr env sigma)) bd)
)
| VernacDeclareModule (export,id,bl,m1) ->
- let b = pr_module_binders bl pr_lconstr in
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
return (
hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
pr_lident id ++ b ++ str " :" ++
- pr_module_ast_inl true pr_lconstr m1)
+ pr_module_ast_inl true (pr_lconstr env sigma) m1)
)
| VernacDeclareModuleType (id,bl,tyl,m) ->
- let b = pr_module_binders bl pr_lconstr in
- let pr_mt = pr_module_ast_inl true pr_lconstr in
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
+ let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) in
return (
hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
@@ -964,7 +991,7 @@ open Pputils
prlist_with_sep (fun () -> str " <+ ") pr_mt m)
)
| VernacInclude (mexprs) ->
- let pr_m = pr_module_ast_inl false pr_lconstr in
+ let pr_m = pr_module_ast_inl false (pr_lconstr env sigma) in
return (
hov 2 (keyword "Include" ++ spc() ++
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
@@ -1013,7 +1040,7 @@ open Pputils
pr_opt_hintbases dbnames)
)
| VernacHints (dbnames,h) ->
- return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
+ return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
| VernacSyntacticDefinition (id,(ids,c),compat) ->
return (
hov 2
@@ -1071,7 +1098,7 @@ open Pputils
let n = List.length (List.flatten (List.map fst bl)) in
return (
hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
- ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
+ ++ pr_ne_params_list (pr_lconstr_expr env sigma) (List.map (fun sb -> false,sb) bl))
)
| VernacGeneralizable g ->
return (
@@ -1143,9 +1170,9 @@ open Pputils
let pr_mayeval r c = match r with
| Some r0 ->
hov 2 (keyword "Eval" ++ spc() ++
- Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
- spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
- | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
+ Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
+ spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c)
+ | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma c)
in
let pr_i = match io with None -> mt ()
| Some i -> Goal_select.pr_goal_selector i ++ str ": " in
@@ -1155,12 +1182,12 @@ open Pputils
| VernacDeclareReduction (s,r) ->
return (
keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
- Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+ Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
)
| VernacPrint p ->
return (pr_printable p)
| VernacSearch (sea,g,sea_r) ->
- return (pr_search sea g sea_r pr_constr_pattern_expr)
+ return (pr_search sea g sea_r @@ pr_constr_pattern_expr env sigma)
| VernacLocate loc ->
let pr_locate =function
| LocateAny qid -> pr_smart_global qid
@@ -1192,7 +1219,7 @@ open Pputils
return (
hov 2
(keyword "Comments" ++ spc()
- ++ prlist_with_sep sep (pr_comment pr_constr) l)
+ ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) l)
)
(* For extension *)
@@ -1204,12 +1231,12 @@ open Pputils
return (keyword "Proof " ++ spc () ++
keyword "using" ++ spc() ++ pr_using e)
| VernacProof (Some te, None) ->
- return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te)
+ return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic env sigma te)
| VernacProof (Some te, Some e) ->
return (
keyword "Proof" ++ spc () ++
keyword "using" ++ spc() ++ pr_using e ++ spc() ++
- keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te
+ keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma te
)
| VernacProofMode s ->
return (keyword "Proof Mode" ++ str s)
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index ed93267665..60b0bdc7e7 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -196,8 +196,8 @@ let init_tag_map styles =
let default_styles () =
init_tag_map (default_tag_map ())
-let parse_color_config file =
- let styles = Terminal.parse file in
+let parse_color_config str =
+ let styles = Terminal.parse str in
init_tag_map styles
let dump_tags () = CString.Map.bindings !tag_map
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f5cf3401d0..4bfe5c66b5 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -235,7 +235,7 @@ type 'a argument_rule =
| Arg_rules of 'a Extend.production_rule list
type 'a vernac_argument = {
- arg_printer : 'a -> Pp.t;
+ arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;
}
@@ -251,6 +251,6 @@ let vernac_argument_extend ~name arg =
e
in
let pr = arg.arg_printer in
- let pr x = Genprint.PrinterBasic (fun () -> pr x) in
+ let pr x = Genprint.PrinterBasic (fun env sigma -> pr env sigma x) in
let () = Genprint.register_vernac_print0 wit pr in
(wit, entry)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 118907c31b..4d89eaffd9 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -109,7 +109,7 @@ type 'a argument_rule =
entries instead of ty_user_symbol and thus arguments as roots. *)
type 'a vernac_argument = {
- arg_printer : 'a -> Pp.t;
+ arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:11:43 +0000