aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.ml4
-rw-r--r--pretyping/classops.mli7
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/detyping.mli6
-rw-r--r--pretyping/evardefine.mli2
-rw-r--r--pretyping/evarsolve.ml6
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/reductionops.mli10
-rw-r--r--pretyping/retyping.ml7
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/typing.ml8
12 files changed, 20 insertions, 40 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 078990a8c1..1cc072a2a2 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -89,7 +89,7 @@ sig
type t
val compare : t -> t -> int
val equal : t -> t -> bool
- val print : t -> std_ppcmds
+ val print : t -> Pp.t
end
type 'a t
val empty : 'a t
@@ -324,7 +324,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
(* rajouter une coercion dans le graphe *)
let path_printer = ref (fun _ -> str "<a class path>"
- : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds)
+ : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t)
let install_path_printer f = path_printer := f
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 2e5ce30f35..8707078b58 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -95,15 +95,14 @@ val lookup_pattern_path_between :
(**/**)
(* Crade *)
-open Pp
val install_path_printer :
- ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
+ ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
(**/**)
(** {6 This is for printing purpose } *)
val string_of_class : cl_typ -> string
-val pr_class : cl_typ -> std_ppcmds
-val pr_cl_index : cl_index -> std_ppcmds
+val pr_class : cl_typ -> Pp.t
+val pr_cl_index : cl_index -> Pp.t
val get_coercion_value : coe_index -> Constr.t
val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f830d4be3f..cac4111836 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -81,7 +81,7 @@ let encode_tuple r =
module PrintingInductiveMake =
functor (Test : sig
val encode : reference -> inductive
- val member_message : std_ppcmds -> bool -> std_ppcmds
+ val member_message : Pp.t -> bool -> Pp.t
val field : string
val title : string
end) ->
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index ffd67299d5..59f3f967d3 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -66,7 +66,7 @@ val subst_genarg_hook :
module PrintingInductiveMake :
functor (Test : sig
val encode : Libnames.reference -> Names.inductive
- val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds
+ val member_message : Pp.t -> bool -> Pp.t
val field : string
val title : string
end) ->
@@ -75,9 +75,9 @@ module PrintingInductiveMake :
val compare : t -> t -> int
val encode : Libnames.reference -> Names.inductive
val subst : substitution -> t -> t
- val printer : t -> Pp.std_ppcmds
+ val printer : t -> Pp.t
val key : Goptions.option_name
val title : string
- val member_message : t -> bool -> Pp.std_ppcmds
+ val member_message : t -> bool -> Pp.t
val synchronous : bool
end
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index c727332c79..5477c5c99d 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -43,5 +43,5 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
(** {6 debug pretty-printer:} *)
-val pr_tycon : env -> evar_map -> type_constraint -> Pp.std_ppcmds
+val pr_tycon : env -> evar_map -> type_constraint -> Pp.t
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f48297613..ef0fb8ea6e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -34,12 +34,6 @@ let get_polymorphic_positions sigma f =
(match oib.mind_arity with
| RegularArity _ -> assert false
| TemplateArity templ -> templ.template_param_levels)
- | Const (cst, u) ->
- let cb = Global.lookup_constant cst in
- (match cb.const_type with
- | RegularArity _ -> assert false
- | TemplateArity (_, templ) ->
- templ.template_param_levels)
| _ -> assert false
let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index de09edcdcb..5480b14af0 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -67,7 +67,7 @@ type obj_typ = {
(** Return the form of the component of a canonical structure *)
val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
-val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
+val pr_cs_pattern : cs_pattern -> Pp.t
val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
val declare_canonical_structure : global_reference -> unit
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1d75fecb15..3563235434 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -272,7 +272,7 @@ module Stack :
sig
open EConstr
type 'a app_node
- val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+ val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
type cst_member =
| Cst_const of pconstant
@@ -290,7 +290,7 @@ sig
exception IncompatibleFold2
- val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+ val pr : ('a -> Pp.t) -> 'a t -> Pp.t
val empty : 'a t
val is_empty : 'a t -> bool
val append_app : 'a array -> 'a t -> 'a t
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index db407b6c9b..1828196fe4 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -26,7 +26,7 @@ module ReductionBehaviour : sig
bool -> Globnames.global_reference -> (int list * int * flag list) -> unit
val get :
Globnames.global_reference -> (int list * int * flag list) option
- val print : Globnames.global_reference -> Pp.std_ppcmds
+ val print : Globnames.global_reference -> Pp.t
end
(** Option telling if reduction should use the refolding machinery of cbn
@@ -63,13 +63,13 @@ module Cst_stack : sig
val best_cst : t -> (constr * constr list) option
val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
val reference : Evd.evar_map -> t -> Constant.t option
- val pr : t -> Pp.std_ppcmds
+ val pr : t -> Pp.t
end
module Stack : sig
type 'a app_node
- val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+ val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
type cst_member =
| Cst_const of pconstant
@@ -86,7 +86,7 @@ module Stack : sig
| Update of 'a
and 'a t = 'a member list
- val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+ val pr : ('a -> Pp.t) -> 'a t -> Pp.t
val empty : 'a t
val is_empty : 'a t -> bool
@@ -145,7 +145,7 @@ type contextual_state_reduction_function =
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
-val pr_state : state -> Pp.std_ppcmds
+val pr_state : state -> Pp.t
(** {6 Reduction Function Operators } *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e0f9bfcb72..079524f344 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -192,11 +192,6 @@ let retype ?(polyprop=true) sigma =
EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
~polyprop env (mip, u) argtyps
with Reduction.NotArity -> retype_error NotAnArity)
- | Const (cst, u) ->
- let u = EInstance.kind sigma u in
- EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps
- with Reduction.NotArity -> retype_error NotAnArity)
- | Var id -> type_of_var env id
| Construct (cstr, u) ->
let u = EInstance.kind sigma u in
EConstr.of_constr (type_of_constructor env (cstr, u))
@@ -220,7 +215,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
| Const (cst, u) ->
let t = constant_type_in env (cst, EInstance.kind sigma u) in
(* TODO *)
- sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||])
+ sigma, EConstr.of_constr t
| Var id -> sigma, type_of_var env id
| Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
| _ -> assert false
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 163d3975af..ed3a9d0f96 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -48,4 +48,4 @@ val sorts_of_context : env -> evar_map -> rel_context -> sorts list
val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
-val print_retype_error : retype_error -> Pp.std_ppcmds
+val print_retype_error : retype_error -> Pp.t
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1bb0035751..1f35fa19aa 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,11 +35,6 @@ let meta_type evd mv =
let ty = Evd.map_fl EConstr.of_constr ty in
meta_instance evd ty
-let constant_type_knowing_parameters env sigma (cst, u) jl =
- let u = Unsafe.to_instance u in
- let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
- EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp)
-
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
@@ -315,9 +310,6 @@ let rec execute env evdref cstr =
| Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
make_judge f
(inductive_type_knowing_parameters env !evdref (ind, u) jl)
- | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env ->
- make_judge f
- (constant_type_knowing_parameters env !evdref (cst, u) jl)
| _ ->
(* No template polymorphism *)
execute env evdref f
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 19:31:15 +0000