diff options
| author | coq | 2001-05-29 16:11:18 +0000 |
|---|---|---|
| committer | coq | 2001-05-29 16:11:18 +0000 |
| commit | 982812b7e66746d588fc9dcf37da21f891cf8948 (patch) | |
| tree | df82489723d9f4db73fef36568c0abbd3cbb07bd /contrib/interface | |
| parent | e4adec22d1525a4eb0b59285dc4c8c7d41d63128 (diff) | |
Facilites pour le debogguage des univers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/dad.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 1fefb6c444..c26a8039d4 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -181,7 +181,7 @@ let more_general_pat pat1 pat2 = | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma - | PSort RType, PSort RType -> sigma + | PSort (RType _), PSort (RType _) -> sigma | PApp (c1,arg1), PApp (c2,arg2) -> (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 0ce95049ae..63ef38e4f5 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1564,7 +1564,7 @@ let rec cvt_varg = | _ -> xlate_error "cvt_varg : PROP : Failed match ") | Node (_, "CONSTR", ((Node (_, "PROP", [])) :: [])) -> Varg_sorttype (CT_sortc "Prop") - | Node (_, "CONSTR", ((Node (_, "TYPE", [])) :: [])) -> + | Node (_, "CONSTR", ((Node (_, "TYPE", _)) :: [])) -> Varg_sorttype (CT_sortc "Type") | Node (_, "CONSTR", [c]) -> Varg_constr (xlate_formula c) | Node (_, "CONSTRLIST", cs) -> Varg_constrlist (List.map xlate_formula cs) |