From 2f56f0fcf21902bb1317f1d6f7ba4b593d712646 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 5 Nov 2015 16:04:43 -0500
Subject: Fix bug #4293: ensure let-ins do not contain algebraic universes in
 their type annotation.

---
 pretyping/evarsolve.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 21d976091..86a1e3e0c 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,7 +34,8 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?inferred:bool -> ?onlyalg:bool (* Only algebraic universes *) ->
+val refresh_universes : ?status:Evd.rigid ->
+			?onlyalg:bool (* Only algebraic universes *) ->
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
-- 
cgit v1.2.3