aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/miscprint.mli20
-rw-r--r--proofs/pfedit.ml5
-rw-r--r--proofs/proof.mli2
-rw-r--r--proofs/proof_bullet.mli2
-rw-r--r--proofs/proof_global.ml6
-rw-r--r--proofs/refine.mli2
-rw-r--r--proofs/refiner.ml2
-rw-r--r--proofs/refiner.mli8
-rw-r--r--proofs/tacmach.mli4
11 files changed, 29 insertions, 26 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 26c6e60141..9c69995f4b 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -112,7 +112,7 @@ exception NotExtensibleClause
val clenv_push_prod : clausenv -> clausenv
(** {6 Pretty-print (debug only) } *)
-val pr_clenv : clausenv -> Pp.std_ppcmds
+val pr_clenv : clausenv -> Pp.t
(** {6 Evar-based clauses} *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index cd71d11f86..6d3ec8bd4e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -20,7 +20,7 @@ val uid : goal -> string
val get_by_uid : string -> goal
(* Debugging help *)
-val pr_goal : goal -> Pp.std_ppcmds
+val pr_goal : goal -> Pp.t
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 21d410c7b0..b75718cd01 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -11,27 +11,27 @@ open Misctypes
(** Printing of [intro_pattern] *)
val pr_intro_pattern :
- ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds
+ ('a -> Pp.t) -> 'a intro_pattern_expr Loc.located -> Pp.t
val pr_or_and_intro_pattern :
- ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds
+ ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
+val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t
(** Printing of [move_location] *)
val pr_move_location :
- ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+ ('a -> Pp.t) -> 'a move_location -> Pp.t
val pr_bindings :
- ('a -> Pp.std_ppcmds) ->
- ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+ ('a -> Pp.t) ->
+ ('a -> Pp.t) -> 'a bindings -> Pp.t
val pr_bindings_no_with :
- ('a -> Pp.std_ppcmds) ->
- ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+ ('a -> Pp.t) ->
+ ('a -> Pp.t) -> 'a bindings -> Pp.t
val pr_with_bindings :
- ('a -> Pp.std_ppcmds) ->
- ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
+ ('a -> Pp.t) ->
+ ('a -> Pp.t) -> 'a * 'a bindings -> Pp.t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a949c8e911..1937885587 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
else { ce with
const_entry_body = Future.chain ~pure:true ce.const_entry_body
- (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
- let (cb, ctx), se = Future.force ce.const_entry_body in
+ (fun (pt, _) -> pt, ()) } in
+ let (cb, ctx), () = Future.force ce.const_entry_body in
let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
- assert(Safe_typing.empty_private_constants = se);
cb, status, Evd.evar_universe_context univs'
let refine_by_tactic env sigma ty tac =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1865382e41..698aa48b02 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -182,7 +182,7 @@ val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
focused goals. *)
val unshelve : proof -> proof
-val pr_proof : proof -> Pp.std_ppcmds
+val pr_proof : proof -> Pp.t
(*** Compatibility layer with <=v8.2 ***)
module V82 : sig
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 9ae521d3f0..9e924fec97 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -48,6 +48,6 @@ val suggest : proof -> Pp.t
(* *)
(**********************************************************)
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
val get_default_goal_selector : unit -> Vernacexpr.goal_selector
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 52d6787d44..2ade797f63 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let t = EConstr.Unsafe.to_constr t in
let univstyp, body = make_body t p in
let univs, typ = Future.force univstyp in
+ let univs =
+ if poly then Entries.Polymorphic_const_entry univs
+ else Entries.Monomorphic_const_entry univs
+ in
{ Entries.
const_entry_body = body;
const_entry_secctx = section_vars;
@@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
const_entry_inline_code = false;
const_entry_opaque = true;
const_entry_universes = univs;
- const_entry_polymorphic = poly})
+ })
fpl initial_goals in
let binders =
Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 20f5a07912..3b0a9e5b6f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,7 +17,7 @@ open Proofview
(** Printer used to print the constr which refine refines. *)
val pr_constr :
- (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+ (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t
(** {7 Refinement primitives} *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index f1b1cd359f..3e3313eb57 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -63,7 +63,7 @@ let tclIDTAC_MESSAGE s gls =
let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
(* A special exception for levels for the Fail tactic *)
-exception FailError of int * std_ppcmds Lazy.t
+exception FailError of int * Pp.t Lazy.t
(* The Fail tactic *)
let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index aac10e81b7..3ff010fe3e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -31,7 +31,7 @@ val refiner : rule -> tactic
(** [tclIDTAC] is the identity tactic without message printing*)
val tclIDTAC : tactic
-val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic
+val tclIDTAC_MESSAGE : Pp.t -> tactic
(** [tclEVARS sigma] changes the current evar map *)
val tclEVARS : evar_map -> tactic
@@ -100,7 +100,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENFIRSTn : tactic -> tactic array -> tactic
(** A special exception for levels for the Fail tactic *)
-exception FailError of int * Pp.std_ppcmds Lazy.t
+exception FailError of int * Pp.t Lazy.t
(** Takes an exception and either raise it at the next
level or do nothing. *)
@@ -116,8 +116,8 @@ val tclTRY : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL : int -> Pp.std_ppcmds -> tactic
-val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic
+val tclFAIL : int -> Pp.t -> tactic
+val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 2b7c365943..40b6573a15 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -94,8 +94,8 @@ val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
(** {6 Pretty-printing functions (debug only). } *)
-val pr_gls : goal sigma -> Pp.std_ppcmds
-val pr_glls : goal list sigma -> Pp.std_ppcmds
+val pr_gls : goal sigma -> Pp.t
+val pr_glls : goal list sigma -> Pp.t
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:10:55 +0000