1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: mod_typing.mli 11170 2008-06-25 08:31:04Z soubiran $ i*)
19
val translate_module : env -> module_entry -> module_body
21
val translate_struct_entry : env -> module_struct_entry ->
22
struct_expr_body * substitution
24
val add_modtype_constraints : env -> module_type_body -> env
26
val add_module_constraints : env -> module_body -> env
28
val add_struct_expr_constraints : env -> struct_expr_body -> env
30
val struct_expr_constraints : struct_expr_body -> Univ.constraints
32
val module_constraints : module_body -> Univ.constraints