From 6bcf420febbce8092db54eb23ed17fa3963c0c99 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 Apr 2013 16:05:16 +0000
Subject: Checker: vo validation is now done in check.ml (and always)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/values.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index 386f853654..227f18ca25 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -267,14 +267,16 @@ let v_deps = Array (v_tuple "dep" [|v_dp;String|])
 let v_compiled_lib =
   v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
 
-(** Library objects (unused by the checker) *)
+(** Library objects *)
 
 let v_obj = Tuple ("Dyn.t",[|String;Any|])
 let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
 let v_libobjs = List v_libobj
 let v_libraryobjs = Tuple ("library_objects",[|v_mp;v_libobjs;v_libobjs|])
 
-(** Main structure of a vo (opaque tables left aside) *)
+(** Main structures of a vo *)
 
 let v_lib =
-  Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps; List v_dp|])
+  Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
+
+let v_opaques = Array v_constr
-- 
cgit v1.2.3