diff options
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 : |