From 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 Apr 2020 23:06:35 +0200
Subject: Remove mod_constraints field of module body

---
 kernel/declarations.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 244cd2865d..d5f219b55f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -293,8 +293,6 @@ and 'a generic_module_body =
     mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
-    mod_constraints : Univ.ContextSet.t; (**
-      set of all universes constraints in the module  *)
     mod_delta : Mod_subst.delta_resolver; (**
       quotiented set of equivalent constants and inductive names *)
     mod_retroknowledge : 'a module_retroknowledge }
-- 
cgit v1.2.3