aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml13
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrextern.mli2
-rw-r--r--kernel/univ.ml69
-rw-r--r--kernel/univ.mli16
-rw-r--r--library/universes.ml3
-rw-r--r--library/universes.mli2
-rw-r--r--pretyping/detyping.ml25
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--pretyping/evd.ml35
-rw-r--r--pretyping/evd.mli1
-rw-r--r--pretyping/reductionops.ml3
-rw-r--r--pretyping/termops.ml2
-rw-r--r--printing/pptactic.ml2
-rw-r--r--printing/printer.ml12
-rw-r--r--printing/printer.mli3
-rw-r--r--tactics/inv.ml2
-rw-r--r--test-suite/bugs/closed/3392.v2
-rw-r--r--toplevel/cerrors.ml3
-rw-r--r--toplevel/himsg.ml17
-rw-r--r--toplevel/vernacentries.ml4
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 ())
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 22:33:55 +0000