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 /pretyping/pattern.ml | |
| 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 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 01ccd27fa3..f423777d9b 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -171,7 +171,7 @@ let matches_core convert pat c = | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma - | PSort RType, IsSort (Type _) -> sigma + | PSort (RType _), IsSort (Type _) -> sigma | PApp (c1,arg1), IsApp (c2,arg2) -> (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 @@ -309,7 +309,7 @@ let rec pattern_of_constr t = | IsMeta n -> PMeta (Some n) | IsVar id -> PVar id | IsSort (Prop c) -> PSort (RProp c) - | IsSort (Type _) -> PSort RType + | IsSort (Type _) -> PSort (RType None) | IsCast (c,_) -> pattern_of_constr c | IsLetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | IsProd (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) |