blob: f24ee3914a52053d9827002b2bbf0adbfe9d0633 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* $Id$ *)
(*i*)
open Term
open Environ
open Evd
(*i*)
(* This module provides the typing machine with existential variables
(but without universes). *)
val type_of : unsafe_env -> 'a evar_map -> constr -> constr
val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type
|
