From ec4aa4971f7789eeccec2f38f2bb7ec976f87ede Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Aug 2018 15:21:12 +0200
Subject: Do not catch already declared universes in Environ.add_universes

Include is still causing repeat declarations in add_universes_set
---
 kernel/environ.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e7efa5e2c9..778c9a24dd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -365,8 +365,7 @@ let push_constraints_to_env (_,univs) env =
 
 let add_universes strict ctx g =
   let g = Array.fold_left
-	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+            (fun g v -> UGraph.add_universe v strict g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
@@ -376,6 +375,7 @@ let push_context ?(strict=false) ctx env =
 
 let add_universes_set strict ctx g =
   let g = Univ.LSet.fold
+            (* Be lenient, module typing reintroduces universes and constraints due to includes *)
 	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
-- 
cgit v1.2.3