diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 79b051845..72e9971d6 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -81,7 +81,7 @@ val understand_ltac : inference_flags -> (** Standard call to get a constr from a glob_constr, resolving implicit args *) val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - evar_map -> env -> glob_constr -> constr Univ.in_universe_context_set + evar_map -> env -> glob_constr -> constr Evd.in_evar_universe_context (** Idem but returns the judgment of the understood term *) |