From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 21:55:33 +0100 Subject: Clenv API using EConstr. --- pretyping/typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typing.mli') diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1fb414906..94a56b6e1 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -31,7 +31,7 @@ val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit (** Returns the instantiated type of a metavariable *) -val meta_type : evar_map -> metavariable -> types +val meta_type : evar_map -> metavariable -> EConstr.types (** Solve existential variables using typing *) val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr -- cgit v1.2.3