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: typing.mli 6113 2004-09-17 20:28:19Z barras $ i*)
17
(* This module provides the typing machine with existential variables
18
(but without universes). *)
20
(* Typecheck a term and return its type *)
21
val type_of : env -> evar_map -> constr -> types
22
(* Typecheck a type and return its sort *)
23
val sort_of : env -> evar_map -> types -> sorts
24
(* Typecheck a term has a given type (assuming the type is OK *)
25
val check : env -> evar_map -> constr -> types -> unit
27
(* The same but with metas... *)
28
val mtype_of : env -> evar_defs -> constr -> types
29
val msort_of : env -> evar_defs -> types -> sorts
30
val mcheck : env -> evar_defs -> constr -> types -> unit
31
val meta_type : evar_defs -> metavariable -> types
33
(* unused typing function... *)
34
val mtype_of_type : env -> evar_defs -> types -> types