checker validation fixed w.r.t. Futures

still not working, it complains about the universe constraint
set...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 4 deletions

diff --git a/checker/values.ml b/checker/values.ml
index eb18bf34b1..f8244e06d2 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 1e607e046b15faeee5912eda83dbb1ba  checker/cic.mli
+MD5 43e0b61e2a549058ae0a59bbadbb9d61 checker/cic.mli
 
 *)
 
@@ -64,6 +64,14 @@ let v_map vk vd =
     [|[|m; Annot("key",vk); Annot("data",vd); m; Annot("bal",Int)|]|])
   in m
 
+(* lib/future *)
+let v_computation f =
+  Annot ("Future.computation",
+  v_ref
+    (v_sum "computation" 2
+      [| [| Fail "Closure" |];
+         [| f ; v_sum "option" 1 [| [| Fail "Val(_,Some _)" |] |] |];
+     [| Fail "Exn" |] |]))
 
 (** kernel/names *)
 
@@ -186,7 +194,7 @@ let v_cst_type =
 
 let v_cst_def =
   v_sum "constant_def" 0
-    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
+    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_computation v_lazy_constr|]|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
diff --git a/lib/future.ml b/lib/future.ml
index b1b9607182..9333089fbe 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -29,11 +29,11 @@ let _ = Errors.register_handler (function
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
 type 'a comp =
+  | Delegated
+  | Dropped
   | Closure of (unit -> 'a)
   | Val of 'a * Dyn.t option
   | Exn of exn
-  | Delegated
-  | Dropped
 
 type 'a computation = 'a comp ref