From 8966c9241207b6f5d4ee38508246ee97ed006e72 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 31 Jul 2017 16:49:06 +0200
Subject: proof_global: cleanup and comment close_proof

evd: Move constrain_variables to an operation on UState

Necessary to check universe declarations correctly for deferred proofs
in particular.
---
 engine/evd.mli    |  2 +-
 engine/uState.ml  | 28 ++++++++++++++++++----------
 engine/uState.mli |  2 +-
 3 files changed, 20 insertions(+), 12 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.mli b/engine/evd.mli
index 76fa69e313..8c3771cd94 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context
 val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
-val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context
 
 
 val evar_universe_context_of_binders :
diff --git a/engine/uState.ml b/engine/uState.ml
index 312502491c..979a9b086b 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -101,16 +101,6 @@ let initial_graph ctx = ctx.uctx_initial_universes
 
 let algebraics ctx = ctx.uctx_univ_algebraic
 
-let constrain_variables diff ctx =
-  Univ.LSet.fold
-    (fun l cstrs ->
-      try
-        match Univ.LMap.find l ctx.uctx_univ_variables with
-        | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
-        | None -> cstrs
-      with Not_found | Option.IsNone -> cstrs)
-    diff Univ.Constraint.empty
-
 let add_uctx_names ?loc s l (names, names_rev) =
   (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
 
@@ -242,6 +232,24 @@ let add_universe_constraints ctx cstrs =
       uctx_univ_variables = vars;
       uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
+let constrain_variables diff ctx =
+  let univs, local = ctx.uctx_local in
+  let univs, vars, local =
+    Univ.LSet.fold
+      (fun l (univs, vars, cstrs) ->
+        try
+          match Univ.LMap.find l vars with
+          | Some u ->
+             (Univ.LSet.add l univs,
+              Univ.LMap.remove l vars,
+              Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs)
+          | None -> (univs, vars, cstrs)
+        with Not_found | Option.IsNone -> (univs, vars, cstrs))
+      diff (univs, ctx.uctx_univ_variables, local)
+  in
+  { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
+  
+
 let pr_uctx_level uctx = 
   let map, map_rev = uctx.uctx_names in 
     fun l ->
diff --git a/engine/uState.mli b/engine/uState.mli
index ba03058693..0b67bb71f8 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -108,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
 
 val normalize_variables : t -> Univ.universe_subst * t
 
-val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> t -> t
 
 val abstract_undefined_variables : t -> t
 
-- 
cgit v1.2.3