From 83188dacc43df02245d13810d08cc63b7a5633ed Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 28 May 2015 14:13:12 +0200
Subject: Fixup for 866c41b

---
 pretyping/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fe96aa347d..60b1da7049 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -339,7 +339,7 @@ let evar_universe_context_set diff ctx =
 	 match Univ.LMap.find l ctx.uctx_univ_variables with
 	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
 	 | None -> cstrs
-       with Not_found -> cstrs)
+       with Not_found | Option.IsNone -> cstrs)
       (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
   in
     Univ.ContextSet.add_constraints cstrs initctx 
-- 
cgit v1.2.3