aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml5
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/explainErr.mli6
-rw-r--r--vernac/himsg.mli21
-rw-r--r--vernac/indschemes.ml8
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/metasyntax.mli2
-rw-r--r--vernac/mltop.mli6
-rw-r--r--vernac/obligations.ml10
-rw-r--r--vernac/obligations.mli5
-rw-r--r--vernac/record.ml7
-rw-r--r--vernac/topfmt.mli8
-rw-r--r--vernac/vernacentries.ml4
13 files changed, 43 insertions, 43 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 86bbf46a3..6711b14da 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -311,10 +311,7 @@ let traverse current t =
(** Hopefully bullet-proof function to recover the type of a constant. It just
ignores all the universe stuff. There are many issues that can arise when
considering terms out of any valid environment, so use with caution. *)
-let type_of_constant cb = match cb.Declarations.const_type with
-| Declarations.RegularArity ty -> ty
-| Declarations.TemplateArity (ctx, arity) ->
- Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
+let type_of_constant cb = cb.Declarations.const_type
let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let (idts, knst) = st in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 793a4c580..2178a7caa 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -18,7 +18,7 @@ let guill s = str "\"" ++ str s ++ str "\""
(** Invariant : exceptions embedded in EvaluatedError satisfy
Errors.noncritical *)
-exception EvaluatedError of std_ppcmds * exn option
+exception EvaluatedError of Pp.t * exn option
(** Registration of generic errors
Nota: explain_exn does NOT end with a newline anymore!
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index 944339d85..0cbd71fa4 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -7,7 +7,7 @@
(************************************************************************)
(** Toplevel Exception *)
-exception EvaluatedError of Pp.std_ppcmds * exn option
+exception EvaluatedError of Pp.t * exn option
(** Pre-explain a vernac interpretation error *)
@@ -16,6 +16,6 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
(** General explain function. Should not be used directly now,
see instead function [Errors.print] and variants *)
-val explain_exn_default : exn -> Pp.std_ppcmds
+val explain_exn_default : exn -> Pp.t
-val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit
+val register_additional_error_info : (Util.iexn -> (Pp.t option Loc.located) option) -> unit
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index b95ef8425..5b91f9e68 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Indtypes
open Environ
open Type_errors
@@ -18,28 +17,28 @@ open Logic
(** This module provides functions to explain the type errors. *)
-val explain_type_error : env -> Evd.evar_map -> type_error -> std_ppcmds
+val explain_type_error : env -> Evd.evar_map -> type_error -> Pp.t
-val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> std_ppcmds
+val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
-val explain_inductive_error : inductive_error -> std_ppcmds
+val explain_inductive_error : inductive_error -> Pp.t
-val explain_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds
+val explain_typeclass_error : env -> typeclass_error -> Pp.t
-val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
+val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
-val explain_refiner_error : refiner_error -> std_ppcmds
+val explain_refiner_error : refiner_error -> Pp.t
val explain_pattern_matching_error :
- env -> Evd.evar_map -> pattern_matching_error -> std_ppcmds
+ env -> Evd.evar_map -> pattern_matching_error -> Pp.t
val explain_reduction_tactic_error :
- Tacred.reduction_tactic_error -> std_ppcmds
+ Tacred.reduction_tactic_error -> Pp.t
-val explain_module_error : Modops.module_typing_error -> std_ppcmds
+val explain_module_error : Modops.module_typing_error -> Pp.t
val explain_module_internalization_error :
- Modintern.module_internalization_error -> std_ppcmds
+ Modintern.module_internalization_error -> Pp.t
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 3d97a767c..6ea8bc7f2 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,13 +109,17 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
+ let _, univs = Evd.universe_context ctx in
+ let univs =
+ if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
+ else Monomorphic_const_entry univs
+ in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
- const_entry_polymorphic = Flags.is_universe_polymorphism ();
- const_entry_universes = snd (Evd.universe_context ctx);
+ const_entry_universes = univs;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 41e3be1ed..c0974d0a7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1081,7 +1081,7 @@ module SynData = struct
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
- msgs : ((std_ppcmds -> unit) * std_ppcmds) list;
+ msgs : ((Pp.t -> unit) * Pp.t) list;
(* Fields for internalization *)
recvars : (Id.t * Id.t) list;
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index c9e37a4eb..9cd00cbcb 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntactic_definition : Id.t -> Id.t list * constr_expr ->
(** Print the Camlp4 state of a grammar *)
-val pr_grammar : string -> Pp.std_ppcmds
+val pr_grammar : string -> Pp.t
type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 3ecda656d..324a66d38 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -83,6 +83,6 @@ val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
(** {5 Utilities} *)
-val print_ml_path : unit -> Pp.std_ppcmds
-val print_ml_modules : unit -> Pp.std_ppcmds
-val print_gc : unit -> Pp.std_ppcmds
+val print_ml_path : unit -> Pp.t
+val print_ml_modules : unit -> Pp.t
+val print_gc : unit -> Pp.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 10d3317f8..28aeaa725 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -636,12 +636,12 @@ let declare_obligation prg obl body ty uctx =
shrink_body body ty else [], body, ty, [||]
in
let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
let ce =
{ const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
const_entry_secctx = None;
const_entry_type = ty;
- const_entry_polymorphic = poly;
- const_entry_universes = uctx;
+ const_entry_universes = univs;
const_entry_opaque = opaque;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx =
id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
- let body, eff = Future.force entry.const_entry_body in
- assert(Safe_typing.empty_private_constants = eff);
+ let body, () = Future.force entry.const_entry_body in
let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
Inductiveops.control_only_guard (Global.env ()) (fst body);
(fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
@@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf =
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let ty = entry.Entries.const_entry_type in
- let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
- assert(Safe_typing.empty_private_constants = eff);
+ let (body, cstr), () = Future.force entry.Entries.const_entry_body in
let sigma = Evd.from_ctx (fst uctx) in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
Inductiveops.control_only_guard (Global.env ()) body;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index fa691ad1b..5614403ba 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -10,7 +10,6 @@ open Environ
open Term
open Evd
open Names
-open Pp
open Globnames
(* This is a hack to make it possible for Obligations to craft a Qed
@@ -96,12 +95,12 @@ val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option ->
val show_obligations : ?msg:bool -> Names.Id.t option -> unit
-val show_term : Names.Id.t option -> std_ppcmds
+val show_term : Names.Id.t option -> Pp.t
val admit_obligations : Names.Id.t option -> unit
exception NoObligations of Names.Id.t option
-val explain_no_obligations : Names.Id.t option -> Pp.std_ppcmds
+val explain_no_obligations : Names.Id.t option -> Pp.t
val set_program_mode : bool -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index 63ca22786..a2e443e5f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -322,13 +322,16 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
+ let univs =
+ if poly then Polymorphic_const_entry ctx
+ else Monomorphic_const_entry ctx
+ in
let entry = {
const_entry_body =
Future.from_val (Safe_typing.mk_pure_proof proj);
const_entry_secctx = None;
const_entry_type = Some projtyp;
- const_entry_polymorphic = poly;
- const_entry_universes = ctx;
+ const_entry_universes = univs;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 6e006fc6c..afe76f6f8 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -37,8 +37,8 @@ val set_margin : int option -> unit
val get_margin : unit -> int option
(** Console display of feedback, we may add some location information *)
-val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
-val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
+val std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
+val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
(** Color output *)
val clear_styles : unit -> unit
@@ -51,8 +51,8 @@ val init_terminal_output : color:bool -> unit
(** Error printing *)
(* To be deprecated when we can fully move to feedback-based error
printing. *)
-val pr_loc : Loc.t -> Pp.std_ppcmds
-val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit
+val pr_loc : Loc.t -> Pp.t
+val print_err_exn : ?extra:Pp.t -> exn -> unit
(** [with_output_to_file file f x] executes [f x] with logging
redirected to a file [file] *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9650ea19d..959df89f6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -257,7 +257,7 @@ let print_namespace ns =
in
let print_constant k body =
(* FIXME: universes *)
- let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in
+ let t = body.Declarations.const_type in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
in
let matches mp = match match_modulepath ns mp with
@@ -2120,7 +2120,7 @@ let locate_if_not_already ?loc (e, info) =
| Some l -> (e, info)
exception HasNotFailed
-exception HasFailed of std_ppcmds
+exception HasFailed of Pp.t
let with_fail b f =
if not b then f ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 10:30:44 +0000