diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:28:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | f8e639f3b81ae142f5b529be1ad90210fc259375 (patch) | |
| tree | d73251d05312b34ba8f6e38387c3a07372603588 /pretyping/pretyping.mli | |
| parent | d071eac98b7812ac5c03004b438022900885d874 (diff) | |
Fix interpretation of global universes in univdecl constraints.
Also nicer error when the constraints are impossible.
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index b2735ee22..d0fb5cad9 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -20,6 +20,9 @@ open Glob_term open Ltac_pretype open Evardefine +val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> + Misctypes.glob_level -> Univ.Level.t + (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : |