From bff2278b7e558a58cb322edfb301c6241adf379b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 1 Sep 2017 16:22:52 +0200
Subject: Remove unused output of Universes.normalize_univ_variables

---
 engine/uState.ml     |  2 +-
 engine/univSubst.ml  | 12 ++++++------
 engine/univSubst.mli |  2 +-
 engine/universes.mli |  2 +-
 4 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index 81ab3dd66..0791e4c27 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -583,7 +583,7 @@ let refresh_constraints univs (ctx, cstrs) =
   in ((ctx, cstrs'), univs')
 
 let normalize_variables uctx =
-  let normalized_variables, undef, def, subst = 
+  let normalized_variables, def, subst =
     UnivSubst.normalize_univ_variables uctx.uctx_univ_variables
   in
   let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 6a433d9fb..2f59a3fa8 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -162,13 +162,13 @@ let subst_opt_univs_constr s =
 
 let normalize_univ_variables ctx =
   let ctx = normalize_opt_subst ctx in
-  let undef, def, subst =
-    Univ.LMap.fold (fun u v (undef, def, subst) ->
+  let def, subst =
+    Univ.LMap.fold (fun u v (def, subst) ->
       match v with
-      | None -> (Univ.LSet.add u undef, def, subst)
-      | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
-    ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
-  in ctx, undef, def, subst
+      | None -> (def, subst)
+      | Some b -> (Univ.LSet.add u def, Univ.LMap.add u b subst))
+    ctx (Univ.LSet.empty, Univ.LMap.empty)
+  in ctx, def, subst
 
 let pr_universe_body = function
   | None -> mt ()
diff --git a/engine/univSubst.mli b/engine/univSubst.mli
index 26e8d1db9..e76d25333 100644
--- a/engine/univSubst.mli
+++ b/engine/univSubst.mli
@@ -23,7 +23,7 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn
 val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 
 val normalize_univ_variables : universe_opt_subst ->
-  universe_opt_subst * LSet.t * LSet.t * universe_subst
+  universe_opt_subst * LSet.t * universe_subst
 
 val normalize_univ_variable :
   find:(Level.t -> Universe.t) ->
diff --git a/engine/universes.mli b/engine/universes.mli
index 306ba0db0..ad937471e 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -154,7 +154,7 @@ val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 [@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"]
 
 val normalize_univ_variables : universe_opt_subst ->
-  universe_opt_subst * LSet.t * LSet.t * universe_subst
+  universe_opt_subst * LSet.t * universe_subst
 [@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"]
 
 val normalize_univ_variable :
-- 
cgit v1.2.3