j
k
j a
j l
Est-ce que quelque chosde la forme:
type lexp_context = env_elem myers (* ancien env *) type db_context = senv_length * scope (* ancien senv *)
type elab_context = db_context * lexp_context * property_env
serait mieux ?
Pièces jointes :
Retour au fil de discussion
Retour à la liste