diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-19 15:24:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-19 15:33:09 +0100 |
| commit | 6550d1ecd5cdd45b4dde353df52d1c20c4dd4fd5 (patch) | |
| tree | 9105f3efe5ca3fa5f6af39201abd23a954dcdb4e /checker/values.ml | |
| parent | 8181467e240d7643e2d9ff5388cd8e5db5cf56d6 (diff) | |
Fixing checker representation of values.
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 0113eca12..08cb08be8 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 bed14962eac3aa2feba45a572f72b9531 checker/cic.mli +MD5 ed14962eac3aa2feba45a572f72b9531 checker/cic.mli *) @@ -52,6 +52,7 @@ let v_enum name n = Sum(name,n,[||]) (** Ocaml standard library *) +let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 let v_ref v = v_tuple "ref" [|v|] @@ -197,7 +198,7 @@ let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] let v_cst_type = - v_sum "constant_type" 0 [|[|v_constr|];[|v_rctxt;v_pol_arity|]|] + v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|] let v_cst_def = v_sum "constant_def" 0 |