From f8e639f3b81ae142f5b529be1ad90210fc259375 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 28 Sep 2017 22:28:21 +0200
Subject: Fix interpretation of global universes in univdecl constraints.

Also nicer error when the constraints are impossible.
---
 pretyping/pretyping.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/pretyping.mli')

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 :
-- 
cgit v1.2.3