From 2d6de8b102ea3cd05c5d193190faf787ccb84baa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 17:29:26 +0200
Subject: Fix restrict_universe_context removing some universes that do appear
 in the term.

---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index a11e3a2cd3..2d82b93523 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -257,7 +257,7 @@ let do_assumptions kind nl l =
     let t = replace_vars subst t in
     let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in
     let subst' = List.map2 
-      (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) (*FIXME incorrect should also enrich the context of the current assumption with c's context *)
+      (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
       idl refs 
     in
       (subst'@subst, status' && status)) ([],true) l)
-- 
cgit v1.2.3