diff --git a/src/reify.ml4 b/src/reify.ml4
index 38790cc66..83d90ebff 100644
--- a/src/reify.ml4
+++ b/src/reify.ml4
@@ -349,9 +349,9 @@ struct
   let cMonomorphic_ctx = resolve_symbol pkg_univ "Monomorphic_ctx"
   let cPolymorphic_ctx = resolve_symbol pkg_univ "Polymorphic_ctx"
   let tUContextmake = resolve_symbol (ext_pkg_univ "UContext") "make"
-  (* let tConstraintempty = resolve_symbol (ext_pkg_univ "Constraint") "empty" *)
-  let tConstraintempty = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "Constraint") "empty")
-  let tConstraintadd = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "Constraint") "add")
+  (* let tConstraintSetempty = resolve_symbol (ext_pkg_univ "ConstraintSet") "empty" *)
+  let tConstraintSetempty = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "ConstraintSet") "empty")
+  let tConstraintSetadd = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "ConstraintSet") "add")
   let tmake_univ_constraint = resolve_symbol pkg_univ "make_univ_constraint"
   let tinit_graph = resolve_symbol pkg_ugraph "init_graph"
   let tadd_global_constraints = resolve_symbol pkg_ugraph  "add_global_constraints"
@@ -513,8 +513,8 @@ struct
     let const = Univ.Constraint.elements const in
     List.fold_left (fun tm c ->
         let c = quote_univ_constraint c in
-        Term.mkApp (tConstraintadd, [| c; tm|])
-      ) tConstraintempty const
+        Term.mkApp (tConstraintSetadd, [| c; tm|])
+      ) tConstraintSetempty const
 
   let quote_ucontext inst const =
     let inst' = quote_univ_instance inst in
diff --git a/test-suite/demo.v b/test-suite/demo.v
index 949656145..bb6116ab3 100644
--- a/test-suite/demo.v
+++ b/test-suite/demo.v
@@ -135,7 +135,7 @@ Definition mut_i : mutual_inductive_entry :=
   mind_entry_finite := Finite;
   mind_entry_params := [];
   mind_entry_inds := [one_i; one_i2];
-  mind_entry_universes := Monomorphic_ctx ([], Constraint.empty);
+  mind_entry_universes := Monomorphic_ctx ([], ConstraintSet.empty);
   mind_entry_private := None;
 |}.
 
@@ -162,7 +162,7 @@ Definition mut_list_i : mutual_inductive_entry :=
   mind_entry_finite := Finite;
   mind_entry_params := [("A", LocalAssum (tSort Universe.type0))];
   mind_entry_inds := [one_list_i];
-  mind_entry_universes := Monomorphic_ctx ([], Constraint.empty);
+  mind_entry_universes := Monomorphic_ctx ([], ConstraintSet.empty);
   mind_entry_private := None;
 |}.
 
@@ -187,7 +187,7 @@ Definition mut_pt_i : mutual_inductive_entry :=
   mind_entry_finite := BiFinite;
   mind_entry_params := [("A", LocalAssum (tSort Universe.type0))];
   mind_entry_inds := [one_pt_i];
-  mind_entry_universes := Monomorphic_ctx ([], Constraint.empty);
+  mind_entry_universes := Monomorphic_ctx ([], ConstraintSet.empty);
   mind_entry_private := None;
 |}.
 
diff --git a/test-suite/univ.v b/test-suite/univ.v
index 68a466750..37417ae98 100644
--- a/test-suite/univ.v
+++ b/test-suite/univ.v
@@ -61,8 +61,8 @@ Module toto.
   (*               tProd nAnon (tSort ((Level.Var 0, false) :: nil)%list) (tRel 1), *)
   (*               1) :: nil; *)
   (*  ind_projs := nil |}] (UContext.make (Level.Var 0 :: Level.Var 1 :: nil)%list *)
-  (*    (Constraint.add (make_univ_constraint (Level.Var 0) Lt (Level.Var 1)) *)
-  (*       Constraint.empty)))) ;; *)
+  (*    (ConstraintSet.add (make_univ_constraint (Level.Var 0) Lt (Level.Var 1)) *)
+  (*       ConstraintSet.empty)))) ;; *)
 
 End toto.
 
diff --git a/theories/Checker.v b/theories/Checker.v
index b2853146b..b93451023 100644
--- a/theories/Checker.v
+++ b/theories/Checker.v
@@ -378,7 +378,7 @@ Inductive type_error :=
 | NotAProduct (t t' : term)
 | NotAnInductive (t : term)
 | IllFormedFix (m : mfixpoint term) (i : nat)
-| UnsatisfiedConstraints (c : Constraint.t)
+| UnsatisfiedConstraints (c : ConstraintSet.t)
 | NotEnoughFuel (n : nat).
 
 Definition string_of_nat (n : nat) := Template.utils.string_of_int n.
@@ -595,7 +595,7 @@ Section Typecheck2.
 
   Definition polymorphic_constraints (u : universe_context) :=
     match u with
-    | Monomorphic_ctx _ => Constraint.empty
+    | Monomorphic_ctx _ => ConstraintSet.empty
     | Polymorphic_ctx ctx => UContext.constraints ctx
     end.
 
diff --git a/theories/Typing.v b/theories/Typing.v
index ed5c6ca59..31e4ef332 100644
--- a/theories/Typing.v
+++ b/theories/Typing.v
@@ -638,7 +638,7 @@ Definition type_global_decl Σ decl :=
 
 Definition contains_init_graph φ :=
   LevelSet.In Level.prop (fst φ) /\ LevelSet.In Level.set (fst φ) /\
-  Constraint.In (Level.prop, ConstraintType.Le, Level.set) (snd φ).
+  ConstraintSet.In (Level.prop, ConstraintType.Le, Level.set) (snd φ).
 
 Definition wf_graph φ :=
   contains_init_graph φ /\ (no_universe_inconsistency φ = true).
diff --git a/theories/UnivSubst.v b/theories/UnivSubst.v
index cbd7c728d..66c2dd134 100644
--- a/theories/UnivSubst.v
+++ b/theories/UnivSubst.v
@@ -21,9 +21,9 @@ Definition subst_instance_level u l :=
   end.
 
 Definition subst_instance_cstrs u cstrs :=
-  Constraint.fold (fun '(l,d,r) =>
-                     Constraint.add (subst_instance_level u l, d, subst_instance_level u r))
-                  cstrs Constraint.empty.
+  ConstraintSet.fold (fun '(l,d,r) =>
+                     ConstraintSet.add (subst_instance_level u l, d, subst_instance_level u r))
+                  cstrs ConstraintSet.empty.
 
 Definition subst_instance_level_expr (u : universe_instance) (s : Universe.Expr.t) :=
   let '(l, b) := s in (subst_instance_level u l, b).
diff --git a/theories/kernel/uGraph.v b/theories/kernel/uGraph.v
index 4044c03c8..37318944a 100644
--- a/theories/kernel/uGraph.v
+++ b/theories/kernel/uGraph.v
@@ -9,7 +9,7 @@ From Template Require Import univ.
 
 (* For the moment we recompute the graph each time *)
 (* TODO the first component is useless *)
-Definition t : Type := LevelSet.t * Constraint.t.
+Definition t : Type := LevelSet.t * ConstraintSet.t.
 
 (* TODO use nat where Z is not useful or BinNat *)
 Local Open Scope Z.
@@ -26,7 +26,7 @@ Definition edges_of_constraint (uc : univ_constraint) : list edge
 
 Definition init_graph : t :=
   let levels := LevelSet.add Level.prop (LevelSet.add Level.set LevelSet.empty) in
-  let constraints := Constraint.add (Level.prop, ConstraintType.Lt, Level.set) Constraint.empty in
+  let constraints := ConstraintSet.add (Level.prop, ConstraintType.Lt, Level.set) ConstraintSet.empty in
   (levels, constraints).
 
 (* The monomorphic levels are > Set while polymorphic ones are >= Set. *)
@@ -35,8 +35,8 @@ Definition add_node (l : Level.t) (G : t) : t
      let constraints :=
          match l with
          | Level.lProp | Level.lSet => snd G (* supposed to be yet here *)
-         | Level.Var _ => Constraint.add (Level.set, ConstraintType.Le, l) (snd G)
-         | Level.Level _ => Constraint.add (Level.set, ConstraintType.Lt, l) (snd G)
+         | Level.Var _ => ConstraintSet.add (Level.set, ConstraintType.Le, l) (snd G)
+         | Level.Level _ => ConstraintSet.add (Level.set, ConstraintType.Lt, l) (snd G)
          end in
      (levels, constraints).
 
@@ -45,7 +45,7 @@ Definition add_constraint (uc : univ_constraint) (G : t) : t
      (* maybe useless if we always add constraints
         in which the universes are declared *)
      let G := add_node l (add_node l' G) in
-     let constraints := Constraint.add uc (snd G) in
+     let constraints := ConstraintSet.add uc (snd G) in
      (fst G, constraints).
 
 Definition repr (uctx : universe_context) : UContext.t :=
@@ -58,7 +58,7 @@ Definition add_global_constraints (uctx : universe_context) (G : t) : t
   := match uctx with
      | Monomorphic_ctx (inst, cstrs) =>
        let G := List.fold_left (fun s l => add_node l s) inst G in
-       Constraint.fold add_constraint cstrs G
+       ConstraintSet.fold add_constraint cstrs G
      | Polymorphic_ctx _ => G
      end.
 
@@ -67,7 +67,7 @@ Section UGraph.
 
   (* FIXME duplicates *)
   Definition edges : list edge
-    := Constraint.fold (fun uc E => edges_of_constraint uc ++ E) (snd φ) [].
+    := ConstraintSet.fold (fun uc E => edges_of_constraint uc ++ E) (snd φ) [].
 
   (* The graph *)
   (* For each node we record its predecessos  *)
@@ -137,8 +137,8 @@ Section UGraph.
     | ConstraintType.Le => check_le_level l r
     end.
 
-  Definition check_constraints (cstrs : Constraint.t) :=
-    Constraint.for_all check_constraint cstrs.
+  Definition check_constraints (cstrs : ConstraintSet.t) :=
+    ConstraintSet.for_all check_constraint cstrs.
 
   Definition check_le_level_expr (e1 e2 : Universe.Expr.t) : bool :=
     match e1, e2 with
diff --git a/theories/kernel/univ.v b/theories/kernel/univ.v
index 983e2030d..6bec945aa 100644
--- a/theories/kernel/univ.v
+++ b/theories/kernel/univ.v
@@ -305,14 +305,14 @@ Module UnivConstraintDec.
     unfold eq. repeat decide equality.
   Defined.
 End UnivConstraintDec.
-Module Constraint := MSets.MSetWeakList.Make UnivConstraintDec.
+Module ConstraintSet := MSets.MSetWeakList.Make UnivConstraintDec.
 
 Definition make_univ_constraint : universe_level -> constraint_type -> universe_level -> univ_constraint
   := fun x y z => (x, y, z).
 
 (** Needs to be in Type because template polymorphism of MSets does not allow setting
     the lowest universe *)
-Definition constraints : Type := Constraint.t.  (* list univ_constraint *)
+Definition constraints : Type := ConstraintSet.t.  (* list univ_constraint *)
 
 (* val empty_constraint : constraints *)
 (* val union_constraint : constraints -> constraints -> constraints *)
@@ -397,15 +397,15 @@ Module UContext.
   Definition t := constrained Instance.t.
 
   (* Definition make : constrained Instance.t -> t := fun x => x. *)
-  Definition make : Instance.t -> Constraint.t -> t := pair.
+  Definition make : Instance.t -> ConstraintSet.t -> t := pair.
 
-  Definition empty : t := (Instance.empty, Constraint.empty).
+  Definition empty : t := (Instance.empty, ConstraintSet.empty).
   (* val is_empty : t -> bool *)
 
   Definition instance : t -> Instance.t := fst.
   Definition constraints : t -> constraints := snd.
 
-  Definition dest : t -> Instance.t * Constraint.t := fun x => x.
+  Definition dest : t -> Instance.t * ConstraintSet.t := fun x => x.
 
   (* (** Keeps the order of the instances *) *)
   (* val union : t -> t -> t *)