diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-26 23:06:44 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-26 23:06:44 +0000 |
| commit | ab06ce3344abe42cac82dc5477b43b4951063c4f (patch) | |
| tree | 0c8b4a52fdf59f5666a6e7c45810e8ad5fd9f7f5 /checker/validate.ml | |
| parent | 62112e387e868923a13e07b0844cc8bf2b0a108b (diff) | |
Adapt the checker after commit 15080
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15100 85f007b7-540e-0410-9357-904b9bb8a0f7
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|]|] |