diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 8 | ||||
| -rw-r--r-- | printing/printer.ml | 75 | ||||
| -rw-r--r-- | printing/printer.mli | 44 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 2 |
6 files changed, 6 insertions, 129 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 418e13759b..e7f995c84e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -194,7 +194,6 @@ let tag_var = tag Tag.variable sl ++ id let pr_id = Id.print - let pr_name = Name.print let pr_qualid = pr_qualid let pr_patvar = pr_id @@ -675,9 +674,6 @@ let tag_var = tag Tag.variable return (pr_prim_token p, prec_of_prim_token p) | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) - | CProj (p,c) -> - let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in - return (p, lproj) in let loc = constr_loc a in pr_with_comments ?loc diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index bca419c9ac..e7f71849a5 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -34,8 +34,6 @@ val pr_sep_com : constr_expr -> Pp.t val pr_id : Id.t -> Pp.t -val pr_name : Name.t -> Pp.t -[@@ocaml.deprecated "alias of Names.Name.print"] val pr_qualid : qualid -> Pp.t val pr_patvar : Pattern.patvar -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 66f748454d..e6f82c60ee 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -617,10 +617,10 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,"MODULE") -> - let (mp,_,l) = KerName.repr kn in + let (mp,l) = KerName.repr kn in Some (print_module with_values (MPdot (mp,l))) | (_,"MODULE TYPE") -> - let (mp,_,l) = KerName.repr kn in + let (mp,l) = KerName.repr kn in Some (print_modtype (MPdot (mp,l))) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None @@ -734,12 +734,12 @@ let print_full_pure_context env sigma = str "." ++ fnl () ++ fnl () | "MODULE" -> (* TODO: make it reparsable *) - let (mp,_,l) = KerName.repr kn in + let (mp,l) = KerName.repr kn in print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | "MODULE TYPE" -> (* TODO: make it reparsable *) (* TODO: make it reparsable *) - let (mp,_,l) = KerName.repr kn in + let (mp,l) = KerName.repr kn in print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _ -> mt () in prec rest ++ pp diff --git a/printing/printer.ml b/printing/printer.ml index 3a2450c426..990bdaad7d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -17,7 +17,6 @@ open Environ open Globnames open Nametab open Evd -open Proof_type open Refiner open Constrextern open Ppconstr @@ -87,7 +86,6 @@ let pr_leconstr_core = Proof_diffs.pr_leconstr_core let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) let pr_lconstr_env = Proof_diffs.pr_lconstr_env let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) -let _ = Hook.set Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c) let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c) @@ -99,20 +97,6 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c -(* NB do not remove the eta-redexes! Global.env() has side-effects... *) -let pr_lconstr t = - let (sigma, env) = Pfedit.get_current_context () in - pr_lconstr_env env sigma t -let pr_constr t = - let (sigma, env) = Pfedit.get_current_context () in - pr_constr_env env sigma t - -let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) -let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) - -let pr_open_lconstr (_,c) = pr_leconstr c -let pr_open_constr (_,c) = pr_econstr c - let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) @@ -123,13 +107,6 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env -let pr_constr_under_binders c = - let (sigma, env) = Pfedit.get_current_context () in - pr_constr_under_binders_env env sigma c -let pr_lconstr_under_binders c = - let (sigma, env) = Pfedit.get_current_context () in - pr_lconstr_under_binders_env env sigma c - let pr_etype_core goal_concl_style env sigma t = pr_constr_expr (extern_type goal_concl_style env sigma t) let pr_letype_core = Proof_diffs.pr_letype_core @@ -137,13 +114,6 @@ let pr_letype_core = Proof_diffs.pr_letype_core let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c) let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) -let pr_ltype t = - let (sigma, env) = Pfedit.get_current_context () in - pr_ltype_env env sigma t -let pr_type t = - let (sigma, env) = Pfedit.get_current_context () in - pr_type_env env sigma t - let pr_etype_env env sigma c = pr_etype_core false env sigma c let pr_letype_env env sigma c = pr_letype_core false env sigma c let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c @@ -151,29 +121,15 @@ let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) -let pr_ljudge j = - let (sigma, env) = Pfedit.get_current_context () in - pr_ljudge_env env sigma j - let pr_lglob_constr_env env c = pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c) let pr_glob_constr_env env c = pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c) -let pr_lglob_constr c = - let (sigma, env) = Pfedit.get_current_context () in - pr_lglob_constr_env env c -let pr_glob_constr c = - let (sigma, env) = Pfedit.get_current_context () in - pr_glob_constr_env env c - let pr_closed_glob_n_env env sigma n c = pr_constr_expr_n n (extern_closed_glob false env sigma c) let pr_closed_glob_env env sigma c = pr_constr_expr (extern_closed_glob false env sigma c) -let pr_closed_glob c = - let (sigma, env) = Pfedit.get_current_context () in - pr_closed_glob_env env sigma c let pr_lconstr_pattern_env env sigma c = pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) @@ -183,16 +139,9 @@ let pr_constr_pattern_env env sigma c = let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) -let pr_lconstr_pattern t = - let (sigma, env) = Pfedit.get_current_context () in - pr_lconstr_pattern_env env sigma t -let pr_constr_pattern t = - let (sigma, env) = Pfedit.get_current_context () in - pr_constr_pattern_env env sigma t - let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) -let _ = Termops.set_print_constr +let _ = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t)) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" @@ -248,13 +197,6 @@ let safe_gen f env sigma c = let safe_pr_lconstr_env = safe_gen pr_lconstr_env let safe_pr_constr_env = safe_gen pr_constr_env -let safe_pr_lconstr t = - let (sigma, env) = Pfedit.get_current_context () in - safe_pr_lconstr_env env sigma t - -let safe_pr_constr t = - let (sigma, env) = Pfedit.get_current_context () in - safe_pr_constr_env env sigma t let pr_universe_ctx_set sigma c = if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then @@ -890,19 +832,6 @@ let pr_goal_by_id ~proof id = pr_selected_subgoal (pr_id id) sigma g) with Not_found -> user_err Pp.(str "No such goal.") -(* Elementary tactics *) - -let pr_prim_rule = function - | Refine c -> - (** FIXME *) - str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ - Constrextern.with_meta_as_hole pr_constr c - -(* Backwards compatibility *) - -let prterm = pr_lconstr - - (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) @@ -960,7 +889,7 @@ let pr_assumptionset env sigma s = try pr_constant env kn with Not_found -> (* FIXME? *) - let mp,_,lab = Constant.repr3 kn in + let mp,lab = Constant.repr2 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in let safe_pr_inductive env kn = diff --git a/printing/printer.mli b/printing/printer.mli index 96db7091a6..f9d1a62895 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -27,13 +27,9 @@ val enable_goal_names_printing : bool ref (** Terms *) val pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val pr_lconstr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t val pr_constr_env : env -> evar_map -> constr -> Pp.t -val pr_constr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t @@ -43,19 +39,11 @@ val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> co in case of remaining issues (such as reference not in env). *) val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val safe_pr_lconstr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t -val safe_pr_constr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t -val pr_econstr : EConstr.t -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t -val pr_leconstr : EConstr.t -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t @@ -63,54 +51,30 @@ val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t -val pr_open_constr : open_constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t -val pr_open_lconstr : open_constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t -val pr_constr_under_binders : constr_under_binders -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t -val pr_lconstr_under_binders : constr_under_binders -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t val pr_ltype_env : env -> evar_map -> types -> Pp.t -val pr_ltype : types -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_type_env : env -> evar_map -> types -> Pp.t -val pr_type : types -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t -val pr_closed_glob : closed_glob_constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t -val pr_lglob_constr : 'a glob_constr_g -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t -val pr_glob_constr : 'a glob_constr_g -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t -val pr_lconstr_pattern : constr_pattern -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t -val pr_constr_pattern : constr_pattern -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_cases_pattern : cases_pattern -> Pp.t @@ -222,16 +186,8 @@ val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t -val pr_prim_rule : prim_rule -> Pp.t -[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"] - val print_and_diff : Proof.t option -> Proof.t option -> unit -(** Backwards compatibility *) - -val prterm : constr -> Pp.t (** = pr_lconstr *) -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] - (** Declarations for the "Print Assumption" command *) type axiom = | Constant of Constant.t (* An axiom or a constant. *) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 5bb1053645..0b630b39b5 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -523,8 +523,6 @@ let match_goals ot nt = | CPrim p, CPrim p2 -> () | CDelimiters (key,e), CDelimiters (key2,e2) -> constr_expr ogname e e2 - | CProj (pr,c), CProj (pr2,c2) -> - constr_expr ogname c c2 | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)") end in |