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. --- kernel/cClosure.ml | 6 +++--- kernel/cClosure.mli | 12 ++++++------ kernel/conv_oracle.mli | 2 +- kernel/kernel.mllib | 1 + kernel/names.ml | 7 ------- kernel/names.mli | 8 -------- kernel/reduction.ml | 8 ++++---- kernel/reduction.mli | 8 ++++---- kernel/transpState.ml | 18 ++++++++++++++++++ kernel/transpState.mli | 26 ++++++++++++++++++++++++++ kernel/vconv.ml | 4 ++-- 11 files changed, 65 insertions(+), 35 deletions(-) create mode 100644 kernel/transpState.ml create mode 100644 kernel/transpState.mli (limited to 'kernel') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95546a83e1..c8028f713a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -93,8 +93,8 @@ module type RedFlagsSig = sig val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> transparent_state -> reds - val red_transparent : reds -> transparent_state + val red_add_transparent : reds -> TranspState.t -> reds + val red_transparent : reds -> TranspState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool @@ -110,7 +110,7 @@ module RedFlags = (struct r_beta : bool; r_delta : bool; r_eta : bool; - r_const : transparent_state; + r_const : TranspState.t; r_zeta : bool; r_match : bool; r_fix : bool; diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1ee4bccc25..9d41ee0695 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -26,11 +26,11 @@ val with_stats: 'a Lazy.t -> 'a -val all_opaque : transparent_state -val all_transparent : transparent_state +val all_opaque : TranspState.t +val all_transparent : TranspState.t -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> Constant.t -> bool +val is_transparent_variable : TranspState.t -> variable -> bool +val is_transparent_constant : TranspState.t -> Constant.t -> bool (** Sets of reduction kinds. *) module type RedFlagsSig = sig @@ -60,10 +60,10 @@ module type RedFlagsSig = sig val red_sub : reds -> red_kind -> reds (** Adds a reduction kind to a set *) - val red_add_transparent : reds -> transparent_state -> reds + val red_add_transparent : reds -> TranspState.t -> reds (** Retrieve the transparent state of the reduction flags *) - val red_transparent : reds -> transparent_state + val red_transparent : reds -> TranspState.t (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 67add5dd35..3b51515352 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle (** Fold over the non-transparent levels of the oracle. Order unspecified. *) val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a -val get_transp_state : oracle -> transparent_state +val get_transp_state : oracle -> TranspState.t diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index a18c5d1e20..e716972ebe 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,4 +1,5 @@ Names +TranspState Uint31 Univ UGraph diff --git a/kernel/names.ml b/kernel/names.ml index 18560d5f8d..b2d6a489a6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -715,13 +715,6 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons (*****************) -type transparent_state = Id.Pred.t * Cpred.t - -let empty_transparent_state = (Id.Pred.empty, Cpred.empty) -let full_transparent_state = (Id.Pred.full, Cpred.full) -let var_full_transparent_state = (Id.Pred.full, Cpred.empty) -let cst_full_transparent_state = (Id.Pred.empty, Cpred.full) - type 'a tableKey = | ConstKey of 'a | VarKey of Id.t diff --git a/kernel/names.mli b/kernel/names.mli index 98995752a2..350db871d5 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -510,14 +510,6 @@ type 'a tableKey = | VarKey of Id.t | RelKey of Int.t -(** Sets of names *) -type transparent_state = Id.Pred.t * Cpred.t - -val empty_transparent_state : transparent_state -val full_transparent_state : transparent_state -val var_full_transparent_state : transparent_state -val cst_full_transparent_state : transparent_state - type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5515ff9767..a45a5b3247 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = - ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?l2r:bool -> ?reds:TranspState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = +let gen_conv cv_pb ?(l2r=false) ?(reds=TranspState.full) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in @@ -792,11 +792,11 @@ let infer_conv_universes = CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes -let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) +let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) env univs t1 t2 = infer_conv_universes CONV l2r evars ts env univs t1 t2 -let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) +let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 581e8bd88a..9b26e7b3dc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertibleVect of int type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = - ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?l2r:bool -> ?reds:TranspState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:Names.transparent_state -> constr infer_conversion_function + ?ts:TranspState.t -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:Names.transparent_state -> types infer_conversion_function + ?ts:TranspState.t -> types infer_conversion_function (** Depending on the universe state functions, this might raise [UniverseInconsistency] in addition to [NotConvertible] (for better error messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> - Names.transparent_state -> (constr,'a) generic_conversion_function + TranspState.t -> (constr,'a) generic_conversion_function val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function diff --git a/kernel/transpState.ml b/kernel/transpState.ml new file mode 100644 index 0000000000..9acb7244f7 --- /dev/null +++ b/kernel/transpState.ml @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* None) - full_transparent_state env univs t1 t2 + TranspState.full env univs t1 t2 else try let v1 = val_of_constr env t1 in @@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 = with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2 + TranspState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in -- 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. --- kernel/cClosure.ml | 31 ++++++++++++++----------------- kernel/cClosure.mli | 8 -------- kernel/conv_oracle.ml | 3 ++- kernel/transpState.ml | 37 ++++++++++++++++++++++++++++++++----- kernel/transpState.mli | 10 +++++++++- 5 files changed, 57 insertions(+), 32 deletions(-) (limited to 'kernel') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c8028f713a..625a9a7277 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -72,11 +72,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = (Id.Pred.empty, Cpred.empty) -let all_transparent = (Id.Pred.full, Cpred.full) - -let is_transparent_variable (ids, _) id = Id.Pred.mem id ids -let is_transparent_constant (_, csts) cst = Cpred.mem cst csts +let all_opaque = TranspState.empty +let all_transparent = TranspState.full module type RedFlagsSig = sig type reds @@ -106,6 +103,8 @@ module RedFlags = (struct (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) + open TranspState + type reds = { r_beta : bool; r_delta : bool; @@ -143,30 +142,30 @@ module RedFlags = (struct | ETA -> { red with r_eta = true } | DELTA -> { red with r_delta = true; r_const = all_transparent } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.add kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } } | MATCH -> { red with r_match = true } | FIX -> { red with r_fix = true } | COFIX -> { red with r_cofix = true } | ZETA -> { red with r_zeta = true } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.add id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } } let red_sub red = function | BETA -> { red with r_beta = false } | ETA -> { red with r_eta = false } | DELTA -> { red with r_delta = false } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.remove kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } } | MATCH -> { red with r_match = false } | FIX -> { red with r_fix = false } | COFIX -> { red with r_cofix = false } | ZETA -> { red with r_zeta = false } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.remove id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } } let red_transparent red = red.r_const @@ -179,12 +178,10 @@ module RedFlags = (struct | BETA -> incr_cnt red.r_beta beta | ETA -> incr_cnt red.r_eta eta | CONST kn -> - let (_,l) = red.r_const in - let c = Cpred.mem kn l in + let c = is_transparent_constant red.r_const kn in incr_cnt c delta | VAR id -> (* En attendant d'avoir des kn pour les Var *) - let (l,_) = red.r_const in - let c = Id.Pred.mem id l in + let c = is_transparent_variable red.r_const id in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | MATCH -> incr_cnt red.r_match nb_match diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 9d41ee0695..26710a64d0 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) - - -val all_opaque : TranspState.t -val all_transparent : TranspState.t - -val is_transparent_variable : TranspState.t -> variable -> bool -val is_transparent_constant : TranspState.t -> Constant.t -> bool - (** Sets of reduction kinds. *) module type RedFlagsSig = sig type reds diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index ac78064235..c66beb49b8 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -81,7 +81,8 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu = let accu = Id.Map.fold fvar var_opacity accu in Cmap.fold fcst cst_opacity accu -let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) +let get_transp_state { var_trstate; cst_trstate; _ } = + { TranspState.tr_var = var_trstate; tr_cst = cst_trstate } let dep_order l2r k1 k2 = match k1, k2 with | RelKey _, RelKey _ -> l2r diff --git a/kernel/transpState.ml b/kernel/transpState.ml index 9acb7244f7..9661dace6a 100644 --- a/kernel/transpState.ml +++ b/kernel/transpState.ml @@ -10,9 +10,36 @@ open Names -type t = Id.Pred.t * Cpred.t +type t = { + tr_var : Id.Pred.t; + tr_cst : Cpred.t; +} -let empty = (Id.Pred.empty, Cpred.empty) -let full = (Id.Pred.full, Cpred.full) -let var_full = (Id.Pred.full, Cpred.empty) -let cst_full = (Id.Pred.empty, Cpred.full) +let empty = { + tr_var = Id.Pred.empty; + tr_cst = Cpred.empty; +} + +let full = { + tr_var = Id.Pred.full; + tr_cst = Cpred.full; +} + +let var_full = { + tr_var = Id.Pred.full; + tr_cst = Cpred.empty; +} + +let cst_full = { + tr_var = Id.Pred.empty; + tr_cst = Cpred.full; +} + +let is_empty ts = + Id.Pred.is_empty ts.tr_var && Cpred.is_empty ts.tr_cst + +let is_transparent_variable ts id = + Id.Pred.mem id ts.tr_var + +let is_transparent_constant ts cst = + Cpred.mem cst ts.tr_cst diff --git a/kernel/transpState.mli b/kernel/transpState.mli index a8d301549b..f2999c6869 100644 --- a/kernel/transpState.mli +++ b/kernel/transpState.mli @@ -11,7 +11,10 @@ open Names (** Sets of names *) -type t = Id.Pred.t * Cpred.t +type t = { + tr_var : Id.Pred.t; + tr_cst : Cpred.t; +} val empty : t (** Everything opaque *) @@ -24,3 +27,8 @@ val var_full : t val cst_full : t (** All constant transparent *) + +val is_empty : t -> bool + +val is_transparent_variable : t -> Id.t -> bool +val is_transparent_constant : t -> Constant.t -> bool -- 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. --- kernel/cClosure.ml | 12 ++++++------ kernel/cClosure.mli | 4 ++-- kernel/conv_oracle.ml | 2 +- kernel/conv_oracle.mli | 2 +- kernel/kernel.mllib | 2 +- kernel/reduction.ml | 8 ++++---- kernel/reduction.mli | 8 ++++---- kernel/transpState.ml | 45 --------------------------------------------- kernel/transpState.mli | 34 ---------------------------------- kernel/transparentState.ml | 45 +++++++++++++++++++++++++++++++++++++++++++++ kernel/transparentState.mli | 34 ++++++++++++++++++++++++++++++++++ kernel/vconv.ml | 4 ++-- 12 files changed, 100 insertions(+), 100 deletions(-) delete mode 100644 kernel/transpState.ml delete mode 100644 kernel/transpState.mli create mode 100644 kernel/transparentState.ml create mode 100644 kernel/transparentState.mli (limited to 'kernel') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 625a9a7277..7e73609996 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -72,8 +72,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = TranspState.empty -let all_transparent = TranspState.full +let all_opaque = TransparentState.empty +let all_transparent = TransparentState.full module type RedFlagsSig = sig type reds @@ -90,8 +90,8 @@ module type RedFlagsSig = sig val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> TranspState.t -> reds - val red_transparent : reds -> TranspState.t + val red_add_transparent : reds -> TransparentState.t -> reds + val red_transparent : reds -> TransparentState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool @@ -103,13 +103,13 @@ module RedFlags = (struct (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) - open TranspState + open TransparentState type reds = { r_beta : bool; r_delta : bool; r_eta : bool; - r_const : TranspState.t; + r_const : TransparentState.t; r_zeta : bool; r_match : bool; r_fix : bool; diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 26710a64d0..b6c87b3732 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -52,10 +52,10 @@ module type RedFlagsSig = sig val red_sub : reds -> red_kind -> reds (** Adds a reduction kind to a set *) - val red_add_transparent : reds -> TranspState.t -> reds + val red_add_transparent : reds -> TransparentState.t -> reds (** Retrieve the transparent state of the reduction flags *) - val red_transparent : reds -> TranspState.t + val red_transparent : reds -> TransparentState.t (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index c66beb49b8..fe82353b70 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -82,7 +82,7 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu = Cmap.fold fcst cst_opacity accu let get_transp_state { var_trstate; cst_trstate; _ } = - { TranspState.tr_var = var_trstate; tr_cst = cst_trstate } + { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate } let dep_order l2r k1 k2 = match k1, k2 with | RelKey _, RelKey _ -> l2r diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 3b51515352..bc06cc21b6 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle (** Fold over the non-transparent levels of the oracle. Order unspecified. *) val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a -val get_transp_state : oracle -> TranspState.t +val get_transp_state : oracle -> TransparentState.t diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index e716972ebe..54c239349d 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,5 +1,5 @@ Names -TranspState +TransparentState Uint31 Univ UGraph diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a45a5b3247..fbb481424f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = - ?l2r:bool -> ?reds:TranspState.t -> env -> + ?l2r:bool -> ?reds:TransparentState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=TranspState.full) env ?(evars=(fun _->None), universes env) = +let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in @@ -792,11 +792,11 @@ let infer_conv_universes = CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes -let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) +let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env univs t1 t2 = infer_conv_universes CONV l2r evars ts env univs t1 t2 -let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) +let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9b26e7b3dc..0408dbf057 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertibleVect of int type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = - ?l2r:bool -> ?reds:TranspState.t -> env -> + ?l2r:bool -> ?reds:TransparentState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:TranspState.t -> constr infer_conversion_function + ?ts:TransparentState.t -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:TranspState.t -> types infer_conversion_function + ?ts:TransparentState.t -> types infer_conversion_function (** Depending on the universe state functions, this might raise [UniverseInconsistency] in addition to [NotConvertible] (for better error messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> - TranspState.t -> (constr,'a) generic_conversion_function + TransparentState.t -> (constr,'a) generic_conversion_function val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function diff --git a/kernel/transpState.ml b/kernel/transpState.ml deleted file mode 100644 index 9661dace6a..0000000000 --- a/kernel/transpState.ml +++ /dev/null @@ -1,45 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* bool - -val is_transparent_variable : t -> Id.t -> bool -val is_transparent_constant : t -> Constant.t -> bool diff --git a/kernel/transparentState.ml b/kernel/transparentState.ml new file mode 100644 index 0000000000..9661dace6a --- /dev/null +++ b/kernel/transparentState.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* bool + +val is_transparent_variable : t -> Id.t -> bool +val is_transparent_constant : t -> Constant.t -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 46e52121c7..246c90c09d 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed = let vm_conv_gen cv_pb env univs t1 t2 = if not (typing_flags env).Declarations.enable_VM then Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - TranspState.full env univs t1 t2 + TransparentState.full env univs t1 t2 else try let v1 = val_of_constr env t1 in @@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 = with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - TranspState.full env univs t1 t2 + TransparentState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in -- cgit v1.2.3