diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-21 18:24:59 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 0499f51cedb38eba6b8ecd01ce94ddfb1b6ae9c8 (patch) | |
| tree | eb43b12647b93e52784c9118d77c7a64199989a5 /checker/values.ml | |
| parent | f7338257584ba69e7e815c7ef9ac0d24f0dec36c (diff) | |
checker and votour ported to new vo format (after -vi2vo)
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/checker/values.ml b/checker/values.ml index a047c8005..0a2e53799 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -191,14 +191,14 @@ let v_cst_type = let v_cst_def = v_sum "constant_def" 0 - [|[|Opt Int|]; [|v_cstr_subst|]; [|v_computation v_lazy_constr|]|] + [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; v_cst_type; Any; - v_computation v_cstrs; + v_cstrs; v_bool|] let v_recarg = v_sum "recarg" 1 (* Norec *) @@ -300,7 +300,8 @@ let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) let v_lib = Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) -let v_opaques = Array v_constr +let v_opaques = Array (v_computation v_constr) +let v_univopaques = Opt (Array (v_computation v_cstrs)) (** Registering dynamic values *) |