From ab06ce3344abe42cac82dc5477b43b4951063c4f Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 26 Mar 2012 23:06:44 +0000 Subject: Adapt the checker after commit 15080 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15100 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/validate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/validate.ml') 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|]|] -- cgit v1.2.3