Fix extraction taking a type in the wrong environment.

Fix restriction of universe contexts to not forget about potentially useful
constraints.

1 files changed, 11 insertions, 2 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 6799a99e5b..dd5331fa71 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -691,13 +691,22 @@ let restrict_universe_context (univs,csts) s =
   (* Universes that are not necessary to typecheck the term.
      E.g. univs introduced by tactics and not used in the proof term. *)
   let diff = LSet.diff univs s in
+  let is_useless l r =
+    let lmem = LSet.mem l diff 
+    and rmem = LSet.mem r diff in
+      lmem && rmem
+      (* if lmem then *)
+      (* 	rmem || not (LSet.mem r univs) *)
+      (* else *)
+      (* 	rmem && not (LSet.mem l s) *)
+  in
   let (univscstrs, csts) =
     Constraint.fold
       (fun (l,d,r as c) (univs, csts) ->
-        if LSet.mem l diff && LSet.mem r diff then (univs, csts)
+        if is_useless l r then (univs, csts)
 	else (LSet.add l (LSet.add r univs), Constraint.add c csts))
     csts (LSet.empty, Constraint.empty)
-  in (LSet.union s (LSet.inter univs univscstrs), csts)
+  in (LSet.inter univs (LSet.union s univscstrs), csts)
 
 let simplify_universe_context (univs,csts) =
   let uf = UF.create () in