summaryrefslogtreecommitdiff
path: root/kernel/mod_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_typing.ml')
-rw-r--r--kernel/mod_typing.ml385
1 files changed, 176 insertions, 209 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e366bc97..3a4c93ec 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -1,12 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mod_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+ the Coq module system *)
+
+(* This module provides the main functions for type-checking module
+ declarations *)
open Util
open Names
@@ -25,17 +29,20 @@ let path_of_mexpr = function
| MSEident mp -> mp
| _ -> raise Not_path
-let rec list_split_assoc k rev_before = function
- | [] -> raise Not_found
- | (k',b)::after when k=k' -> rev_before,b,after
- | h::tail -> list_split_assoc k (h::rev_before) tail
+let rec mp_from_mexpr = function
+ | MSEident mp -> mp
+ | MSEapply (expr,_) -> mp_from_mexpr expr
+ | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
+ | MSEwith (expr,_) -> mp_from_mexpr expr
-let rec list_fold_map2 f e = function
- | [] -> (e,[],[])
- | h::t ->
- let e',h1',h2' = f e h in
- let e'',t1',t2' = list_fold_map2 f e' t in
- e'',h1'::t1',h2'::t2'
+let is_modular = function
+ | SFBmodule _ | SFBmodtype _ -> true
+ | SFBconst _ | SFBmind _ -> false
+
+let rec list_split_assoc ((k,m) as km) rev_before = function
+ | [] -> raise Not_found
+ | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+ | h::tail -> list_split_assoc km (h::rev_before) tail
let discr_resolver env mtb =
match mtb.typ_expr with
@@ -51,136 +58,130 @@ let rec rebuild_mp mp l =
let rec check_with env sign with_decl alg_sign mp equiv =
let sign,wd,equiv,cst= match with_decl with
- | With_Definition (id,_) ->
- let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in
- sign,With_definition_body(id,cb),equiv,cst
- | With_Module (id,mp1) ->
- let sign,equiv,cst =
- check_with_aux_mod env sign with_decl mp equiv in
- sign,With_module_body(id,mp1),equiv,cst in
+ | With_Definition (idl,c) ->
+ let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
+ sign,With_definition_body(idl,cb),equiv,cst
+ | With_Module (idl,mp1) ->
+ let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
+ sign,With_module_body(idl,mp1),equiv,cst
+ in
if alg_sign = None then
sign,None,equiv,cst
else
sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
-and check_with_aux_def env sign with_decl mp equiv =
+and check_with_def env sign (idl,c) mp equiv =
let sig_b = match sign with
| SEBstruct(sig_b) -> sig_b
| _ -> error_signature_expected sign
in
- let id,idl = match with_decl with
- | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
- | With_Definition ([],_) | With_Module ([],_) -> assert false
+ let id,idl = match idl with
+ | [] -> assert false
+ | id::idl -> id,idl
in
let l = label_of_id id in
try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
+ let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
let before = List.rev rev_before in
let env' = Modops.add_signature mp before equiv env in
- match with_decl with
- | With_Definition ([],_) -> assert false
- | With_Definition ([id],c) ->
+ if idl = [] then
+ (* Toplevel definition *)
let cb = match spec with
- SFBconst cb -> cb
+ | SFBconst cb -> cb
| _ -> error_not_a_constant l
in
- begin
- match cb.const_body with
- | None ->
- let (j,cst1) = Typeops.infer env' c in
- let typ = Typeops.type_of_constant_type env' cb.const_type in
- let cst2 = Reduction.conv_leq env' j.uj_type typ in
- let cst =
- Constraint.union
- (Constraint.union cb.const_constraints cst1)
- cst2 in
- let body = Some (Declarations.from_val j.uj_val) in
- let cb' = {cb with
- const_body = body;
- const_body_code = Cemitcodes.from_val
- (compile_constant_body env' body false false);
- const_constraints = cst} in
- SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
- | Some b ->
- let cst1 = Reduction.conv env' c (Declarations.force b) in
- let cst = Constraint.union cb.const_constraints cst1 in
- let body = Some (Declarations.from_val c) in
- let cb' = {cb with
- const_body = body;
- const_body_code = Cemitcodes.from_val
- (compile_constant_body env' body false false);
- const_constraints = cst} in
- SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
- end
- | With_Definition (_::_,c) ->
+ (* In the spirit of subtyping.check_constant, we accept
+ any implementations of parameters and opaques terms,
+ as long as they have the right type *)
+ let def,cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let (j,cst1) = Typeops.infer env' c in
+ let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let cst2 = Reduction.conv_leq env' j.uj_type typ in
+ let cst =
+ union_constraints
+ (union_constraints cb.const_constraints cst1)
+ cst2
+ in
+ let def = Def (Declarations.from_val j.uj_val) in
+ def,cst
+ | Def cs ->
+ let cst1 = Reduction.conv env' c (Declarations.force cs) in
+ let cst = union_constraints cb.const_constraints cst1 in
+ let def = Def (Declarations.from_val c) in
+ def,cst
+ in
+ let cb' =
+ { cb with
+ const_body = def;
+ const_body_code =
+ Cemitcodes.from_val (compile_constant_body env' def);
+ const_constraints = cst }
+ in
+ SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
+ else
+ (* Definition inside a sub-module *)
let old = match spec with
- SFBmodule msb -> msb
+ | SFBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
in
begin
match old.mod_expr with
| None ->
- let new_with_decl = With_Definition (idl,c) in
let sign,cb,cst =
- check_with_aux_def env' old.mod_type new_with_decl
+ check_with_def env' old.mod_type (idl,c)
(MPdot(mp,l)) old.mod_delta in
let new_spec = SFBmodule({old with
mod_type = sign;
mod_type_alg = None}) in
- SEBstruct(before@((l,new_spec)::after)),cb,cst
+ SEBstruct(before@(l,new_spec)::after),cb,cst
| Some msb ->
- error_a_generative_module_expected l
+ error_generative_module_expected l
end
- | _ -> anomaly "Modtyping:incorrect use of with"
with
- Not_found -> error_no_such_label l
- | Reduction.NotConvertible -> error_with_incorrect l
+ | Not_found -> error_no_such_label l
+ | Reduction.NotConvertible -> error_incorrect_with_constraint l
-and check_with_aux_mod env sign with_decl mp equiv =
+and check_with_mod env sign (idl,mp1) mp equiv =
let sig_b = match sign with
| SEBstruct(sig_b) ->sig_b
| _ -> error_signature_expected sign
in
- let id,idl = match with_decl with
- | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
- | With_Definition ([],_) | With_Module ([],_) -> assert false
+ let id,idl = match idl with
+ | [] -> assert false
+ | id::idl -> id,idl
in
let l = label_of_id id in
try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
+ let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
let before = List.rev rev_before in
- let rec mp_rec = function
- | [] -> mp
- | i::r -> MPdot(mp_rec r,label_of_id i)
- in
let env' = Modops.add_signature mp before equiv env in
- match with_decl with
- | With_Module ([],_) -> assert false
- | With_Module ([id], mp1) ->
+ if idl = [] then
+ (* Toplevel module definition *)
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
in
let mb_mp1 = (lookup_module mp1 env) in
let mtb_mp1 =
- module_type_of_module env' None mb_mp1 in
+ module_type_of_module None mb_mp1 in
let cst =
match old.mod_expr with
None ->
begin
- try Constraint.union
+ try union_constraints
(check_subtypes env' mtb_mp1
- (module_type_of_module env' None old))
+ (module_type_of_module None old))
old.mod_constraints
- with Failure _ -> error_with_incorrect (label_of_id id)
+ with Failure _ -> error_incorrect_with_constraint (label_of_id id)
end
| Some (SEBident(mp')) ->
check_modpath_equiv env' mp1 mp';
old.mod_constraints
- | _ -> error_a_generative_module_expected l
+ | _ -> error_generative_module_expected l
+ in
+ let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false
in
- let new_mb = strengthen_and_subst_mb mb_mp1
- (MPdot(mp,l)) env false in
let new_spec = SFBmodule {new_mb with
mod_mp = MPdot(mp,l);
mod_expr = Some (SEBident mp1);
@@ -190,7 +191,8 @@ and check_with_aux_mod env sign with_decl mp equiv =
let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
add_delta_resolver equiv new_mb.mod_delta,cst
- | With_Module (idc,mp1) ->
+ else
+ (* Module definition of a sub-module *)
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
@@ -198,10 +200,9 @@ and check_with_aux_mod env sign with_decl mp equiv =
begin
match old.mod_expr with
None ->
- let new_with_decl = With_Module (idl,mp1) in
let sign,equiv',cst =
- check_with_aux_mod env'
- old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in
+ check_with_mod env'
+ old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
let new_equiv = add_delta_resolver equiv equiv' in
let new_spec = SFBmodule {old with
mod_type = sign;
@@ -215,14 +216,13 @@ and check_with_aux_mod env sign with_decl mp equiv =
let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
check_modpath_equiv env' mpnew mp;
SEBstruct(before@(l,spec)::after)
- ,equiv,Constraint.empty
+ ,equiv,empty_constraint
| _ ->
- error_a_generative_module_expected l
+ error_generative_module_expected l
end
- | _ -> anomaly "Modtyping:incorrect use of with"
with
Not_found -> error_no_such_label l
- | Reduction.NotConvertible -> error_with_incorrect l
+ | Reduction.NotConvertible -> error_incorrect_with_constraint l
and translate_module env mp inl me =
match me.mod_entry_expr, me.mod_entry_type with
@@ -243,14 +243,14 @@ and translate_module env mp inl me =
let sign,alg1,resolver,cst2 =
match me.mod_entry_type with
| None ->
- sign,None,resolver,Constraint.empty
+ sign,None,resolver,empty_constraint
| Some mte ->
let mtb = translate_module_type env mp inl mte in
let cst = check_subtypes env
{typ_mp = mp;
typ_expr = sign;
typ_expr_alg = None;
- typ_constraints = Constraint.empty;
+ typ_constraints = empty_constraint;
typ_delta = resolver;}
mtb
in
@@ -258,9 +258,9 @@ and translate_module env mp inl me =
in
{ mod_mp = mp;
mod_type = sign;
- mod_expr = Some alg_implem;
+ mod_expr = alg_implem;
mod_type_alg = alg1;
- mod_constraints = Univ.Constraint.union cst1 cst2;
+ mod_constraints = Univ.union_constraints cst1 cst2;
mod_delta = resolver;
mod_retroknowledge = []}
(* spiwack: not so sure about that. It may
@@ -268,125 +268,92 @@ and translate_module env mp inl me =
If it does, I don't really know how to
fix the bug.*)
+and translate_apply env inl ftrans mexpr mkalg =
+ let sign,alg,resolver,cst1 = ftrans in
+ let farg_id, farg_b, fbody_b = destr_functor env sign in
+ let mp1 =
+ try path_of_mexpr mexpr
+ with Not_path -> error_application_to_not_path mexpr
+ in
+ let mtb = module_type_of_module None (lookup_module mp1 env) in
+ let cst2 = check_subtypes env mtb farg_b in
+ let mp_delta = discr_resolver env mtb in
+ let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
+ let subst = map_mbid farg_id mp1 mp_delta
+ in
+ subst_struct_expr subst fbody_b,
+ mkalg alg mp1 cst2,
+ subst_codom_delta_resolver subst resolver,
+ Univ.union_constraints cst1 cst2
+
+and translate_functor env inl arg_id arg_e trans mkalg =
+ let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
+ let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+ let sign,alg,resolver,cst = trans env'
+ in
+ SEBfunctor (arg_id, mtb, sign),
+ mkalg alg arg_id mtb,
+ resolver,
+ Univ.union_constraints cst mtb.typ_constraints
-and translate_struct_module_entry env mp inl mse = match mse with
+and translate_struct_module_entry env mp inl = function
| MSEident mp1 ->
- let mb = lookup_module mp1 env in
- let mb' = strengthen_and_subst_mb mb mp env false in
- mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty
+ let mb = lookup_module mp1 env in
+ let mb' = strengthen_and_subst_mb mb mp false in
+ mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
| MSEfunctor (arg_id, arg_e, body_expr) ->
- let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
- let env' = add_module (module_body_of_type (MPbound arg_id) mtb)
- env in
- let sign,alg,resolver,cst =
- translate_struct_module_entry env' mp inl body_expr in
- SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
- Univ.Constraint.union cst mtb.typ_constraints
+ let trans env' = translate_struct_module_entry env' mp inl body_expr in
+ let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in
+ translate_functor env inl arg_id arg_e trans mkalg
| MSEapply (fexpr,mexpr) ->
- let sign,alg,resolver,cst1 =
- translate_struct_module_entry env mp inl fexpr
- in
- let farg_id, farg_b, fbody_b = destr_functor env sign in
- let mtb,mp1 =
- try
- let mp1 = path_of_mexpr mexpr in
- let mtb = module_type_of_module env None (lookup_module mp1 env) in
- mtb,mp1
- with
- | Not_path -> error_application_to_not_path mexpr
- (* place for nondep_supertype *) in
- let cst = check_subtypes env mtb farg_b in
- let mp_delta = discr_resolver env mtb in
- let mp_delta = if not inl then mp_delta else
- complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
- in
- let subst = map_mbid farg_id mp1 mp_delta in
- (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
- (subst_codom_delta_resolver subst resolver),
- Univ.Constraint.union cst1 cst
+ let trans = translate_struct_module_entry env mp inl fexpr in
+ let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in
+ translate_apply env inl trans mexpr mkalg
| MSEwith(mte, with_decl) ->
- let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in
- let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
- sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2
-
-and translate_struct_type_entry env inl mse = match mse with
+ let sign,alg,resolve,cst1 =
+ translate_struct_module_entry env mp inl mte in
+ let sign,alg,resolve,cst2 =
+ check_with env sign with_decl alg mp resolve in
+ sign,alg,resolve,Univ.union_constraints cst1 cst2
+
+and translate_struct_type_entry env inl = function
| MSEident mp1 ->
- let mtb = lookup_modtype mp1 env in
- mtb.typ_expr,
- Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty
+ let mtb = lookup_modtype mp1 env in
+ mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint
| MSEfunctor (arg_id, arg_e, body_expr) ->
- let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
- let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
- let sign,alg,resolve,mp_from,cst =
- translate_struct_type_entry env' inl body_expr in
- SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from,
- Univ.Constraint.union cst mtb.typ_constraints
+ let trans env' = translate_struct_type_entry env' inl body_expr in
+ translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None)
| MSEapply (fexpr,mexpr) ->
- let sign,alg,resolve,mp_from,cst1 =
- translate_struct_type_entry env inl fexpr
- in
- let farg_id, farg_b, fbody_b = destr_functor env sign in
- let mtb,mp1 =
- try
- let mp1 = path_of_mexpr mexpr in
- let mtb = module_type_of_module env None (lookup_module mp1 env) in
- mtb,mp1
- with
- | Not_path -> error_application_to_not_path mexpr
- (* place for nondep_supertype *) in
- let cst2 = check_subtypes env mtb farg_b in
- let mp_delta = discr_resolver env mtb in
- let mp_delta = if not inl then mp_delta else
- complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
- in
- let subst = map_mbid farg_id mp1 mp_delta in
- (subst_struct_expr subst fbody_b),None,
- (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2
+ let trans = translate_struct_type_entry env inl fexpr in
+ translate_apply env inl trans mexpr (fun _ _ _ -> None)
| MSEwith(mte, with_decl) ->
- let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
- let sign,alg,resolve,cst1 =
- check_with env sign with_decl alg mp_from resolve in
- sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1
+ let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in
+ let sign,alg,resolve,cst2 =
+ check_with env sign with_decl alg (mp_from_mexpr mte) resolve
+ in
+ sign,alg,resolve,Univ.union_constraints cst1 cst2
and translate_module_type env mp inl mte =
- let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
- let mtb = subst_modtype_and_resolver
- {typ_mp = mp_from;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = cst;
- typ_delta = resolve} mp env
- in {mtb with typ_expr_alg = alg}
-
-let rec translate_struct_include_module_entry env mp inl mse = match mse with
+ let mp_from = mp_from_mexpr mte in
+ let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in
+ let mtb = subst_modtype_and_resolver
+ {typ_mp = mp_from;
+ typ_expr = sign;
+ typ_expr_alg = None;
+ typ_constraints = cst;
+ typ_delta = resolve} mp
+ in {mtb with typ_expr_alg = alg}
+
+let rec translate_struct_include_module_entry env mp inl = function
| MSEident mp1 ->
- let mb = lookup_module mp1 env in
- let mb' = strengthen_and_subst_mb mb mp env true in
- let mb_typ = clean_bounded_mod_expr mb'.mod_type in
- mb_typ, mb'.mod_delta,Univ.Constraint.empty
+ let mb = lookup_module mp1 env in
+ let mb' = strengthen_and_subst_mb mb mp true in
+ let mb_typ = clean_bounded_mod_expr mb'.mod_type in
+ mb_typ,None,mb'.mod_delta,Univ.empty_constraint
| MSEapply (fexpr,mexpr) ->
- let sign,resolver,cst1 =
- translate_struct_include_module_entry env mp inl fexpr in
- let farg_id, farg_b, fbody_b = destr_functor env sign in
- let mtb,mp1 =
- try
- let mp1 = path_of_mexpr mexpr in
- let mtb = module_type_of_module env None (lookup_module mp1 env) in
- mtb,mp1
- with
- | Not_path -> error_application_to_not_path mexpr
- (* place for nondep_supertype *) in
- let cst = check_subtypes env mtb farg_b in
- let mp_delta = discr_resolver env mtb in
- let mp_delta = if not inl then mp_delta else
- complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
- in
- let subst = map_mbid farg_id mp1 mp_delta in
- (subst_struct_expr subst fbody_b),
- (subst_codom_delta_resolver subst resolver),
- Univ.Constraint.union cst1 cst
+ let ftrans = translate_struct_include_module_entry env mp inl fexpr in
+ translate_apply env inl ftrans mexpr (fun _ _ _ -> None)
| _ -> error ("You cannot Include a high-order structure.")
-
let rec add_struct_expr_constraints env = function
| SEBident _ -> env
@@ -397,7 +364,7 @@ let rec add_struct_expr_constraints env = function
| SEBstruct (structure_body) ->
List.fold_left
- (fun env (l,item) -> add_struct_elem_constraints env item)
+ (fun env (_,item) -> add_struct_elem_constraints env item)
env
structure_body
@@ -442,17 +409,17 @@ let rec struct_expr_constraints cst = function
| SEBstruct (structure_body) ->
List.fold_left
- (fun cst (l,item) -> struct_elem_constraints cst item)
+ (fun cst (_,item) -> struct_elem_constraints cst item)
cst
structure_body
| SEBapply (meb1,meb2,cst1) ->
struct_expr_constraints
- (struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1)
+ (struct_expr_constraints (Univ.union_constraints cst1 cst) meb1)
meb2
| SEBwith(meb,With_definition_body(_,cb))->
struct_expr_constraints
- (Univ.Constraint.union cb.const_constraints cst) meb
+ (Univ.union_constraints cb.const_constraints cst) meb
| SEBwith(meb,With_module_body(_,_))->
struct_expr_constraints cst meb
@@ -468,11 +435,11 @@ and module_constraints cst mb =
| Some meb -> struct_expr_constraints cst meb in
let cst =
struct_expr_constraints cst mb.mod_type in
- Univ.Constraint.union mb.mod_constraints cst
+ Univ.union_constraints mb.mod_constraints cst
and modtype_constraints cst mtb =
- struct_expr_constraints (Univ.Constraint.union mtb.typ_constraints cst) mtb.typ_expr
+ struct_expr_constraints (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr
-let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty
-let module_constraints = module_constraints Univ.Constraint.empty
+let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
+let module_constraints = module_constraints Univ.empty_constraint
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 10:07:23 +0000