diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 19:08:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 18:04:32 +0100 |
| commit | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
[printing] Deprecate all printing functions accessing the global proof.
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
57 files changed, 568 insertions, 413 deletions
diff --git a/API/API.mli b/API/API.mli index 51671fc3d..86c6f1415 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5150,12 +5150,20 @@ sig val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t val pr_constr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_constr_pattern : Pattern.constr_pattern -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t @@ -5163,11 +5171,17 @@ sig val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_leconstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_global : Globnames.global_reference -> Pp.t val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t @@ -5176,7 +5190,11 @@ sig val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_ltype : Term.types -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + 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_idpred : Names.Id.Pred.t -> Pp.t val pr_cpred : Names.Cpred.t -> Pp.t val pr_transparent_state : Names.transparent_state -> Pp.t @@ -5689,7 +5707,9 @@ sig val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit val empty_hint_info : 'a Vernacexpr.hint_info_gen val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast + val pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t + [@@ocaml.deprecated "please used pr_hint_db_env"] end module Auto : @@ -5766,7 +5786,7 @@ sig val add_rew_rules : string -> raw_rew_rule list -> unit val find_rewrites : string -> rew_rule list val find_matches : string -> Constr.t -> rew_rule list - val print_rewrite_hintdb : string -> Pp.t + val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t end (************************************************************************) @@ -5799,11 +5819,12 @@ sig Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit val get_current_context : unit -> Evd.evar_map * Environ.env + [@@ocaml.deprecated "please use [Pfedit.get_current_context]"] end module Himsg : sig - val explain_refiner_error : Logic.refiner_error -> Pp.t + val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t end diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 5b09436c2..0f496d3b9 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -60,6 +60,7 @@ let pprecarg = function let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) (* term printers *) +let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) @@ -69,9 +70,9 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.o let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x -let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) -let pppattern = (fun x -> pp(pr_constr_pattern x)) -let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) +let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) +let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) +let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; @@ -121,7 +122,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = and pr_closed_glob_constr_idmap x = pridmap (fun _ -> pr_closed_glob_constr) x and pr_closed_glob_constr {closure=closure;term=term} = - pr_closure closure ++ pr_lglob_constr term + pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term let ppclosure x = pp (pr_closure x) let ppclosedglobconstr x = pp (pr_closed_glob_constr x) @@ -140,14 +141,14 @@ let safe_pr_global = function let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x let ppconst (sp,j) = - pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val) + pp (str"#" ++ KerName.print sp ++ str"=" ++ envpp pr_lconstr_env j.uj_val) let ppvar ((id,a)) = - pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a) + pp (str"#" ++ Id.print id ++ str":" ++ envpp pr_lconstr_env a) let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) -let ppj j = pp (genppj pr_ljudge j) +let ppj j = pp (genppj (envpp pr_ljudge_env) j) let prsubst s = pp (Mod_subst.debug_pr_subst s) let prdelta s = pp (Mod_subst.debug_pr_delta s) @@ -175,13 +176,13 @@ let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g)) -let pphintdb db = pp(Hints.pr_hint_db db) +let pphintdb db = pp(envpp Hints.pr_hint_db_env db) let ppproofview p = let gls,sigma = Proofview.proofview p in pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d980b1995..51b06580e 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -60,6 +60,19 @@ val set_extern_reference : val get_extern_reference : unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) +(** WARNING: The following functions are evil due to + side-effects. Think of the following case as used in the printer: + + without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c + + vs + + without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c + + which one is wrong? We should turn this kind of state into an + explicit argument. +*) + (** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index da8955f0d..a09abfa19 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -200,7 +200,8 @@ module Btauto = struct let assign = List.combine env var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let term = Printer.pr_constr key in + let sigma, env = Pfedit.get_current_context () in + let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in let assign = List.map map_msg assign in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bd5fb1d92..29e824f44 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) +let pr_leconstr_fp = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let debug_queue = Stack.create () let rec print_debug_queue e = @@ -172,7 +176,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -220,7 +224,8 @@ let find_rectype env sigma c = let isAppConstruct ?(env=Global.env ()) sigma t = try let t',l = find_rectype env sigma t in - observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l))); + observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++ + Printer.pr_leconstr_env env sigma (applist (t',l))); true with Not_found -> false @@ -233,7 +238,8 @@ exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); + observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++ + match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t ); raise NoChange; end in @@ -841,7 +847,7 @@ let build_proof | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam princ_params ); observe (str "fbody_with_full_params := " ++ - pr_leconstr fbody_with_full_params + pr_leconstr_env (Global.env ()) !evd fbody_with_full_params ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 722dbc16b..3899bc709 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -115,7 +115,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in - observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); + observe (str "replacing " ++ + pr_lconstr_env env Evd.empty c ++ str " by " ++ + pr_lconstr_env env Evd.empty res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = @@ -565,7 +567,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; - observe (Printer.pr_lconstr scheme_type); + observe (Printer.pr_lconstr_env env sigma scheme_type); let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in @@ -577,8 +579,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let g = fst (decompose_app applied_g) in if Constr.equal f g then raise (Found_type j); - observe (Printer.pr_lconstr f ++ str " <> " ++ - Printer.pr_lconstr g) + observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ + Printer.pr_lconstr_env env sigma g) ) ta; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8ab6dbcdf..d04b7a33d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -379,29 +379,30 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let open Context.Rel.Declaration in - match decl with + let open Context.Rel.Declaration in + let sigma, _ = Pfedit.get_current_context () in + match decl with | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false | LocalAssum (Name id, t) -> - let new_t = substl ctxt t in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> - let new_t = substl ctxt t in - let new_v = substl ctxt v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ - str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) - ) + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++ + str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + ) (Environ.rel_context new_env) ~init:(env,[]) ) @@ -479,7 +480,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); + observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> @@ -652,8 +653,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); @@ -684,8 +685,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); @@ -897,24 +898,24 @@ let same_raw_term rt1 rt2 = | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = - let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); - let (rhd,lrhs) = glob_decompose_app rhs in - let (lhd,llhs) = glob_decompose_app lhs in - observe (str "lhd := " ++ pr_glob_constr lhd); - observe (str "rhd := " ++ pr_glob_constr rhd); + let _, env = Pfedit.get_current_context () in + let rec decompose_raw_eq lhs rhs acc = + observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr_env env lhd); + observe (str "rhd := " ++ pr_glob_constr_env env rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); - let sllhs = List.length llhs in - let slrhs = List.length lrhs in - if same_raw_term lhd rhd && Int.equal sllhs slrhs + let sllhs = List.length llhs in + let slrhs = List.length lrhs in + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc else (lhs,rhs)::acc in decompose_raw_eq lhs rhs [] - exception Continue (* @@ -923,7 +924,7 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); + observe (str "rebuilding : " ++ pr_glob_constr_env env rt); let open Context.Rel.Declaration in let open CAst in match DAst.get rt with @@ -967,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when CErrors.noncritical e -> raise Continue @@ -1012,7 +1013,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let eq' = DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = @@ -1099,7 +1100,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1115,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1134,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index dab094f91..f01b6669d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -46,7 +46,7 @@ let functional_induction with_clean c princl pat = try find_Function_infos c' with Not_found -> user_err (str "Cannot find induction information on "++ - Printer.pr_leconstr (mkConst c') ) + Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma @@ -74,7 +74,7 @@ let functional_induction with_clean c princl pat = (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) user_err (str "Cannot find induction principle for " - ++Printer.pr_leconstr (mkConst c') ) + ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in let princ = EConstr.of_constr princ in (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') @@ -841,12 +841,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list * let make_graph (f_ref:global_reference) = let c,c_body = match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> - raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) ) - end - | _ -> raise (UserError (None, str "Not a function reference") ) + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + let sigma, env = Pfedit.get_current_context () in + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) + end + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 61d207b95..8bf6e48fd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -333,15 +333,17 @@ let discharge_Function (_,finfos) = } let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) + Printer.pr_lconstr_env env sigma + (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -349,7 +351,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 692a874d3..694c80051 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -851,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) funs_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b372241d2..9e2774ff3 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -90,20 +90,28 @@ let next_ident_fresh (id:Id.t) = (* comment this line to see debug msgs *) let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c) -let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prconstr c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c) + +let prconstrnl c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") + let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) let prNamedConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); msg(str ""); end let prNamedRConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b8d41d539..04d729b10 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,6 +54,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] +let pr_leconstr_rd = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let coq_init_constant s = EConstr.of_constr ( Universes.constr_of_global @@ @@ -337,7 +341,8 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p) + let _, env = Pfedit.get_current_context () in + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -455,7 +460,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin @@ -463,7 +468,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -491,8 +496,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> @@ -515,7 +520,7 @@ and travel_args jinfo is_final continuation_tac infos = {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac - (str jinfo.message ++ Printer.pr_leconstr expr_info.info) + (str jinfo.message ++ pr_leconstr_rd expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -731,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') + observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac @@ -740,7 +745,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g @@ -991,11 +996,11 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info) + observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos) + (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch @@ -1419,7 +1424,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1471,7 +1476,7 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 89feea8dc..bb01aca55 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c -let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 5baa0d5c1..84e79d8ab 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -51,8 +51,12 @@ let eval_uconstrs ist cs = List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) ARGUMENT EXTEND auto_using TYPED AS uconstr_list diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b148d962e..91abe1019 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings -let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge))) -let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge)) +let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst (snd ge))) +let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst ge)) let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l @@ -272,5 +276,7 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> + [ let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 3f885f8ba..d70751245 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1243,6 +1243,15 @@ let make_constr_printer f c = let lift f a = Genprint.PrinterBasic (fun () -> f a) + +let pr_glob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_glob_constr_env env c + +let pr_lglob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_lglob_constr_env env c + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1257,7 +1266,7 @@ let () = Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) + (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl @@ -1267,46 +1276,46 @@ let () = ; Genprint.register_print0 wit_constr - Ppconstr.pr_lconstr_expr - (fun (c, _) -> Printer.pr_lglob_constr c) + Ppconstr.pr_constr_expr + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr - (fun (c,_) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) pr_red_expr_env ; Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_bindings_env ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 wit_open_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_destruction_arg_env ; Genprint.register_print0 Stdarg.wit_int int int (lift int); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 180fb2db4..918d1faeb 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -91,9 +91,10 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (is_global ref' t') then - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ - pr_global ref') ; + (let sigma, env = Pfedit.get_current_context () in + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ + pr_global ref')); ref' in subst_or_var (subst_located subst_global) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index a669692fc..2dd7c9a74 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> Printer.pr_constr_pattern p) rl + (fun (_,p) -> + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + let sigma, env = Pfedit.get_current_context () in + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 218342efe..cb54cac3f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -984,7 +984,9 @@ struct let parse_expr sigma parse_constant parse_exp ops_spec env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term); + then ( + let _, env = Pfedit.get_current_context () in + Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); (* let constant_or_variable env term = @@ -1103,9 +1105,10 @@ struct | _ -> raise ParseError - let rconstant sigma term = + let rconstant sigma term = + let _, env = Pfedit.get_current_context () in if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1145,9 +1148,9 @@ struct let parse_arith parse_op parse_expr env cstr gl = let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); - match EConstr.kind sigma cstr with + if debug + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); + match EConstr.kind sigma cstr with | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in @@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr ff); + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; @@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' + (dump_cstr spec.typ spec.dump_coeff) ff' in + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; (* Even if it does not work, this does not mean it is not provable diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 430b608f4..54ff44fbd 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -183,8 +183,9 @@ let print_env_reification env = let rec loop c i = function [] -> str " ===============================\n\n" | t :: l -> + let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 05ab8ab32..a7d6d5bb2 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) + 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 ] END @@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) + 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 ] END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9e4b896f8..1c3bdb958 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -344,8 +344,6 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -let pr_constr c = pr_econstr c - module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -368,7 +366,7 @@ let find_ring_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) | [] -> assert false let add_entry (sp,_kn) e = @@ -529,19 +527,19 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\","++spc()++ str"\""++pr_constr mul_m_lem++ - str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ + str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ str"\""++spc()++str"and \""++ - pr_constr mul_m_lem++str"\""); + pr_econstr_env env !evd mul_m_lem++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) @@ -861,7 +859,7 @@ let find_field_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) | [] -> assert false let add_field_entry (sp,_kn) e = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index c1d7e6278..83b454769 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -240,7 +240,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c)); + ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); (sigma, (sigma, c)) @@ -539,7 +539,7 @@ module Intset = Evar.Set let pf_abs_evars_pirrel gl (sigma, c0) = pp(lazy(str"==PF_ABS_EVARS_PIRREL==")); - pp(lazy(str"c0= " ++ Printer.pr_constr c0)); + pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0)); let sigma0 = project gl in let c0 = nf_evar sigma0 (nf_evar sigma c0) in let nenv = env_size (pf_env gl) in @@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") (fun (k,_) -> str(Evd.string_of_existential k)) evlist)); let evplist = @@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in - pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t)); + pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Tacmach.refine_no_check t gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = @@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = compose_lam (let xs,y = List.chop (n-1) l in y @ xs) (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) in - pp(lazy(str"after: " ++ Printer.pr_constr oc)); + pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc)); try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error @@ -1202,7 +1202,7 @@ let genclrtac cl cs clr = let gentac ist gen gl = (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr c)); + ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 26b5c5767..4e0b44a44 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma = if not (EConstr.eq_constr sigma t t') then loop ctx t' else errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++ str"A (applied) bound variable was expected as the conclusion of "++ - str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in + str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in let n_elim_args = Context.Rel.nhyps ctx in let is_rec_elim = @@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr c)); + ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr | Some (c, _, _,gl) -> true, gl | None -> errorstrm Pp.(str"Unable to apply the eliminator to the term"++ - spc()++pr_econstr c++spc()++str"or to unify it's type with"++ - pr_econstr inf_arg_ty) in + spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++ + pr_econstr_env env (project gl) inf_arg_ty) in ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index e82f222b9..274c7110c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -77,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt)); + ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -86,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term ist gl t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -109,7 +109,7 @@ let congrtac ((n, t), ty) ist gl = let newssrcongrtac arg ist gl = ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -247,7 +247,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr c)), + ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -267,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl = | Proj _ when same_proj sigma0 c t -> body env t c | Const f -> aux (body env c c) | App (f, a) -> aux (EConstr.mkApp (body env f f, a)) - | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++ - str" contains no " ++ pr_econstr t ++ str" even after unfolding") + | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++ + str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding") in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c) else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in @@ -352,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* We check the proof is well typed *) let sigma, proof_ty = try Typing.type_of env sigma proof with _ -> raise PRtype_error in - ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty)); + ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl with _ -> @@ -374,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) | _ -> anomaly "rewrite rule not an application" in - errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++ - (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty)) + errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++ + (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; let is_construct_ref sigma c r = @@ -391,12 +391,12 @@ let rwcltac cl rdx dir sr gl = let gl = pf_unsafe_merge_uc ucst gl in let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr))); + ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = if EConstr.Vars.closed0 (project gl) r' then let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty)); + ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in @@ -411,7 +411,7 @@ let rwcltac cl rdx dir sr gl = let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr)) - ++ str " to " ++ pr_econstr r2) in + ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in @@ -605,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in - let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in Feedback.msg_info Pp.(str"BEGIN INSTANCES"); try while true do diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 29e96ec59..a707226cd 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -72,13 +72,14 @@ let examine_abstract id gl = let gl, tid = pfe_type_of gl id in let abstract, gl = pf_mkSsrConst "abstract" gl in let sigma = project gl in + let env = pf_env gl in if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then - errorstrm(strbrk"not an abstract constant: "++pr_econstr id); + errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id); let _, args_id = EConstr.destApp sigma tid in if Array.length args_id <> 3 then - errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id); + errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id); if not (is_Evar_or_CastedMeta sigma args_id.(2)) then - errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used"); + errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used"); tid, args_id let pf_find_abstract_proof check_lock gl abstract_n = @@ -94,7 +95,7 @@ let pf_find_abstract_proof check_lock gl abstract_n = | _ -> l) (project gl) [] in match l with | [e] -> e - | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++ strbrk" not found in the evar map exactly once. "++ strbrk"Did you tamper with it?") @@ -205,7 +206,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function @@ -271,7 +272,7 @@ let ssrabstract ist gens (*last*) gl = let gl, proof = let pf_unify_HO gl a b = try pf_unify_HO gl a b - with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++ + with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++ strbrk" cannot abstract this goal. Did you generalize it?") in let find_hole p t = match EConstr.kind (project gl) t with @@ -290,7 +291,7 @@ let ssrabstract ist gens (*last*) gl = | App(hd, [|left; right|]) when Term.Constr.equal hd prod -> find_hole (mkApp (proj1,[|left;right;p|])) left *) - | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++ strbrk" has an unexpected shape. Did you tamper with it?") in find_hole @@ -361,14 +362,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Sort _, [] -> EConstr.Vars.subst_vars s ct | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) - | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in let c = var2rel c gens [] in let rec pired c = function | [] -> c | t::ts as args -> match EConstr.kind sigma c with | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args) - | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in c, args, pired c args, pf_merge_uc uc gl in let tacipat pats = introstac ~ist pats in let tacigens = @@ -396,8 +397,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Some id -> if pats = [] then Tacticals.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++pr_econstr ct)); + ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); + ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); Tacticals.tclTHENS (basecuttac "ssr_have" ct) [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in "ssr_have", diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 023778fdb..6c325cce4 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl = (* Utils of local interest only *) let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in - ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in + ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in let protectC, gl = pf_mkSsrConst "protect_term" gl in let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in let eq = EConstr.of_constr eq in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7b591fead..46403aef3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function | (fk, h), (_, (_, Some c)) -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | (fk, h), (_, (c, None)) -> - pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) + pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c) let pr_unguarded prc prlc = prlc diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e865ef706..4b2fab6d1 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs -> hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs let pp_term gl t = - let t = Reductionops.nf_evar (project gl) t in pr_econstr t + let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t (* FIXME *) (* terms are pre constr, the kind is parsing/printing flag to distinguish diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 36dce37ae..cd614fee9 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -343,7 +343,7 @@ let coerce_search_pattern_to_sort hpat = let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ - pr_constr_pattern hpat') in + pr_constr_pattern_env env sigma hpat') in if EConstr.isSort sigma ht then begin warn (); true, hpat' end else let filter_head, coe_path = try @@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat = let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc () + errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path @@ -468,10 +468,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref c = match DAst.get c with +let pr_rawhintref c = + let _, env = Pfedit.get_current_context () in + match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr c + pr_glob_constr_env env f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d5c9e4988..276b7c8ab 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -100,7 +100,6 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let pr_constr = pr_constr let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr @@ -427,7 +426,8 @@ let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = if isEvar c then hole_var else map wipe_evar c in - pr_constr (wipe_evar c0) + let sigma, env = Pfedit.get_current_context () in + pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = @@ -1215,7 +1215,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in let e_body = match e_body with Evar_defined c -> c - | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++ + | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++ str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ str "in the pattern?") in @@ -1417,7 +1417,8 @@ let ssrinstancesof ist arg gl = let find, conclude = mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma None (etpat,[tpat]) in - let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in ppnl (str"BEGIN INSTANCES"); try while true do diff --git a/printing/pputils.ml b/printing/pputils.ml index 3cc7a3e6b..12d5338ad 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -103,6 +103,9 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function | CbvNative o -> keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o +let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = + pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) + let pr_or_by_notation f = function | AN v -> f v | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc diff --git a/printing/pputils.mli b/printing/pputils.mli index 1f4fa1390..f7f586b77 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -21,8 +21,16 @@ val pr_with_occurrences : val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t + val pr_red_expr : ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t + +val pr_red_expr_env : Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + ('b -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index acbd2d5d2..e2d23ce7b 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,13 +35,13 @@ module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> Pp.t; print_constant_with_infos : Constant.t -> Pp.t; - print_section_variable : variable -> Pp.t; - print_syntactic_def : KerName.t -> Pp.t; + print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; + print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : Context.Named.Declaration.t -> Pp.t; - print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; - print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -487,25 +487,25 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) synthesizes the type nat of the abstraction on u *) -let print_named_def name body typ = - let pbody = pr_lconstr body in - let ptyp = pr_ltype typ in +let print_named_def env sigma name body typ = + let pbody = pr_lconstr_env env sigma body in + let ptyp = pr_ltype_env env sigma typ in let pbody = if isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ str "]") -let print_named_assum name typ = - str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" +let print_named_assum env sigma name typ = + str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" -let gallina_print_named_decl = +let gallina_print_named_decl env sigma = let open Context.Named.Declaration in function | LocalAssum (id, typ) -> - print_named_assum (Id.to_string id) typ + print_named_assum env sigma (Id.to_string id) typ | LocalDef (id, body, typ) -> - print_named_def (Id.to_string id) body typ + print_named_def env sigma (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -524,11 +524,11 @@ let gallina_print_inductive sp = print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) -let print_named_decl id = - gallina_print_named_decl (Global.lookup_named id) ++ fnl () +let print_named_decl env sigma id = + gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () -let gallina_print_section_variable id = - print_named_decl id ++ +let gallina_print_section_variable env sigma id = + print_named_decl env sigma id ++ with_line_skip (print_name_infos (VarRef id)) let print_body env evd = function @@ -601,7 +601,7 @@ let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ with_line_skip (print_name_infos (ConstRef sp)) -let gallina_print_syntactic_def kn = +let gallina_print_syntactic_def env kn = let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in let c = Notation_ops.glob_constr_of_notation_constr a in @@ -612,16 +612,16 @@ let gallina_print_syntactic_def kn = spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols - [Notation.SynDefRule kn] pr_glob_constr c) + [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " and tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> (* Outside sections, VARIABLES still exist but only with universes constraints *) - (try Some(print_named_decl (basename sp)) with Not_found -> None) + (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> Some (print_constant with_values sep (Constant.make1 kn)) | (_,"INDUCTIVE") -> @@ -637,11 +637,11 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = (* To deal with forgotten cases... *) | (_,s) -> None -let gallina_print_library_entry with_values ent = +let gallina_print_library_entry env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (oname,Lib.ClosedSection _) -> @@ -653,10 +653,10 @@ let gallina_print_library_entry with_values ent = | (oname,Lib.ClosedModule _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) -let gallina_print_context with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -718,10 +718,10 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context () = print_context true None (Lib.contents ()) -let print_full_context_typ () = print_context false None (Lib.contents ()) +let print_full_context env sigma = print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) -let print_full_pure_context () = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf lobj)::rest -> let pp = match object_tag lobj with @@ -733,15 +733,15 @@ let print_full_pure_context () = match cb.const_body with | Undef _ -> str "Parameter " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype typ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc) + str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ + str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ - pr_lconstr (Mod_subst.force_constr c)) + str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ + pr_lconstr_env env sigma (Mod_subst.force_constr c)) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in @@ -787,18 +787,18 @@ let read_sec_context r = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context sec = - print_context true None (read_sec_context sec) +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) -let print_sec_context_typ sec = - print_context false None (read_sec_context sec) +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) -let print_any_name = function +let print_any_name env sigma = function | Term (ConstRef sp) -> print_constant_with_infos sp | Term (IndRef (sp,_)) -> print_inductive sp | Term (ConstructRef ((sp,_),_)) -> print_inductive sp - | Term (VarRef sp) -> print_section_variable sp - | Syntactic kn -> print_syntactic_def kn + | Term (VarRef sp) -> print_section_variable env sigma sp + | Syntactic kn -> print_syntactic_def env kn | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp @@ -807,22 +807,21 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - str |> Global.lookup_named |> print_named_decl + str |> Global.lookup_named |> print_named_decl env sigma with Not_found -> user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name = function +let print_name env sigma = function | ByNotation (loc,(ntn,sc)) -> - print_any_name + print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> - print_any_name (locate_any_name ref) + print_any_name env sigma (locate_any_name ref) -let print_opaque_name qid = - let env = Global.env () in +let print_opaque_name env sigma qid = match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in @@ -840,9 +839,9 @@ let print_opaque_name qid = let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> print_named_decl + env |> lookup_named id |> print_named_decl env sigma -let print_about_any ?loc k = +let print_about_any ?loc env sigma k = match k with | Term ref -> let rb = Reductionops.ReductionBehaviour.print ref in @@ -858,23 +857,23 @@ let print_about_any ?loc k = | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref | _ -> () in v 0 ( - print_syntactic_def kn ++ fnl () ++ + print_syntactic_def env kn ++ fnl () ++ hov 0 (str "Expands to: " ++ pr_located_qualid k)) | Dir _ | ModuleType _ | Undefined _ -> hov 0 (pr_located_qualid k) | Other (obj, info) -> hov 0 (info.about obj) -let print_about = function +let print_about env sigma = function | ByNotation (loc,(ntn,sc)) -> - print_about_any ?loc + print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> - print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref) + print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) (* for debug *) -let inspect depth = - print_context false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) @@ -882,18 +881,20 @@ let inspect depth = open Classops -let print_coercion_value v = pr_lconstr (get_coercion_value v) +let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) let print_class i = let cl,_ = class_info_from_index i in pr_class cl let print_path ((i,j),p) = + let sigma, env = Pfedit.get_current_context () in hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ + str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j +(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path let print_graph () = @@ -902,8 +903,8 @@ let print_graph () = let print_classes () = pr_sequence pr_class (classes()) -let print_coercions () = - pr_sequence print_coercion_value (coercions()) +let print_coercions env sigma = + pr_sequence (print_coercion_value env sigma) (coercions()) let index_of_class cl = try @@ -925,11 +926,11 @@ let print_path_between cls clt = in print_path ((i,j),p) -let print_canonical_projections () = +let print_canonical_projections env sigma = prlist_with_sep fnl (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ str " <- " ++ - pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") + pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") (canonical_projections ()) (*************************************************************************) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 31fd766ea..89099a043 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -18,37 +18,37 @@ open Misctypes val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option -val print_full_context : unit -> Pp.t -val print_full_context_typ : unit -> Pp.t -val print_full_pure_context : unit -> Pp.t -val print_sec_context : reference -> Pp.t -val print_sec_context_typ : reference -> Pp.t +val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option +val print_full_context : env -> Evd.evar_map -> Pp.t +val print_full_context_typ : env -> Evd.evar_map -> Pp.t +val print_full_pure_context : env -> Evd.evar_map -> Pp.t +val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : reference or_by_notation -> Pp.t -val print_opaque_name : reference -> Pp.t -val print_about : reference or_by_notation -> Pp.t +val print_name : env -> Evd.evar_map -> reference or_by_notation -> Pp.t +val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t +val print_about : env -> Evd.evar_map -> reference or_by_notation -> Pp.t val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t -val print_coercions : unit -> Pp.t +val print_coercions : env -> Evd.evar_map -> Pp.t val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t -val print_canonical_projections : unit -> Pp.t +val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) val print_typeclasses : unit -> Pp.t val print_instances : global_reference -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : int -> Pp.t +val inspect : env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -82,15 +82,15 @@ val print_located_other : string -> reference -> Pp.t type object_pr = { print_inductive : MutInd.t -> Pp.t; print_constant_with_infos : Constant.t -> Pp.t; - print_section_variable : variable -> Pp.t; - print_syntactic_def : KerName.t -> Pp.t; + print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; + print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : Context.Named.Declaration.t -> Pp.t; - print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; - print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; - print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } val set_object_pr : object_pr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index ba31b72d6..377a6b4e1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -26,9 +26,6 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration -let get_current_context () = - Pfedit.get_current_context () - let enable_unfocused_goal_printing = ref false let enable_goal_tags_printing = ref false let enable_goal_names_printing = ref false @@ -104,10 +101,10 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_env env sigma t let pr_constr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_constr_env env sigma t let pr_open_lconstr (_,c) = pr_lconstr c @@ -127,10 +124,10 @@ 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) = get_current_context () in + 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) = get_current_context () in + 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 = @@ -142,10 +139,10 @@ let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) let pr_ltype t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_ltype_env env sigma t let pr_type t = - let (sigma, env) = get_current_context () in + 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 @@ -156,7 +153,7 @@ 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) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_ljudge_env env sigma j let pr_lglob_constr_env env c = @@ -165,10 +162,10 @@ 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) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lglob_constr_env env c let pr_glob_constr c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_glob_constr_env env c let pr_closed_glob_n_env env sigma n c = @@ -176,7 +173,7 @@ let pr_closed_glob_n_env env sigma n 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) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_closed_glob_env env sigma c let pr_lconstr_pattern_env env sigma c = @@ -188,10 +185,10 @@ 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) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_pattern_env env sigma t let pr_constr_pattern t = - let (sigma, env) = get_current_context () in + 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) @@ -253,11 +250,11 @@ 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) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in safe_pr_lconstr_env env sigma t let safe_pr_constr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in safe_pr_constr_env env sigma t let pr_universe_ctx sigma c = @@ -788,7 +785,7 @@ let pr_goal x = !printer_pr.pr_goal x (* End abstraction layer *) (**********************************************************************) -let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = +let pr_open_subgoals ~proof = (* spiwack: it shouldn't be the job of the printer to look up stuff in the [evar_map], I did stuff that way because it was more straightforward, but seriously, [Proof.proof] should return @@ -826,15 +823,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused end -let pr_nth_open_subgoal n = - let pf = Proof_global.give_me_the_proof () in - let gls,_,_,_,sigma = Proof.proof pf in +let pr_nth_open_subgoal ~proof n = + let gls,_,_,_,sigma = Proof.proof proof in pr_subgoal n sigma gls -let pr_goal_by_id id = - let p = Proof_global.give_me_the_proof () in +let pr_goal_by_id ~proof id = try - Proof.in_proof p (fun sigma -> + Proof.in_proof proof (fun sigma -> let g = Evd.evar_key id sigma in pr_selected_subgoal (pr_id id) sigma g) with Not_found -> user_err Pp.(str "No such goal.") @@ -916,7 +911,7 @@ let pr_assumptionset env s = with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = - let sigma, env = get_current_context () in + let sigma, env = Pfedit.get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () diff --git a/printing/printer.mli b/printing/printer.mli index fbba14ede..e014baa2c 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -27,10 +27,12 @@ val enable_goal_names_printing : bool ref 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_term.tolerability -> constr -> Pp.t @@ -41,14 +43,18 @@ val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> co 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_term.tolerability -> EConstr.t -> Pp.t @@ -57,41 +63,53 @@ 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_term.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 @@ -166,8 +184,8 @@ val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar l val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals : ?proof:Proof.proof -> unit -> Pp.t -val pr_nth_open_subgoal : int -> Pp.t +val pr_open_subgoals : proof:Proof.proof -> Pp.t +val pr_nth_open_subgoal : proof:Proof.proof -> int -> Pp.t val pr_evar : evar_map -> (evar * evar_info) -> Pp.t val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t @@ -200,13 +218,13 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> types ContextObjectMap.t -> Pp.t -val pr_goal_by_id : Id.t -> Pp.t +val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t type printer_pr = { pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; -};; +} val set_printer_pr : printer_pr -> unit diff --git a/printing/printmod.ml b/printing/printmod.ml index 0abca0160..13a03e9b4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -374,9 +374,12 @@ let rec print_typ_expr env mp locals mty = | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in + (* XXX: What should env and sigma be here? *) + let env = Global.env () in + let sigma = Evd.empty in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() - ++ Printer.pr_lconstr c) + ++ Printer.pr_lconstr_env env sigma c) | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ diff --git a/stm/stm.ml b/stm/stm.ml index 864fff9e0..a9cbcc9a6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1931,9 +1931,10 @@ end = struct (* {{{ *) let open Notations in match Future.join f with | Some (pt, uc) -> + let sigma, env = Pfedit.get_current_context () in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ - str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ + str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> diff --git a/tactics/auto.ml b/tactics/auto.ml index d0424eb89..fa8435d1f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -388,7 +388,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) else Tacticals.New.tclFAIL 0 (str"Unbound reference") end - | Extern tacast -> + | Extern tacast -> conclPattern concl p tacast in let pr_hint () = @@ -396,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint t ++ origin + let sigma, env = Pfedit.get_current_context () in + pr_hint env sigma t ++ origin in tclLOG dbg pr_hint (run_hint t tactic) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e68087f14..6a9cd7e20 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -74,12 +74,12 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb bas = +let print_rewrite_hintdb env sigma bas = (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index d2b5e070b..44acf3c01 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : string -> Pp.t +val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t open Clenv diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b98b10315..cee6d4bea 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -464,15 +464,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co in let tac = run_hint t tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in + let _, env = Pfedit.get_current_context () in let pp = match p with | Some pat when get_typeclasses_filtered_unification () -> - str " with pattern " ++ Printer.pr_constr_pattern pat + str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat | _ -> mt () in match repr_hint t with - | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp)) - | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp)) + | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp)) + | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db secvars only_classes sigma concl = diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 239661498..f5c6ab879 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -178,7 +178,8 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - (tac, lazy (pr_hint t))) + let sigma, env = Pfedit.get_current_context () in + (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl diff --git a/tactics/hints.ml b/tactics/hints.ml index 99be1846c..70e84013b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1392,14 +1392,14 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint_elt (c, _, _) = pr_econstr c +let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c -let pr_hint h = match h.obj with - | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c) - | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c) - | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c) +let pr_hint env sigma h = match h.obj with + | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c) + | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c) + | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> - (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial") + (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> let env = @@ -1410,21 +1410,21 @@ let pr_hint h = match h.obj with in (str "(*external*) " ++ Pputils.pr_glb_generic env tac) -let pr_id_hint (id, v) = - let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in - (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat +let pr_id_hint env sigma (id, v) = + let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in + (pr_hint env sigma v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat ++ str", id " ++ int id ++ str ")" ++ spc ()) -let pr_hint_list hintlist = - (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) +let pr_hint_list env sigma hintlist = + (str " " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ()) -let pr_hints_db (name,db,hintlist) = +let pr_hints_db env sigma (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ if List.is_empty hintlist then (str " nothing" ++ fnl ()) - else (fnl () ++ pr_hint_list hintlist)) + else (fnl () ++ pr_hint_list env sigma hintlist)) (* Print all hints associated to head c in any database *) -let pr_hint_list_for_head c = +let pr_hint_list_for_head env sigma c = let dbs = current_db () in let validate (name, db) = let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in @@ -1436,13 +1436,13 @@ let pr_hint_list_for_head c = else hov 0 (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let pr_hint_term sigma cl = +let pr_hint_term env sigma cl = try let dbs = current_db () in let valid_dbs = @@ -1460,18 +1460,19 @@ let pr_hint_term sigma cl = (str "No hint applicable for current goal") else (str "Applicable Hints :" ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) with Match_failure _ | Failure _ -> (str "No hint applicable for current goal") (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint () = + let env = Global.env () in let pts = Proof_global.give_me_the_proof () in let glss,_,_,_,sigma = Proof.proof pts in match glss with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> - pr_hint_term sigma (Goal.V82.concl sigma g) + pr_hint_term env sigma (Goal.V82.concl sigma g) let pp_hint_mode = function | ModeInput -> str"+" @@ -1479,9 +1480,9 @@ let pp_hint_mode = function | ModeOutput -> str"-" (* displays the whole hint database db *) -let pr_hint_db db = +let pr_hint_db_env env sigma db = let pr_mode = prvect_with_sep spc pp_hint_mode in - let pr_modes l = + let pr_modes l = if List.is_empty l then mt () else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")" in @@ -1491,7 +1492,7 @@ let pr_hint_db db = | None -> str "For any goal" | Some head -> str "For " ++ pr_global head ++ pr_modes modes in - let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in + let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in accu ++ hint_descr in @@ -1506,17 +1507,21 @@ let pr_hint_db db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content -let pr_hint_db_by_name dbname = +let pr_hint_db db = + let sigma, env = Pfedit.get_current_context () in + pr_hint_db_env env sigma db + +let pr_hint_db_by_name env sigma dbname = try - let db = searchtable_map dbname in pr_hint_db db + let db = searchtable_map dbname in pr_hint_db_env env sigma db with Not_found -> error_no_such_hint_database dbname (* displays all the hints of all databases *) -let pr_searchtable () = +let pr_searchtable env sigma = let fold name db accu = accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++ - pr_hint_db db ++ fnl () + pr_hint_db_env env sigma db ++ fnl () in Hintdbmap.fold fold !searchtable (mt ()) @@ -1534,10 +1539,13 @@ let warn_non_imported_hint = strbrk "Hint used but not imported: " ++ hint ++ print_mp mp) let warn h x = - let hint = pr_hint h in - let (mp, _, _) = KerName.repr h.uid in - warn_non_imported_hint (hint,mp); - Proofview.tclUNIT x + let open Proofview in + tclBIND tclENV (fun env -> + tclBIND tclEVARMAP (fun sigma -> + let hint = pr_hint env sigma h in + let (mp, _, _) = KerName.repr h.uid in + warn_non_imported_hint (hint,mp); + Proofview.tclUNIT x)) let run_hint tac k = match !warn_hint with | `LAX -> k tac.obj diff --git a/tactics/hints.mli b/tactics/hints.mli index 22df29b80..cbf204981 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -260,14 +260,15 @@ val rewrite_db : hint_db_name (** Printing hints *) -val pr_searchtable : unit -> Pp.t +val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : global_reference -> Pp.t -val pr_hint_db_by_name : hint_db_name -> Pp.t +val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t +val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t -val pr_hint : hint -> Pp.t +[@@ocaml.deprecated "please used pr_hint_db_env"] +val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) - val add_hints_init : (unit -> unit) -> unit diff --git a/tactics/inv.ml b/tactics/inv.ml index 8648dfb90..46b10bf33 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -282,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id = let error_too_many_names pats = let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") let get_names (allow_conj,issimple) (loc, pat as x) = match pat with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 15c25b346..e072bd95f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -945,10 +945,14 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = - let trace () = + let trace env sigma = let open Printer in - let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in - Pp.(hov 2 (Pputils.pr_red_expr pr str redexp)) + let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in + Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp)) + in + let trace () = + let sigma, env = Pfedit.get_current_context () in + trace env sigma in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> @@ -3128,11 +3132,11 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] let warn_unused_intro_pattern env sigma = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" - (fun names -> - strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") - ++ str": " ++ prlist_with_sep spc - (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c env sigma)))) names) + (fun names -> + strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ + str": " ++ prlist_with_sep spc + (Miscprint.pr_intro_pattern + (fun c -> Printer.pr_econstr_env env sigma (snd (c env sigma)))) names) let check_unused_names env sigma names = if not (List.is_empty names) then diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f3d5d9b85..c61a1fd41 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -844,8 +844,10 @@ let start () = exit 1 | _ -> flush_all(); - if !output_context then - Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); + if !output_context then begin + let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) + end; Profile.print_profile (); exit 0 diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cf63fbdc3..8fdaedbaf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -100,7 +100,9 @@ let print_cmd_header ?loc com = Format.pp_print_flush !Topfmt.std_ft () let pr_open_cur_subgoals () = - try Printer.pr_open_subgoals () + try + let proof = Proof_global.give_me_the_proof () in + Printer.pr_open_subgoals ~proof with Proof_global.NoCurrentProof -> Pp.str "" (* Reenable when we get back to feedback printing *) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9e63df51d..51dd5cd4f 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -377,6 +377,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Proofview.Goal.enter begin fun gl -> let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let u,v = destruct_ind sigma type_of_pq in let lb_type_of_p = try @@ -389,7 +390,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_econstr type_of_pq ++ + Printer.pr_econstr_env env sigma type_of_pq ++ str " first.") in Tacticals.New.tclZEROMSG err_msg @@ -442,6 +443,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = Proofview.Goal.enter begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind sigma tt1 @@ -461,7 +463,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_econstr tt1 ++ + Printer.pr_econstr_env env sigma tt1 ++ str " first.") in user_err err_msg diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 2178a7caa..3a8e8fb43 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -76,7 +76,8 @@ let process_vernac_interp_error exn = match fst exn with | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error exn (Himsg.explain_refiner_error e) + let sigma, env = Pfedit.get_current_context () in + wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ diff --git a/vernac/himsg.ml b/vernac/himsg.ml index d15a811ba..839064aa0 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -92,9 +92,7 @@ let jv_nf_betaiotaevar sigma jl = (** Printers *) -let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e s c = quote (pr_lconstr_env e s c) -let pr_leconstr c = quote (pr_leconstr c) let pr_leconstr_env e s c = quote (pr_leconstr_env e s c) let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) @@ -1037,52 +1035,52 @@ let explain_typeclass_error env = function (* Refiner errors *) -let explain_refiner_bad_type arg ty conclty = +let explain_refiner_bad_type env sigma arg ty conclty = str "Refiner was given an argument" ++ brk(1,1) ++ - pr_lconstr arg ++ spc () ++ - str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ - str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "." + 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 "." let explain_refiner_unresolved_bindings l = str "Unable to find an instance for the " ++ str (String.plural (List.length l) "variable") ++ spc () ++ prlist_with_sep pr_comma Name.print l ++ str"." -let explain_refiner_cannot_apply t harg = +let explain_refiner_cannot_apply env sigma t harg = str "In refiner, a term of type" ++ brk(1,1) ++ - pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ - pr_lconstr harg ++ str "." + pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ + pr_lconstr_env env sigma harg ++ str "." -let explain_refiner_not_well_typed c = - str "The term " ++ pr_lconstr c ++ str " is not well-typed." +let explain_refiner_not_well_typed env sigma c = + str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed." let explain_intro_needs_product () = str "Introduction tactics needs products." -let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ +let explain_does_not_occur_in env sigma c hyp = + str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." -let explain_non_linear_proof c = - str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ +let explain_non_linear_proof env sigma c = + str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++ spc () ++ str "because a metavariable has several occurrences." -let explain_meta_in_type c = - str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++ +let explain_meta_in_type env sigma c = + str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr_env env sigma c ++ str " of another meta" let explain_no_such_hyp id = str "No such hypothesis: " ++ Id.print id -let explain_refiner_error = function - | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty +let explain_refiner_error env sigma = function + | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t - | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg - | NotWellTyped c -> explain_refiner_not_well_typed c + | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg + | NotWellTyped c -> explain_refiner_not_well_typed env sigma c | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp - | NonLinearProof c -> explain_non_linear_proof c - | MetaInType c -> explain_meta_in_type c + | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp + | NonLinearProof c -> explain_non_linear_proof env sigma c + | MetaInType c -> explain_meta_in_type env sigma c | NoSuchHyp id -> explain_no_such_hyp id (* Inductive errors *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 5b91f9e68..8945ebadb 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t -val explain_refiner_error : refiner_error -> Pp.t +val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t val explain_pattern_matching_error : env -> Evd.evar_map -> pattern_matching_error -> Pp.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7b8a38d5f..a025bfff8 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -253,7 +253,9 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) | App (t, args) -> mkApp (body_i t, args) - | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in + | _ -> + let sigma, env = Pfedit.get_current_context () in + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in let body_i = body_i body in match locality with | Discharge -> @@ -530,7 +532,5 @@ let save_proof ?proof = function Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) +let get_current_context () = Pfedit.get_current_context () -let get_current_context () = - Pfedit.get_current_context () - diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 6972edd52..1b1304db5 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -66,3 +66,4 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni and the current global env *) val get_current_context : unit -> Evd.evar_map * Environ.env +[@@ocaml.deprecated "please use [Pfedit.get_current_context]"] diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c00b107cf..10c139e5a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -56,8 +56,9 @@ let scope_class_of_qualid qid = let show_proof () = (* spiwack: this would probably be cooler with a bit of polishing. *) let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf) + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) @@ -255,7 +256,8 @@ let print_namespace ns = let print_constant k body = (* FIXME: universes *) let t = body.Declarations.const_type in - print_kn k ++ str":" ++ spc() ++ Printer.pr_type t + let sigma, env = Pfedit.get_current_context () in + print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t in let matches mp = match match_modulepath ns mp with | Some [] -> true @@ -484,8 +486,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = let red_option = match red_option with | None -> None | Some r -> - let (evc,env)= get_current_context () in - Some (snd (Hook.get f_interp_redexp env evc r)) in + let sigma, env= Pfedit.get_current_context () in + Some (snd (Hook.get f_interp_redexp env sigma r)) in do_definition id (local,p,k) pl bl red_option c typ_opt hook) let vernac_start_proof locality p kind l = @@ -1537,7 +1539,7 @@ let vernac_print_option key = let get_current_context_of_args = function | Some n -> Pfedit.get_goal_context n - | None -> get_current_context () + | None -> Pfedit.get_current_context () let query_command_selector ?loc = function | None -> None @@ -1626,17 +1628,20 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl() + let sigma, env = Pfedit.get_current_context () in + v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) - | NoHyp | Not_found -> print_about ref_or_by_not + | NoHyp | Not_found -> + let sigma, env = Pfedit.get_current_context () in + print_about env sigma ref_or_by_not - -let vernac_print ?loc = let open Feedback in function + +let vernac_print ?loc env sigma = let open Feedback in function | PrintTables -> msg_notice (print_tables ()) - | PrintFullContext-> msg_notice (print_full_context_typ ()) - | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) - | PrintInspect n -> msg_notice (inspect n) + | PrintFullContext-> msg_notice (print_full_context_typ env sigma) + | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) + | PrintInspect n -> msg_notice (inspect env sigma n) | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent) | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir) | PrintModules -> msg_notice (print_modules ()) @@ -1646,15 +1651,15 @@ let vernac_print ?loc = let open Feedback in function | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName qid -> dump_global qid; msg_notice (print_name qid) + | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid) | PrintGraph -> msg_notice (Prettyp.print_graph()) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintCoercions -> msg_notice (Prettyp.print_coercions()) + | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) - | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) + | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then UGraph.sort_universes univ else univ in @@ -1666,16 +1671,16 @@ let vernac_print ?loc = let open Feedback in function | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | Some s -> dump_universes_gen univ s end - | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) + | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) - | PrintHintDb -> msg_notice (Hints.pr_searchtable ()) + | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s) + | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma) | PrintScopes -> - msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) + msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))) | PrintScope s -> - msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) + msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) | PrintVisibility s -> - msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) + msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) | PrintAbout (ref_or_by_not,glnumopt) -> msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt) | PrintImplicit qid -> @@ -1778,9 +1783,10 @@ let vernac_locate = let open Feedback in function | LocateTerm (AN qid) -> msg_notice (print_located_term qid) | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, (ntn, sc))) -> - msg_notice - (Notation.locate_notation - (Constrextern.without_symbols pr_lglob_constr) ntn sc) + let _, env = Pfedit.get_current_context () in + msg_notice + (Notation.locate_notation + (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> msg_notice (print_located_module qid) | LocateOther (s, qid) -> msg_notice (print_located_other s qid) @@ -1847,10 +1853,11 @@ let vernac_bullet (bullet : Proof_bullet.t) = let vernac_show = let open Feedback in function | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> + let proof = Proof_global.give_me_the_proof () in let info = match goalref with - | OpenSubgoals -> pr_open_subgoals () - | NthGoal n -> pr_nth_open_subgoal n - | GoalId id -> pr_goal_by_id id + | OpenSubgoals -> pr_open_subgoals ~proof + | NthGoal n -> pr_nth_open_subgoal ~proof n + | GoalId id -> pr_goal_by_id ~proof id in msg_notice info | ShowProof -> show_proof () @@ -2041,7 +2048,9 @@ let interp ?proof ?loc locality poly st c = | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r | VernacGlobalCheck c -> vernac_global_check c - | VernacPrint p -> vernac_print ?loc p + | VernacPrint p -> + let sigma, env = Pfedit.get_current_context () in + vernac_print ?loc env sigma p | VernacSearch (s,g,r) -> vernac_search ?loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r |