From 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 00:43:01 +0200 Subject: Move transparent_state to its own module. --- pretyping/reductionops.mli | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 41de779414..2f2728465f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -266,21 +266,21 @@ type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool +val is_conv : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool +val is_conv_leq : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool +val is_fconv : ?reds:TranspState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) -val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool +val check_conv : ?pb:conv_pb -> ?ts:TranspState.t -> env -> evar_map -> constr -> constr -> bool (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) -val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> +val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) @@ -292,9 +292,9 @@ val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a conversion function. Used to pretype vm and native casts. *) -val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> +val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> - ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> + ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> env -> evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) @@ -302,13 +302,13 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> val whd_meta : local_reduction_function val plain_instance : evar_map -> constr Metamap.t -> constr -> constr val instance : evar_map -> constr Metamap.t -> constr -> constr -val head_unfold_under_prod : transparent_state -> reduction_function +val head_unfold_under_prod : TranspState.t -> reduction_function val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) val whd_betaiota_deltazeta_for_iota_state : - transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> + TranspState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> state * Cst_stack.t (** {6 Meta-related reduction functions } *) -- cgit v1.2.3 From ad5aea737ecc639c31dda84322b3550a4d380b47 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 21:06:01 +0200 Subject: Proper record type and accessors for transparent states. This is documented in dev/doc/changes.md. --- pretyping/reductionops.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 2f2728465f..749e23bde2 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -302,7 +302,6 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t -> val whd_meta : local_reduction_function val plain_instance : evar_map -> constr Metamap.t -> constr -> constr val instance : evar_map -> constr Metamap.t -> constr -> constr -val head_unfold_under_prod : TranspState.t -> reduction_function val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) -- cgit v1.2.3 From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Nov 2018 08:12:28 +0100 Subject: Rename TranspState into TransparentState. --- pretyping/reductionops.mli | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 749e23bde2..088e898a99 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -266,21 +266,21 @@ type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool -val is_conv_leq : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool -val is_fconv : ?reds:TranspState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool +val is_conv : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool +val is_conv_leq : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool +val is_fconv : ?reds:TransparentState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) -val check_conv : ?pb:conv_pb -> ?ts:TranspState.t -> env -> evar_map -> constr -> constr -> bool +val check_conv : ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> bool (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) -val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> +val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) @@ -292,9 +292,9 @@ val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a conversion function. Used to pretype vm and native casts. *) -val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t -> +val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> - ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> env -> + ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) @@ -307,7 +307,7 @@ val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) val whd_betaiota_deltazeta_for_iota_state : - TranspState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> + TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> state * Cst_stack.t (** {6 Meta-related reduction functions } *) -- cgit v1.2.3