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.ml15
-rw-r--r--pretyping/detyping.mli6
-rw-r--r--pretyping/evardefine.mli2
-rw-r--r--pretyping/pretyping.ml9
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/reductionops.mli10
-rw-r--r--pretyping/retyping.mli2
10 files changed, 37 insertions, 24 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..a27debe735 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) ->
@@ -475,8 +475,8 @@ let rec detype flags avoid env sigma t = CAst.make @@
GApp (f',args''@args')
| _ -> GApp (f',args')
in
- mkapp (detype flags avoid env sigma f)
- (Array.map_to_list (detype flags avoid env sigma) args)
+ mkapp (detype flags avoid env sigma f)
+ (detype_array flags avoid env sigma args)
| Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
| Proj (p,c) ->
let noparams () =
@@ -694,6 +694,15 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in
GLetIn (na', c, t, r)
+(** We use a dedicated function here to prevent overallocation from
+ Array.map_to_list. *)
+and detype_array flags avoid env sigma args =
+ let ans = ref [] in
+ for i = Array.length args - 1 downto 0 do
+ ans := detype flags avoid env sigma args.(i) :: !ans;
+ done;
+ !ans
+
let detype_rel_context ?(lax=false) where avoid env sigma sign =
let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
let rec aux avoid env = function
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/pretyping.ml b/pretyping/pretyping.ml
index bfc6bf5cff..b4d87dfdb0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1136,8 +1136,13 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
| _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
in
- { utj_val = v;
- utj_type = s }
+ (* Correction of bug #5315 : we need to define an evar for *all* holes *)
+ let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
+ let ev,_ = destEvar !evdref evkt in
+ evdref := Evd.define ev (to_constr !evdref v) !evdref;
+ (* End of correction of bug #5315 *)
+ { utj_val = v;
+ utj_type = s }
| None ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
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.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:45:47 +0000