diff options
38 files changed, 133 insertions, 160 deletions
diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh new file mode 100644 index 0000000000..81ed91f52b --- /dev/null +++ b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then + + Elpi_CI_REF=master+generalized-evar-printers-pr8688 + Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 44d44ccc4b..fd08f9ffe8 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -168,8 +168,8 @@ let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(Termops.pr_metaset metas) -let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd) -let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) (Global.env ()) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None (Global.env ()) evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = @@ -180,14 +180,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with 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 ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g)) 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) + pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) (Global.env ()) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) (Global.env ()) evd ++ envpp pr_econstr_env c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) diff --git a/engine/termops.ml b/engine/termops.ml index 5e220fd8f1..f720e5195d 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -104,12 +104,7 @@ let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c) let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c) let term_printer = ref debug_print_constr_env -let print_constr_env env sigma t = !term_printer env sigma t -let print_constr t = - let env = Global.env () in - let evd = Evd.from_env env in - !term_printer env evd t - +let print_constr_env env sigma t = !term_printer (env:env) sigma (t:Evd.econstr) let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -164,10 +159,10 @@ let protect f x = try f x with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) -let print_kconstr a = - protect (fun c -> print_constr c) a +let print_kconstr env sigma a = + protect (fun c -> print_constr_env env sigma c) a -let pr_meta_map evd = +let pr_meta_map env sigma = let open Evd in let print_constr = print_kconstr in let pr_name = function @@ -177,25 +172,25 @@ let pr_meta_map evd = | (mv,Cltyp (na,b)) -> hov 0 (pr_meta mv ++ pr_name na ++ str " : " ++ - print_constr b.rebus ++ fnl ()) + print_constr env sigma b.rebus ++ fnl ()) | (mv,Clval(na,(b,s),t)) -> hov 0 (pr_meta mv ++ pr_name na ++ str " := " ++ - print_constr b.rebus ++ - str " : " ++ print_constr t.rebus ++ + print_constr env sigma b.rebus ++ + str " : " ++ print_constr env sigma t.rebus ++ spc () ++ pr_instance_status s ++ fnl ()) in - prlist pr_meta_binding (meta_list evd) + prlist pr_meta_binding (meta_list sigma) -let pr_decl (decl,ok) = +let pr_decl env sigma (decl,ok) = let open NamedDecl in let print_constr = print_kconstr in match decl with | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}") | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++ - print_constr c ++ str (if ok then ")" else "}") + print_constr env sigma c ++ str (if ok then ")" else "}") -let pr_evar_source = function +let pr_evar_source env sigma = function | Evar_kinds.NamedHole id -> Id.print id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" @@ -208,11 +203,11 @@ let pr_evar_source = function let print_constr = print_kconstr in let id = Option.get ido in str "parameter " ++ Id.print id ++ spc () ++ str "of" ++ - spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c) + spc () ++ print_constr env sigma (EConstr.of_constr @@ printable_constr_of_global c) | Evar_kinds.InternalHole -> str "internal placeholder" | Evar_kinds.TomatchTypeParameter (ind,n) -> let print_constr = print_kconstr in - pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind) + pr_nth n ++ str " argument of type " ++ print_constr env sigma (EConstr.mkInd ind) | Evar_kinds.GoalEvar -> str "goal evar" | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" @@ -224,7 +219,7 @@ let pr_evar_source = function | Some Evar_kinds.Domain -> str "domain of " | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk -let pr_evar_info evi = +let pr_evar_info env sigma evi = let open Evd in let print_constr = print_kconstr in let phyps = @@ -233,23 +228,23 @@ let pr_evar_info evi = | None -> List.map (fun c -> (c, true)) (evar_context evi) | Some filter -> List.combine (evar_context evi) filter in - prlist_with_sep spc pr_decl (List.rev decls) + prlist_with_sep spc (pr_decl env sigma) (List.rev decls) with Invalid_argument _ -> str "Ill-formed filtered context" in - let pty = print_constr evi.evar_concl in + let pty = print_constr env sigma evi.evar_concl in let pb = match evi.evar_body with | Evar_empty -> mt () - | Evar_defined c -> spc() ++ str"=> " ++ print_constr c + | Evar_defined c -> spc() ++ str"=> " ++ print_constr env sigma c in let candidates = match evi.evar_body, evi.evar_candidates with | Evar_empty, Some l -> spc () ++ str "{" ++ - prlist_with_sep (fun () -> str "|") print_constr l ++ str "}" + prlist_with_sep (fun () -> str "|") (print_constr env sigma) l ++ str "}" | _ -> mt () in - let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in + let src = str "(" ++ pr_evar_source env sigma (snd evi.evar_source) ++ str ")" in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++ candidates ++ spc() ++ src) @@ -304,8 +299,8 @@ let has_no_evar sigma = try let () = Evd.fold (fun _ _ () -> raise Exit) sigma () in true with Exit -> false -let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) -let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l +let pr_evd_level sigma = UState.pr_uctx_level (Evd.evar_universe_context sigma) +let reference_of_level sigma l = UState.qualid_of_level (Evd.evar_universe_context sigma) l let pr_evar_universe_context ctx = let open UState in @@ -321,12 +316,12 @@ let pr_evar_universe_context ctx = str "WEAK CONSTRAINTS:"++brk(0,1)++ h 0 (UState.pr_weak prl ctx) ++ fnl ()) -let print_env_short env = +let print_env_short env sigma = let print_constr = print_kconstr in let pr_rel_decl = function | RelDecl.LocalAssum (n,_) -> Name.print n | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " - ++ print_constr (EConstr.of_constr b) ++ str ")" + ++ print_constr env sigma (EConstr.of_constr b) ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in @@ -346,7 +341,7 @@ let pr_evar_constraints sigma pbs = naming/renaming. *) Namegen.make_all_name_different env sigma in - print_env_short env ++ spc () ++ str "|-" ++ spc () ++ + print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++ protect (print_constr_env env sigma) t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" @@ -355,7 +350,7 @@ let pr_evar_constraints sigma pbs = in prlist_with_sep fnl pr_evconstr pbs -let pr_evar_map_gen with_univs pr_evars sigma = +let pr_evar_map_gen with_univs pr_evars env sigma = let uvs = Evd.evar_universe_context sigma in let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl () @@ -374,15 +369,15 @@ let pr_evar_map_gen with_univs pr_evars sigma = and metas = if List.is_empty (Evd.meta_list sigma) then mt () else - str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma + str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma in evs ++ svs ++ cstrs ++ typeclasses ++ metas -let pr_evar_list sigma l = +let pr_evar_list env sigma l = let open Evd in let pr (ev, evi) = h 0 (Evar.print ev ++ - str "==" ++ pr_evar_info evi ++ + str "==" ++ pr_evar_info env sigma evi ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) @@ -405,18 +400,18 @@ let to_list d = Evd.fold fold_undef d (); !l -let pr_evar_by_depth depth sigma = match depth with +let pr_evar_by_depth depth env sigma = match depth with | None -> (* Print all evars *) - str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl() + str"EVARS:" ++ brk(0,1) ++ pr_evar_list env sigma (to_list sigma) ++ fnl() | Some n -> (* Print closure of undefined evars *) str"UNDEFINED EVARS:"++ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++ brk(0,1)++ - pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl() + pr_evar_list env sigma (evar_dependency_closure n sigma) ++ fnl() -let pr_evar_by_filter filter sigma = +let pr_evar_by_filter filter env sigma = let open Evd in let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in let elts = List.rev elts in @@ -431,49 +426,49 @@ let pr_evar_by_filter filter sigma = let prdef = if List.is_empty defined then mt () else str "DEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list sigma defined + pr_evar_list env sigma defined in let prundef = if List.is_empty undefined then mt () else str "UNDEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list sigma undefined + pr_evar_list env sigma undefined in prdef ++ prundef -let pr_evar_map ?(with_univs=true) depth sigma = - pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma +let pr_evar_map ?(with_univs=true) depth env sigma = + pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth env sigma) env sigma -let pr_evar_map_filter ?(with_univs=true) filter sigma = - pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma +let pr_evar_map_filter ?(with_univs=true) filter env sigma = + pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter env sigma) env sigma let pr_metaset metas = str "[" ++ pr_sequence pr_meta (Evd.Metaset.elements metas) ++ str "]" let pr_var_decl env decl = let open NamedDecl in - let evd = Evd.from_env env in + let sigma = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env evd c in + let pb = print_constr_env env sigma c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in + let pt = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in - let evd = Evd.from_env env in + let sigma = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env evd c in + let pb = print_constr_env env sigma c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in + let ptyp = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) diff --git a/engine/termops.mli b/engine/termops.mli index f7b9469ae8..1054fbbc5e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -304,11 +304,11 @@ val pr_existential_key : evar_map -> Evar.t -> Pp.t val pr_evar_suggested_name : Evar.t -> evar_map -> Id.t -val pr_evar_info : evar_info -> Pp.t +val pr_evar_info : env -> evar_map -> evar_info -> Pp.t val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t +val pr_evar_map : ?with_univs:bool -> int option -> env -> evar_map -> Pp.t val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.t + env -> evar_map -> Pp.t val pr_metaset : Metaset.t -> Pp.t val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t diff --git a/interp/declare.mli b/interp/declare.mli index 02e73cd66c..468e056909 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Libnames open Constr open Entries open Decl_kinds @@ -29,7 +28,7 @@ type section_variable_entry = type variable_declaration = DirPath.t * section_variable_entry * logical_kind -val declare_variable : variable -> variable_declaration -> object_name +val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) @@ -69,7 +68,7 @@ val set_declare_scheme : (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> object_name * bool +val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool (** Declaration messages *) diff --git a/library/declaremods.mli b/library/declaremods.mli index b42a59bfbd..7aa4bc30ce 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -130,7 +130,7 @@ val declare_include : (together with their section path). *) val iter_all_segments : - (Libnames.object_name -> Libobject.obj -> unit) -> unit + (Libobject.object_name -> Libobject.obj -> unit) -> unit val debug_print_modtab : unit -> Pp.t diff --git a/library/lib.ml b/library/lib.ml index 27c5056a7f..1acc8fd8fd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -138,7 +138,7 @@ let make_kn id = let mp = current_mp () in Names.KerName.make mp (Names.Label.of_id id) -let make_oname id = Libnames.make_oname !lib_state.path_prefix id +let make_oname id = Libobject.make_oname !lib_state.path_prefix id let recalc_path_prefix () = let rec recalc = function diff --git a/library/lib.mli b/library/lib.mli index 686e6a0e2d..c6c6a307d4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -25,7 +25,7 @@ type node = | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | OpenedSection of Libnames.object_prefix * Summary.frozen -type library_segment = (Libnames.object_name * node) list +type library_segment = (Libobject.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list @@ -53,13 +53,13 @@ val segment_of_objects : (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libnames.object_name -> unit +val pull_to_head : Libobject.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name (** {6 ... } *) @@ -70,7 +70,7 @@ val contents : unit -> library_segment (** The function [contents_after] returns the current library segment, starting from a given section path. *) -val contents_after : Libnames.object_name -> library_segment +val contents_after : Libobject.object_name -> library_segment (** {6 Functions relative to current path } *) @@ -113,20 +113,20 @@ val start_modtype : val end_module : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Libnames.object_prefix * Summary.frozen * library_segment val end_modtype : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Libnames.object_prefix * Summary.frozen * library_segment (** {6 Compilation units } *) val start_compilation : DirPath.t -> ModPath.t -> unit -val end_compilation_checks : DirPath.t -> Libnames.object_name +val end_compilation_checks : DirPath.t -> Libobject.object_name val end_compilation : - Libnames.object_name-> Libnames.object_prefix * library_segment + Libobject.object_name-> Libnames.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) diff --git a/library/libnames.ml b/library/libnames.ml index bd2ca550b9..f6fc5ed4b7 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,18 +162,12 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath -type object_name = full_path * KerName.t - type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; obj_sec : DirPath.t; } -(* let make_oname (dirpath,(mp,dir)) id = *) -let make_oname { obj_dir; obj_mp } id = - make_path obj_dir id, KerName.make obj_mp (Label.of_id id) - (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix diff --git a/library/libnames.mli b/library/libnames.mli index 447eecbb5c..9d75ec6e40 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,12 +88,6 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t -(** Both names are passed to objects: a "semantic" [kernel_name], which - can be substituted and a "syntactic" [full_path] which can be printed -*) - -type object_name = full_path * KerName.t - (** Object prefix morally contains the "prefix" naming of an object to be stored by [library], where [obj_dir] is the "absolute" path, [obj_mp] is the current "module" prefix and [obj_sec] is the @@ -116,8 +110,6 @@ type object_prefix = { val eq_op : object_prefix -> object_prefix -> bool -val make_oname : object_prefix -> Id.t -> object_name - (** to this type are mapped [DirPath.t]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix diff --git a/library/libobject.ml b/library/libobject.ml index 79a3fed1b9..ea19fbb90b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -16,6 +16,12 @@ module Dyn = Dyn.Make () type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +type object_name = Libnames.full_path * Names.KerName.t + +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname { obj_dir; obj_mp } id = + Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id)) + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/library/libobject.mli b/library/libobject.mli index aefa81b225..c53537e654 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -66,6 +66,13 @@ open Mod_subst type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +(** Both names are passed to objects: a "semantic" [kernel_name], which + can be substituted and a "syntactic" [full_path] which can be printed +*) + +type object_name = full_path * Names.KerName.t +val make_oname : object_prefix -> Names.Id.t -> object_name + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ad1114b733..d4e410bd69 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -229,10 +229,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t = true with Not_found -> false -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env - - exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = @@ -420,7 +416,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in - let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in + let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp @@ -800,7 +796,7 @@ let build_proof g | LetIn _ -> let new_infos = - { dyn_infos with info = nf_betaiotazeta dyn_infos.info } + { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in tclTHENLIST @@ -834,7 +830,7 @@ let build_proof | LetIn _ -> let new_infos = { dyn_infos with - info = nf_betaiotazeta dyn_infos.info + info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in @@ -977,7 +973,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "body " ++ pr_lconstr bodies.(num)); *) let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) - let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in + let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b0842c3721..96eb7fbc60 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -63,12 +63,6 @@ let observe_tac s tac g = then do_observe_tac (str s) tac g else tac g -(* [nf_zeta] $\zeta$-normalization of a term *) -let nf_zeta = - Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - Environ.empty_env - (Evd.from_env Environ.empty_env) - let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl (* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *) @@ -219,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let mib,_ = Global.lookup_inductive graph_ind in (* and the principle to use in this lemma in $\zeta$ normal form *) let f_principle,princ_type = schemes.(i) in - let princ_type = nf_zeta princ_type in + let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in let princ_infos = Tactics.compute_elim_sig evd princ_type in (* The number of args of the function is then easily computable *) let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in @@ -397,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in - (nf_zeta p)::bindings,id::avoid) + (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) @@ -630,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti *) let lemmas = Array.map - (fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt)) + (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt)) lemmas_types_infos in (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in - let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in + let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in let princ_type = pf_unsafe_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig (project g) princ_type in (* Then we get the number of argument of the function @@ -771,7 +765,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in evd := sigma; - let type_of_lemma = nf_zeta type_of_lemma in + let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info ) @@ -838,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let type_of_lemma = nf_zeta type_of_lemma in + let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f9df3aed45..63a3e0582d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -103,21 +103,6 @@ let const_of_ref = function ConstRef kn -> kn | _ -> anomaly (Pp.str "ConstRef expected.") - -let nf_zeta env = - Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - env (Evd.from_env env) - - -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env - (Evd.from_env Environ.empty_env) - - - - - - (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in @@ -747,7 +732,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_env (pf_env g) sigma 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 = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) )) g @@ -1537,13 +1522,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in - let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in + let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in - let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in + let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in let eq' = EConstr.Unsafe.to_constr eq' in let res = (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9f7669f1d5..8b2721ae4e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1492,7 +1492,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul if not (Evd.is_defined acc ev) then user_err ~hdr:"rewrite" (str "Unsolved constraint remaining: " ++ spc () ++ - Termops.pr_evar_info (Evd.find acc ev)) + Termops.pr_evar_info env acc (Evd.find acc ev)) else Evd.remove acc ev) cstrs evars' in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 16cff420bd..0f88734caf 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -353,7 +353,7 @@ let extend_atomic_tactic name entries = let default = epsilon_value inj e in match default with | None -> raise NonEmptyArgument - | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def + | Some def -> Tacintern.intern_tactic_or_tacarg (Genintern.empty_glob_sign Environ.empty_env) def in try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 55412c74bb..fcbcfae115 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -46,7 +46,6 @@ type glob_sign = Genintern.glob_sign = { extra : Genintern.Store.t; } -let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) (* We have identifier <| global_reference <| constr *) @@ -83,7 +82,8 @@ let intern_hyp ist ({loc;v=id} as locid) = else if find_ident id ist then make id else - Pretype_errors.error_var_not_found ?loc id + CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++ + str "was not found in the current environment.") let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 9146fced2d..a9f2d76e30 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -23,10 +23,8 @@ type glob_sign = Genintern.glob_sign = { extra : Genintern.Store.t; } -val fully_empty_glob_sign : glob_sign - val make_empty_glob_sign : unit -> glob_sign - (** same as [fully_empty_glob_sign], but with [Global.env()] as + (** build an empty [glob_sign] using [Global.env()] as environment *) (** Main globalization functions *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b60b77595b..528d7de549 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2024,7 +2024,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k let interp_redexp env sigma r = let ist = default_ist () in - let gist = { fully_empty_glob_sign with genv = env; } in + let gist = Genintern.empty_glob_sign env in interp_red_expr ist env sigma (intern_red_expr gist r) (***************************************************************************) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index a284c3bfc7..5d75b28539 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -940,7 +940,7 @@ let pf_saturate ?beta ?bi_types gl c ?ty m = let pf_partial_solution gl t evl = let sigma, g = project gl, sig_it gl in - let sigma = Goal.V82.partial_solution sigma g t in + let sigma = Goal.V82.partial_solution (pf_env gl) sigma g t in re_sig (List.map (fun x -> (fst (EConstr.destEvar sigma x))) evl) sigma let dependent_apply_error = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index c04ced4ab4..036b20bfcd 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -433,15 +433,15 @@ let lz_coq_prod = let lz_setoid_relation = let sdir = ["Classes"; "RelationClasses"] in - let last_srel = ref (Environ.empty_env, None) in + let last_srel = ref None in fun env -> match !last_srel with - | env', srel when env' == env -> srel + | Some (env', srel) when env' == env -> srel | _ -> let srel = try Some (UnivGen.constr_of_global @@ Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"]) with _ -> None in - last_srel := (env, srel); srel + last_srel := Some (env, srel); srel let ssr_is_setoid env = match lz_setoid_relation env with diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7f67487f5d..bb6decd848 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1048,7 +1048,7 @@ let thin id sigma goal = | None -> sigma | Some (sigma, hyps, concl) -> let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in + let sigma = Goal.V82.partial_solution_to env sigma goal gl ev in sigma (* diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 856894d9a6..01b0d96f98 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -164,8 +164,8 @@ let error_not_product ?loc env sigma c = (*s Error in conversion from AST to glob_constr *) -let error_var_not_found ?loc s = - raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s) +let error_var_not_found ?loc env sigma s = + raise_pretype_error ?loc (env, sigma, VarNotFound s) (*s Typeclass errors *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 6f14d025c7..054f0c76a9 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -150,9 +150,7 @@ val error_unexpected_type : val error_not_product : ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b -(** {6 Error in conversion from AST to glob_constr } *) - -val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b +val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b (** {6 Typeclass errors } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 37afcf75e1..55817f1b76 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -390,7 +390,7 @@ let pretype_id pretype k0 loc env sigma id = sigma, { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) } with Not_found -> (* [id] not found, standard error message *) - error_var_not_found ?loc id + error_var_not_found ?loc !!env sigma id (*************************************************************************) (* Main pretyping function *) @@ -436,7 +436,7 @@ let pretype_ref ?loc sigma env ref us = (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal variables *) - Pretype_errors.error_var_not_found ?loc id) + Pretype_errors.error_var_not_found ?loc !!env sigma id) | ref -> let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in let ty = unsafe_type_of !!env sigma c in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 367a48cb5e..aced97e910 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1251,6 +1251,7 @@ let clos_whd_flags flgs env sigma t = let nf_beta = clos_norm_flags CClosure.beta let nf_betaiota = clos_norm_flags CClosure.betaiota let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta +let nf_zeta = clos_norm_flags CClosure.zeta let nf_all env sigma = clos_norm_flags CClosure.all env sigma diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index c0ff6723f6..41de779414 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -171,6 +171,7 @@ val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function val nf_beta : reduction_function val nf_betaiota : reduction_function val nf_betaiotazeta : reduction_function +val nf_zeta : reduction_function val nf_all : reduction_function val nf_evar : evar_map -> constr -> constr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8911a2f343..4ec8569dd8 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1135,8 +1135,8 @@ let fold_commands cl env sigma c = let cbv_norm_flags flags env sigma t = cbv_norm (create_cbv_infos flags env sigma) t -let cbv_beta = cbv_norm_flags beta empty_env -let cbv_betaiota = cbv_norm_flags betaiota empty_env +let cbv_beta = cbv_norm_flags beta +let cbv_betaiota = cbv_norm_flags betaiota let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma let compute = cbv_betadeltaiota diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index bf38c30a1f..0887d0efd3 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -69,8 +69,8 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function (** Call by value strategy (uses Closures) *) val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function - val cbv_beta : local_reduction_function - val cbv_betaiota : local_reduction_function + val cbv_beta : reduction_function + val cbv_betaiota : reduction_function val cbv_betadeltaiota : reduction_function val compute : reduction_function (** = [cbv_betadeltaiota] *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 58606db019..9213bc8561 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,7 +19,7 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref 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_library_entry : env -> Evd.evar_map -> bool -> (Libobject.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 @@ -89,7 +89,7 @@ type object_pr = { print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.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; diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d25ae38c53..d01338fa95 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -577,7 +577,7 @@ let pr_clenv clenv = h 0 (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ - pr_evar_map (Some 2) clenv.evd) + pr_evar_map (Some 2) clenv.env clenv.evd) (****************************************************************) (** Evar version of mk_clenv *) diff --git a/proofs/goal.ml b/proofs/goal.ml index 4e540de538..7245d4a004 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -72,18 +72,18 @@ module V82 = struct (evk, ev, evars) (* Instantiates a goal with an open term *) - let partial_solution sigma evk c = + let partial_solution env sigma evk c = (* Check that the goal itself does not appear in the refined term *) let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + else Pretype_errors.error_occur_check env sigma evk c in Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) - let partial_solution_to sigma evk evk' c = + let partial_solution_to env sigma evk evk' c = let id = Evd.evar_ident evk sigma in - let sigma = partial_solution sigma evk c in + let sigma = partial_solution env sigma evk c in match id with | None -> sigma | Some id -> Evd.rename evk' id sigma diff --git a/proofs/goal.mli b/proofs/goal.mli index 3b31cff8d7..af9fb662bf 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -48,11 +48,11 @@ module V82 : sig goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) - val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map + val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map (* Instantiates a goal with an open term, reusing name of goal for second goal *) - val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map + val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index 254c93d0a2..b8612cd2c0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -590,5 +590,5 @@ let prim_refiner r sigma goal = check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in + let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in (sgl, sigma) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 388bf8efb5..231a8fe266 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -130,10 +130,10 @@ let db_pr_goal sigma g = str" " ++ pc) ++ fnl () let pr_gls gls = - hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) + hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++ prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) (* Variants of [Tacmach] functions built with the new proof engine *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f302960870..14c83a6802 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -83,6 +83,7 @@ val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.t val pr_glls : goal list sigma -> Pp.t +[@@ocaml.deprecated "Please move to \"new\" proof engine"] (** Variants of [Tacmach] functions built with the new proof engine *) module New : sig diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ca77e03707..844caf5a3e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -769,7 +769,7 @@ let pr_constraints printenv env sigma evars cstrs = h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in - pr_evar_map_filter ~with_univs:false filter sigma + pr_evar_map_filter ~with_univs:false filter env sigma let explain_unsatisfiable_constraints env sigma constr comp = let (_, constraints) = Evd.extract_all_conv_pbs sigma in |