aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/dune7
-rw-r--r--kernel/environ.ml5
-rw-r--r--kernel/environ.mli1
-rw-r--r--kernel/float64_31.ml35
-rw-r--r--kernel/float64_63.ml35
-rw-r--r--kernel/float64_common.ml (renamed from kernel/float64.ml)24
-rw-r--r--kernel/float64_common.mli95
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--kernel/mod_typing.ml10
-rw-r--r--kernel/nativeconv.ml4
-rw-r--r--kernel/reduction.ml42
-rw-r--r--kernel/reduction.mli6
-rw-r--r--kernel/safe_typing.ml10
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/vconv.ml4
16 files changed, 216 insertions, 67 deletions
diff --git a/kernel/dune b/kernel/dune
index ce6fdc03df..bd663974da 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,7 +3,7 @@
(synopsis "The Coq Kernel")
(public_name coq.kernel)
(wrapped false)
- (modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
+ (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
(libraries lib byterun dynlink))
(executable
@@ -19,6 +19,11 @@
(deps (:gen-file uint63_%{ocaml-config:int_size}.ml))
(action (copy# %{gen-file} %{targets})))
+(rule
+ (targets float64.ml)
+ (deps (:gen-file float64_%{ocaml-config:int_size}.ml))
+ (action (copy# %{gen-file} %{targets})))
+
(documentation
(package coq))
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e497b7904a..dec9e1deb8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -274,6 +274,11 @@ let is_impredicative_sort env = function
let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
+let is_impredicative_family env = function
+ | Sorts.InSProp | Sorts.InProp -> true
+ | Sorts.InSet -> is_impredicative_set env
+ | Sorts.InType -> false
+
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 47a118aa42..f443ba38e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -122,6 +122,7 @@ val indices_matter : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
+val is_impredicative_family : env -> Sorts.family -> bool
(** is the local context empty *)
val empty_context : env -> bool
diff --git a/kernel/float64_31.ml b/kernel/float64_31.ml
new file mode 100644
index 0000000000..09b28e6cf0
--- /dev/null
+++ b/kernel/float64_31.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+include Float64_common
+
+external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul"
+[@@unboxed] [@@noalloc]
+
+external add : float -> float -> float = "coq_fadd_byte" "coq_fadd"
+[@@unboxed] [@@noalloc]
+
+external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub"
+[@@unboxed] [@@noalloc]
+
+external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv"
+[@@unboxed] [@@noalloc]
+
+external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt"
+[@@unboxed] [@@noalloc]
+
+(*** Test at runtime that no harmful double rounding seems to
+ be performed with an intermediate 80 bits representation (x87). *)
+let () =
+ let b = ldexp 1. 53 in
+ let s = add 1. (ldexp 1. (-52)) in
+ if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
+ failwith "Detected non IEEE-754 compliant architecture (or wrong \
+ rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64_63.ml b/kernel/float64_63.ml
new file mode 100644
index 0000000000..0025531cb1
--- /dev/null
+++ b/kernel/float64_63.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+include Float64_common
+
+let mul (x : float) (y : float) : float = x *. y
+[@@ocaml.inline always]
+
+let add (x : float) (y : float) : float = x +. y
+[@@ocaml.inline always]
+
+let sub (x : float) (y : float) : float = x -. y
+[@@ocaml.inline always]
+
+let div (x : float) (y : float) : float = x /. y
+[@@ocaml.inline always]
+
+let sqrt (x : float) : float = sqrt x
+[@@ocaml.inline always]
+
+(*** Test at runtime that no harmful double rounding seems to
+ be performed with an intermediate 80 bits representation (x87). *)
+let () =
+ let b = ldexp 1. 53 in
+ let s = add 1. (ldexp 1. (-52)) in
+ if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
+ failwith "Detected non IEEE-754 compliant architecture (or wrong \
+ rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64.ml b/kernel/float64_common.ml
index 76005a3dc6..2991a20b49 100644
--- a/kernel/float64.ml
+++ b/kernel/float64_common.ml
@@ -88,21 +88,6 @@ let classify x =
| FP_nan -> NaN
[@@ocaml.inline always]
-external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul"
-[@@unboxed] [@@noalloc]
-
-external add : float -> float -> float = "coq_fadd_byte" "coq_fadd"
-[@@unboxed] [@@noalloc]
-
-external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub"
-[@@unboxed] [@@noalloc]
-
-external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv"
-[@@unboxed] [@@noalloc]
-
-external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt"
-[@@unboxed] [@@noalloc]
-
let of_int63 x = Uint63.to_float x
[@@ocaml.inline always]
@@ -157,12 +142,3 @@ let total_compare f1 f2 =
let is_float64 t =
Obj.tag t = Obj.double_tag
[@@ocaml.inline always]
-
-(*** Test at runtime that no harmful double rounding seems to
- be performed with an intermediate 80 bits representation (x87). *)
-let () =
- let b = ldexp 1. 53 in
- let s = add 1. (ldexp 1. (-52)) in
- if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
- failwith "Detected non IEEE-754 compliant architecture (or wrong \
- rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64_common.mli b/kernel/float64_common.mli
new file mode 100644
index 0000000000..4fb1c114a5
--- /dev/null
+++ b/kernel/float64_common.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** [t] is currently implemented by OCaml's [float] type.
+
+Beware: NaNs have a sign and a payload, while they should be
+indistinguishable from Coq's perspective. *)
+type t = float
+
+(** Test functions for special values to avoid calling [classify] *)
+val is_nan : t -> bool
+val is_infinity : t -> bool
+val is_neg_infinity : t -> bool
+
+val of_string : string -> t
+
+(** Print a float exactly as an hexadecimal value (exact decimal
+ * printing would be possible but sometimes requires more than 700
+ * digits). *)
+val to_hex_string : t -> string
+
+(** Print a float as a decimal value. The printing is not exact (the
+ * real value printed is not always the given floating-point value),
+ * however printing is precise enough that forall float [f],
+ * [of_string (to_decimal_string f) = f]. *)
+val to_string : t -> string
+
+val compile : t -> string
+
+val of_float : float -> t
+
+(** Return [true] for "-", [false] for "+". *)
+val sign : t -> bool
+
+val opp : t -> t
+val abs : t -> t
+
+type float_comparison = FEq | FLt | FGt | FNotComparable
+
+val eq : t -> t -> bool
+
+val lt : t -> t -> bool
+
+val le : t -> t -> bool
+
+(** The IEEE 754 float comparison.
+ * NotComparable is returned if there is a NaN in the arguments *)
+val compare : t -> t -> float_comparison
+[@@ocaml.inline always]
+
+type float_class =
+ | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+val classify : t -> float_class
+[@@ocaml.inline always]
+
+(** Link with integers *)
+val of_int63 : Uint63.t -> t
+[@@ocaml.inline always]
+
+val normfr_mantissa : t -> Uint63.t
+[@@ocaml.inline always]
+
+(** Shifted exponent extraction *)
+val eshift : int
+
+val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *)
+[@@ocaml.inline always]
+
+val ldshiftexp : t -> Uint63.t -> t
+[@@ocaml.inline always]
+
+val next_up : t -> t
+
+val next_down : t -> t
+
+(** Return true if two floats are equal.
+ * All NaN values are considered equal. *)
+val equal : t -> t -> bool
+[@@ocaml.inline always]
+
+val hash : t -> int
+
+(** Total order relation over float values. Behaves like [Pervasives.compare].*)
+val total_compare : t -> t -> int
+
+val is_float64 : Obj.t -> bool
+[@@ocaml.inline always]
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index d4d7150222..5b2a7bd9c2 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -2,6 +2,7 @@ Names
TransparentState
Uint63
Parray
+Float64_common
Float64
Univ
UGraph
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5873d1f502..c7b866179b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,12 +80,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let j = Typeops.infer env' c in
assert (j.uj_val == c); (* relevances should already be correct here *)
let typ = cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
+ let cst' = Reduction.infer_conv_leq env' j.uj_type typ in
j.uj_val, cst'
| Def cs ->
let c' = Mod_subst.force_constr cs in
- c, Reduction.infer_conv env' (Environ.universes env') c c'
+ c, Reduction.infer_conv env' c c'
| Primitive _ ->
error_incorrect_with_constraint lab
in
@@ -103,12 +102,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let j = Typeops.infer env' c in
assert (j.uj_val == c); (* relevances should already be correct here *)
let typ = cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
+ let cst' = Reduction.infer_conv_leq env' j.uj_type typ in
cst'
| Def cs ->
let c' = Mod_subst.force_constr cs in
- let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+ let cst' = Reduction.infer_conv env' c c' in
cst'
| Primitive _ ->
error_incorrect_with_constraint lab
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 01e9550ec5..fc6afb79d4 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -176,7 +176,7 @@ let native_conv cv_pb sigma env t1 t2 =
else Constr.eq_constr_univs univs t1 t2
in
if not b then
- let univs = (univs, checked_universes) in
+ let state = (univs, checked_universes) in
let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
- let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()
+ let _ = native_conv_gen cv_pb sigma env state t1 t2 in ()
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7c6b869b4a..96bf370342 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -189,7 +189,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:TransparentState.t -> env ->
- ?evars:((existential->constr option) * UGraph.t) ->
+ ?evars:(existential->constr option) ->
'a -> 'a -> unit
exception NotConvertible
@@ -210,9 +210,6 @@ type conv_pb =
let is_cumul = function CUMUL -> true | CONV -> false
type 'a universe_compare = {
- (* used in reduction *)
- compare_graph : 'a -> UGraph.t;
-
(* Might raise NotConvertible *)
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -224,7 +221,7 @@ type 'a universe_state = 'a * 'a universe_compare
type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t
let sort_cmp_universes env pb s0 s1 (u, check) =
(check.compare_sorts env pb s0 s1 u, check)
@@ -765,9 +762,8 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
convert_list l2r infos lft1 lft2 v1 v2 cuniv
| _, _ -> raise NotConvertible
-let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
+let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
- let graph = (snd univs).compare_graph (fst univs) in
let infos = create_clos_infos ~univs:graph ~evars reds env in
let infos = {
cnv_inf = infos;
@@ -815,8 +811,7 @@ let check_inductive_instances cv_pb variance u1 u2 univs =
else raise NotConvertible
let checked_universes =
- { compare_graph = (fun x -> x);
- compare_sorts = checked_sort_cmp_universes;
+ { compare_sorts = checked_sort_cmp_universes;
compare_instances = check_convert_instances;
compare_cumul_instances = check_inductive_instances; }
@@ -878,8 +873,7 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
(univs, Univ.Constraint.union csts csts')
let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
- { compare_graph = (fun (x,_) -> x);
- compare_sorts = infer_cmp_universes;
+ { compare_sorts = infer_cmp_universes;
compare_instances = infer_convert_instances;
compare_cumul_instances = infer_inductive_instances; }
@@ -890,12 +884,12 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
in
if b then ()
else
- let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in
+ let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
()
(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
- let evars, univs = evars in
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
+ let univs = Environ.universes env in
if Flags.profile then
let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
@@ -906,35 +900,37 @@ let conv = gen_conv CONV
let conv_leq = gen_conv CUMUL
let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
+ let graph = Environ.universes env in
let (s, _) =
- clos_gen_conv reds cv_pb l2r evars env univs t1 t2
+ clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
in s
-let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
+let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+ let univs = Environ.universes env in
let b, cstrs =
if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
else Constr.eq_constr_univs_infer univs t1 t2
in
if b then cstrs
else
- let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
- let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in
+ let state = ((univs, Univ.Constraint.empty), inferred_universes) in
+ let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
cstrs
(* Profiling *)
let infer_conv_universes =
if Flags.profile then
let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
- CProfile.profile8 infer_conv_universes_key infer_conv_universes
+ CProfile.profile7 infer_conv_universes_key infer_conv_universes
else infer_conv_universes
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
+ env t1 t2 =
+ infer_conv_universes CONV l2r evars ts env t1 t2
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
+ env t1 t2 =
+ infer_conv_universes CUMUL l2r evars ts env t1 t2
let default_conv cv_pb ?l2r:_ env t1 t2 =
gen_conv cv_pb env t1 t2
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 4ae3838691..7d32596f74 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,14 +31,12 @@ exception NotConvertible
type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
type 'a extended_conversion_function =
?l2r:bool -> ?reds:TransparentState.t -> env ->
- ?evars:((existential->constr option) * UGraph.t) ->
+ ?evars:(existential->constr option) ->
'a -> 'a -> unit
type conv_pb = CONV | CUMUL
type 'a universe_compare = {
- compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *)
-
(* Might raise NotConvertible *)
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -50,7 +48,7 @@ type 'a universe_state = 'a * 'a universe_compare
type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t
val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index da77a2882e..3dee3d2b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -79,8 +79,10 @@ module NamedDecl = Context.Named.Declaration
* STRUCT (params,oldsenv) : inside a local module, with
module parameters [params] and earlier environment [oldsenv]
* SIG (params,oldsenv) : same for a local module type
- - [modresolver] : delta_resolver concerning the module content
- - [paramresolver] : delta_resolver concerning the module parameters
+ - [modresolver] : delta_resolver concerning the module content, that needs to
+ be marshalled on disk
+ - [paramresolver] : delta_resolver in scope but not part of the library per
+ se, that is from functor parameters and required libraries
- [revstruct] : current module content, most recent declarations first
- [modlabels] and [objlabels] : names defined in the current module,
either for modules/modtypes or for constants/inductives.
@@ -1301,7 +1303,9 @@ let import lib cst vodigest senv =
mp,
{ senv with
env;
- modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
+ (* Do NOT store the name quotient from the dependencies in the set of
+ constraints that will be marshalled on disk. *)
+ paramresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.paramresolver;
required = DPmap.add lib.comp_name vodigest senv.required;
loads = (mp,mb)::senv.loads;
sections;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 28baa82666..76a1c190be 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -85,7 +85,7 @@ let make_labmap mp list =
let check_conv_error error why cst poly f env a1 a2 =
try
- let cst' = f env (Environ.universes env) a1 a2 in
+ let cst' = f env a1 a2 in
if poly then
if Constraint.is_empty cst' then cst
else error (IncompatiblePolymorphism (env, a1, a2))
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 87a5666fcc..d381e55dd6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+val check_hyps_inclusion : env -> ?evars:(existential->constr option) ->
GlobRef.t -> Constr.named_context -> unit
(** Types for primitives *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index cc2c2c0b4b..948195797e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -211,5 +211,5 @@ let vm_conv cv_pb env t1 t2 =
else Constr.eq_constr_univs univs t1 t2
in
if not b then
- let univs = (univs, checked_universes) in
- let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+ let state = (univs, checked_universes) in
+ let _ = vm_conv_gen cv_pb env state t1 t2 in ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 14:20:01 +0000