checker and votour ported to new vo format (after -vi2vo)

1 files changed, 8 insertions, 5 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 97958c2b7..79ba6de22 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -416,24 +416,27 @@ let subst_lazy_constr sub = function
 
 let indirect_opaque_access =
   ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
+let indirect_opaque_univ_access =
+  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints)
 
 let force_lazy_constr = function
   | Indirect (l,dp,i) ->
     let c = !indirect_opaque_access dp i in
     force_constr (List.fold_right subst_constr_subst l (from_val c))
 
+let force_lazy_constr_univs = function
+  | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i
+  | _ -> Univ.empty_constraint
+
 let subst_constant_def sub = function
   | Undef inl -> Undef inl
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc ->
-      OpaqueDef (Future.from_val (subst_lazy_constr sub (Future.join lc)))
-
-type constant_constraints = Univ.constraints Future.computation
+  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (force_constr c)
-  | OpaqueDef c -> Some (force_lazy_constr (Future.join c))
+  | OpaqueDef c -> Some (force_lazy_constr c)
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false