diff options
Diffstat (limited to 'checker/validate.ml')
| -rw-r--r-- | checker/validate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/validate.ml b/checker/validate.ml index c5e0bd34d..3feead8e0 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -195,7 +195,7 @@ let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|] let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|] (* univ *) -let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|] +let val_level = val_sum "level" 1 [|[|val_int;val_dp|]|] let val_univ = val_sum "univ" 0 [|[|val_level|];[|val_list val_level;val_list val_level|]|] |