diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-17 20:17:17 +0530 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:16:44 +0530 |
commit | 237b569dd6539fc1730dbd1dda29f83e24ef8d0c (patch) | |
tree | 71c1eeaec02da28ae34f8428bab7ddcf7ecc251c | |
parent | 1c0110b40a9009aa6b56fafbf34a04e7ae59de0f (diff) |
Univs: proper printing of global and local universe names (only
printing functions touched in the kernel).
-rw-r--r-- | dev/top_printers.ml | 13 | ||||
-rw-r--r-- | interp/constrextern.ml | 2 | ||||
-rw-r--r-- | interp/constrextern.mli | 2 | ||||
-rw-r--r-- | kernel/univ.ml | 69 | ||||
-rw-r--r-- | kernel/univ.mli | 16 | ||||
-rw-r--r-- | library/universes.ml | 3 | ||||
-rw-r--r-- | library/universes.mli | 2 | ||||
-rw-r--r-- | pretyping/detyping.ml | 25 | ||||
-rw-r--r-- | pretyping/detyping.mli | 2 | ||||
-rw-r--r-- | pretyping/evd.ml | 35 | ||||
-rw-r--r-- | pretyping/evd.mli | 1 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 3 | ||||
-rw-r--r-- | pretyping/termops.ml | 2 | ||||
-rw-r--r-- | printing/pptactic.ml | 2 | ||||
-rw-r--r-- | printing/printer.ml | 12 | ||||
-rw-r--r-- | printing/printer.mli | 3 | ||||
-rw-r--r-- | tactics/inv.ml | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/3392.v | 2 | ||||
-rw-r--r-- | toplevel/cerrors.ml | 3 | ||||
-rw-r--r-- | toplevel/himsg.ml | 17 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 4 |
21 files changed, 119 insertions, 101 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 202f9db02..dea70360a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -207,21 +207,22 @@ let ppuni u = pp(pr_uni u) let ppuni_level u = pp (Level.pr u) let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]") -let ppuniverse_set l = pp (LSet.pr l) -let ppuniverse_instance l = pp (Instance.pr l) -let ppuniverse_context l = pp (pr_universe_context l) -let ppuniverse_context_set l = pp (pr_universe_context_set l) +let prlev = Universes.pr_with_global_universes +let ppuniverse_set l = pp (LSet.pr prlev l) +let ppuniverse_instance l = pp (Instance.pr prlev l) +let ppuniverse_context l = pp (pr_universe_context prlev l) +let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) let ppconstraints_map c = pp (Universes.pr_constraints_map c) -let ppconstraints c = pp (pr_constraints c) +let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes u) +let ppuniverses u = pp (Univ.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4b20b024d..58e1eb1d1 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -956,7 +956,7 @@ let extern_type goal_concl_style env sigma t = let r = Detyping.detype goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r -let extern_sort s = extern_glob_sort (detype_sort s) +let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) let extern_closed_glob ?lax goal_concl_style env sigma t = let avoid = if goal_concl_style then ids_of_context env else [] in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d11248a59..b797e455c 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -40,7 +40,7 @@ val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr -val extern_sort : sorts -> glob_sort +val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder list diff --git a/kernel/univ.ml b/kernel/univ.ml index 7d64e894d..08e9fee05 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -343,8 +343,8 @@ end module LSet = struct include LMap.Set - let pr s = - str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}" + let pr prl s = + str"{" ++ prlist_with_sep spc prl (elements s) ++ str"}" let of_array l = Array.fold_left (fun acc x -> add x acc) empty l @@ -1265,10 +1265,10 @@ struct module S = Set.Make(UConstraintOrd) include S - let pr c = + let pr prl c = fold (fun (u1,op,u2) pp_std -> - pp_std ++ Level.pr u1 ++ pr_constraint_type op ++ - Level.pr u2 ++ fnl () ) c (str "") + pp_std ++ prl u1 ++ pr_constraint_type op ++ + prl u2 ++ fnl () ) c (str "") end @@ -1641,7 +1641,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds val levels : t -> LSet.t val check_eq : t check_function end = @@ -1718,7 +1718,7 @@ struct let levels x = LSet.of_array x let pr = - prvect_with_sep spc Level.pr + prvect_with_sep spc let equal t u = t == u || @@ -1764,9 +1764,9 @@ struct let empty = (Instance.empty, Constraint.empty) let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst - let pr (univs, cst as ctx) = + let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - Instance.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst) + Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1832,9 +1832,9 @@ struct let of_context (ctx, cst) = (Instance.levels ctx, cst) - let pr (univs, cst as ctx) = + let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - LSet.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst) + LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) let constraints (univs, cst) = cst let levels (univs, cst) = univs @@ -1983,7 +1983,7 @@ let abstract_universes poly ctx = (** Pretty-printing *) -let pr_arc = function +let pr_arc prl = function | _, Canonical {univ=u; lt=[]; le=[]} -> mt () | _, Canonical {univ=u; lt=lt; le=le} -> @@ -1991,20 +1991,20 @@ let pr_arc = function | [], _ | _, [] -> mt () | _ -> spc () in - Level.pr u ++ str " " ++ + prl u ++ str " " ++ v 0 - (pr_sequence (fun v -> str "< " ++ Level.pr v) lt ++ + (pr_sequence (fun v -> str "< " ++ prl v) lt ++ opt_sep ++ - pr_sequence (fun v -> str "<= " ++ Level.pr v) le) ++ + pr_sequence (fun v -> str "<= " ++ prl v) le) ++ fnl () | u, Equiv v -> - Level.pr u ++ str " = " ++ Level.pr v ++ fnl () + prl u ++ str " = " ++ prl v ++ fnl () -let pr_universes g = +let pr_universes prl g = let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in - prlist pr_arc graph + prlist (pr_arc prl) graph -let pr_constraints = Constraint.pr +let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr @@ -2049,21 +2049,22 @@ let hcons_universe_context_set (v, c) = let hcons_univ x = Universe.hcons x -let explain_universe_inconsistency (o,u,v,p) = - let pr_rel = function - | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" - in - let reason = match p with - | None | Some [] -> mt() - | Some p -> - str " because" ++ spc() ++ pr_uni v ++ - prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) - p ++ - (if Universe.equal (snd (List.last p)) u then mt() else - (spc() ++ str "= " ++ pr_uni u)) - in - str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ - pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")" +let explain_universe_inconsistency prl (o,u,v,p) = + let pr_uni = Universe.pr_with prl in + let pr_rel = function + | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" + in + let reason = match p with + | None | Some [] -> mt() + | Some p -> + str " because" ++ spc() ++ pr_uni v ++ + prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) + p ++ + (if Universe.equal (snd (List.last p)) u then mt() else + (spc() ++ str "= " ++ pr_uni u)) + in + str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ + pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")" let compare_levels = Level.compare let eq_levels = Level.equal diff --git a/kernel/univ.mli b/kernel/univ.mli index 490ec0369..7aaf2ffe6 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -49,7 +49,7 @@ module LSet : sig include CSig.SetS with type elt = universe_level - val pr : t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds (** Pretty-printing *) end @@ -292,7 +292,7 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds (** Pretty-printing, no comments *) val levels : t -> LSet.t @@ -413,14 +413,16 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons (** {6 Pretty-printing of universes. } *) -val pr_universes : universes -> Pp.std_ppcmds +val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds val pr_constraint_type : constraint_type -> Pp.std_ppcmds -val pr_constraints : constraints -> Pp.std_ppcmds -val pr_universe_context : universe_context -> Pp.std_ppcmds -val pr_universe_context_set : universe_context_set -> Pp.std_ppcmds +val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds +val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds +val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds +val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> + univ_inconsistency -> Pp.std_ppcmds + val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds val pr_universe_subst : universe_subst -> Pp.std_ppcmds -val explain_universe_inconsistency : univ_inconsistency -> Pp.std_ppcmds (** {6 Dumping to a file } *) diff --git a/library/universes.ml b/library/universes.ml index 31bbd1504..79070763e 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -22,6 +22,9 @@ let global_universes = Summary.ref ~name:"Global universe names" let global_universe_names () = !global_universes let set_global_universe_names s = global_universes := s +let pr_with_global_universes l = + try Nameops.pr_id (LMap.find l (snd !global_universes)) + with Not_found -> Level.pr l type universe_constraint_type = ULe | UEq | ULub diff --git a/library/universes.mli b/library/universes.mli index 0053d8f4f..f2f68d329 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -23,6 +23,8 @@ type universe_names = val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit +val pr_with_global_universes : Level.t -> Pp.std_ppcmds + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2df197546..046ee0dad 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -394,18 +394,13 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) -let detype_sort = function +let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - then - let _, map = Universes.global_universe_names () in - let pr_level u = - try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u - in - [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)] + then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -416,12 +411,12 @@ type binder_kind = BProd | BLambda | BLetIn let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) let set_detype_anonymous f = detype_anonymous := f -let detype_level l = - GType (Some (Pp.string_of_ppcmds (Univ.Level.pr l))) +let detype_level sigma l = + GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) -let detype_instance l = +let detype_instance sigma l = if Univ.Instance.is_empty l then None - else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l))) + else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) let rec detype flags avoid env sigma t = match kind_of_term (collapse_appl t) with @@ -439,7 +434,7 @@ let rec detype flags avoid env sigma t = | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) with Not_found -> GVar (dl, id)) - | Sort s -> GSort (dl,detype_sort s) + | Sort s -> GSort (dl,detype_sort sigma s) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> detype flags avoid env sigma c1 | Cast (c1,k,c2) -> @@ -463,7 +458,7 @@ let rec detype flags avoid env sigma t = in mkapp (detype flags avoid env sigma f) (Array.map_to_list (detype flags avoid env sigma) args) - | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u) + | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = let pb = Environ.lookup_projection p (snd env) in @@ -521,9 +516,9 @@ let rec detype flags avoid env sigma t = GEvar (dl,id, List.map (on_snd (detype flags avoid env sigma)) l) | Ind (ind_sp,u) -> - GRef (dl, IndRef ind_sp, detype_instance u) + GRef (dl, IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> - GRef (dl, ConstructRef cstr_sp, detype_instance u) + GRef (dl, ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in detype_case comp (detype flags avoid env sigma) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 725fff5b2..eb158686a 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -43,7 +43,7 @@ val detype_case : Id.t list -> inductive * case_style * bool list array * bool list -> constr option -> constr -> constr array -> glob_constr -val detype_sort : sorts -> glob_sort +val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> evar_map -> rel_context -> glob_decl list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d629fd5f5..ee72d3147 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -275,7 +275,7 @@ end (* 2nd part used to check consistency on the fly. *) type evar_universe_context = - { uctx_names : Univ.Level.t UNameMap.t; + { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; uctx_local : Univ.universe_context_set; (** The local context of variables *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) @@ -288,7 +288,7 @@ type evar_universe_context = } let empty_evar_universe_context = - { uctx_names = UNameMap.empty; + { uctx_names = UNameMap.empty, Univ.LMap.empty; uctx_local = Univ.ContextSet.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; @@ -309,8 +309,9 @@ let union_evar_universe_context ctx ctx' = else if is_empty_evar_universe_context ctx' then ctx else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let names = UNameMap.union ctx.uctx_names ctx'.uctx_names in - { uctx_names = names; + let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + { uctx_names = (names, names_rev); uctx_local = local; uctx_univ_variables = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; @@ -1004,6 +1005,9 @@ let merge_universe_subst evd subst = let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + let uctx_new_univ_variable rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in @@ -1018,7 +1022,7 @@ let uctx_new_univ_variable rigid name else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in let names = match name with - | Some n -> UNameMap.add n u uctx.uctx_names + | Some n -> add_uctx_names n u uctx.uctx_names | None -> uctx.uctx_names in {uctx' with uctx_names = names; uctx_local = ctx'; @@ -1253,11 +1257,10 @@ let nf_constraints = else nf_constraints let universe_of_name evd s = - UNameMap.find s evd.universes.uctx_names + UNameMap.find s (fst evd.universes.uctx_names) let add_universe_name evd s l = - let names = evd.universes.uctx_names in - let names' = UNameMap.add s l names in + let names' = add_uctx_names s l evd.universes.uctx_names in {evd with universes = {evd.universes with uctx_names = names'}} let universes evd = evd.universes.uctx_universes @@ -1689,11 +1692,23 @@ let evar_dependency_closure n sigma = let has_no_evar sigma = EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars +let pr_uctx_level uctx = + let map, map_rev = uctx.uctx_names in + fun l -> + try str(Univ.LMap.find l map_rev) + with Not_found -> + Universes.pr_with_global_universes l + +let pr_evd_level evd = pr_uctx_level evd.universes + let pr_evar_universe_context ctx = + let prl = pr_uctx_level ctx in if is_empty_evar_universe_context ctx then mt () else - (str"UNIVERSES:"++brk(0,1)++ h 0 (Univ.pr_universe_context_set ctx.uctx_local) ++ fnl () ++ - str"ALGEBRAIC UNIVERSES:"++brk(0,1)++h 0 (Univ.LSet.pr ctx.uctx_univ_algebraic) ++ fnl() ++ + (str"UNIVERSES:"++brk(0,1)++ + h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++ + str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ + h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 82daa7da3..53f8b0db8 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -598,6 +598,7 @@ val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> evar_map -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds +val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds (** {5 Deprecated functions} *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b8e3b3b14..a23963abc 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -306,7 +306,8 @@ struct match c with | Cst_const (c, u) -> if Univ.Instance.is_empty u then Constant.print c - else str"(" ++ Constant.print c ++ str ", " ++ Univ.Instance.pr u ++ str")" + else str"(" ++ Constant.print c ++ str ", " ++ + Univ.Instance.pr Univ.Level.pr u ++ str")" | Cst_proj p -> str".(" ++ Constant.print (Projection.constant p) ++ str")" diff --git a/pretyping/termops.ml b/pretyping/termops.ml index eee94f228..5862a8525 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -46,7 +46,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = let pr_puniverses p u = if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr u ++ str"*)" + else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" let rec pr_constr c = match kind_of_term c with | Rel n -> str "#"++int n diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7cc193a8d..f8264e5af 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1451,7 +1451,7 @@ let () = (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort pr_sort; + pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr diff --git a/printing/printer.ml b/printing/printer.ml index 7d5b71f34..3403fb9c3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -143,17 +143,12 @@ let pr_constr_pattern t = let (sigma, env) = get_current_context () in pr_constr_pattern_env env sigma t -let pr_sort s = pr_glob_sort (extern_sort s) +let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" -let pr_univ_cstr (c:Univ.constraints) = - if !Detyping.print_universes && not (Univ.Constraint.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_constraints c)) c - else - mt() (** Term printers resilient to [Nametab] errors *) @@ -216,7 +211,8 @@ let safe_pr_constr t = let pr_universe_ctx c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_universe_context c)) c + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context Universes.pr_with_global_universes c)) c else mt() @@ -229,7 +225,7 @@ let pr_global = pr_global_env Id.Set.empty let pr_puniverses f env (c,u) = f env c ++ (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr u ++ str"*)" + str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) diff --git a/printing/printer.mli b/printing/printer.mli index 75ab1722d..6b9c70815 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -79,12 +79,11 @@ val pr_constr_pattern : constr_pattern -> std_ppcmds val pr_cases_pattern : cases_pattern -> std_ppcmds -val pr_sort : sorts -> std_ppcmds +val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_univ_cstr : Univ.constraints -> std_ppcmds val pr_universe_ctx : Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5becb1ed3..5502356fb 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -478,7 +478,7 @@ let wrap_inv_error id = function (e, info) -> match e with Proofview.tclENV >>= fun env -> tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort k ++ + pr_sort Evd.empty k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v index 43acb7bb4..29ee14873 100644 --- a/test-suite/bugs/closed/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -25,7 +25,7 @@ Proof. refine (isequiv_adjointify (functor_forall f g) (functor_forall (f^-1) (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y - )) _ _); + )) _ _); intros h. - abstract ( apply path_forall; intros b; unfold functor_forall; diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index f0f366c48..22ea09c53 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -62,7 +62,8 @@ let process_vernac_interp_error exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then - str "." ++ spc() ++ Univ.explain_universe_inconsistency i + str "." ++ spc() ++ + Univ.explain_universe_inconsistency Universes.pr_with_global_universes i else mt() in wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f660f50d2..9341f2f70 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -180,7 +180,7 @@ let rec pr_disjunction pr = function let pr_puniverses f env (c,u) = f env c ++ (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr u ++ str"*)" + str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" else mt()) let explain_elim_arity env sigma ind sorts c pj okinds = @@ -301,7 +301,7 @@ let rec explain_unification_error env sigma p1 p2 = function | UnifUnivInconsistency p -> if !Constrextern.print_universes then [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency p] + Univ.explain_universe_inconsistency Universes.pr_with_global_universes p] else [str "universe inconsistency"] | CannotSolveConstraint ((pb,env,t,u),e) -> @@ -659,8 +659,9 @@ let explain_non_linear_unification env sigma m t = strbrk " which would require to abstract twice on " ++ pr_lconstr_env env sigma t ++ str "." -let explain_unsatisfied_constraints env cst = - strbrk "Unsatisfied constraints: " ++ Univ.pr_constraints cst ++ +let explain_unsatisfied_constraints env sigma cst = + strbrk "Unsatisfied constraints: " ++ + Univ.pr_constraints (Evd.pr_evd_level sigma) cst ++ spc () ++ str "(maybe a bugged tactic)." let explain_type_error env sigma err = @@ -699,7 +700,7 @@ let explain_type_error env sigma err = | WrongCaseInfo (ind,ci) -> explain_wrong_case_info env ind ci | UnsatisfiedConstraints cst -> - explain_unsatisfied_constraints env cst + explain_unsatisfied_constraints env sigma cst let pr_position (cl,pos) = let clpos = match cl with @@ -860,7 +861,7 @@ let explain_not_match_error = function str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency incon + Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon | IncompatiblePolymorphism (env, t1, t2) -> str "conversion of polymorphic values generates additional constraints: " ++ quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++ @@ -868,7 +869,7 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env Evd.empty t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - quote (Univ.pr_constraints cst) + quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = str "Signature components for label " ++ str (Label.to_string l) ++ @@ -1112,7 +1113,7 @@ let error_large_non_prop_inductive_not_in_type () = let error_not_allowed_case_analysis isrec kind i = str (if isrec then "Induction" else "Case analysis") ++ - strbrk " on sort " ++ pr_sort kind ++ + strbrk " on sort " ++ pr_sort Evd.empty kind ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) (fst i) ++ str "." diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2a2a82770..fb12edfbc 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -78,7 +78,7 @@ let show_universes () = let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universes cstrs) + msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -1604,7 +1604,7 @@ let vernac_print = function | PrintUniverses (b, None) -> let univ = Global.universes () in let univ = if b then Univ.sort_universes univ else univ in - msg_notice (Univ.pr_universes univ) + msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) |