@@ -926,6 +926,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty)

• | Proj (l,lxp,lbl) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in

Looks good.

@@ -1014,6 +1015,7 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v

• | Proj (l,lxp,lbl) -> get_type ctx lxp | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in

Ici, par contre ça n'est pas correct: le type de `Proj foo "field"` ne devrait pas être le même que le type de `foo`: il faut renvoyer le type de l'élément "field".

@@ -1145,6 +1147,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v)

• | L.Proj (l,lxp,lbl) -> erase_type lctx lxp | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

Ici non plus: `erase_type` doit revnoyer la version `elexp` de l'expression qu'il reçoit, et ici tu remplaces `Proj lexp label` par just `lexp` donc tu jettes l'opération de projection :-(

À la place, il faut ajouter un nouveau constructeur `Proj` à `elexp` et tranformer un `L.Proj` en un `E.Proj`.

Stefan