diff options
| -rw-r--r-- | interp/constrextern.ml | 5 | ||||
| -rw-r--r-- | kernel/constr.ml | 2 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 11 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 11 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 2 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 11 | ||||
| -rw-r--r-- | test-suite/success/cumulativity.v | 9 |
8 files changed, 31 insertions, 22 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d5cb25d1fb..c2afa097bb 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1314,7 +1314,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) - | PSort s -> GSort s + | PSort Sorts.InSProp -> GSort GSProp + | PSort Sorts.InProp -> GSort GProp + | PSort Sorts.InSet -> GSort GSet + | PSort Sorts.InType -> GSort (GType []) | PInt i -> GInt i let extern_constr_pattern env sigma pat = diff --git a/kernel/constr.ml b/kernel/constr.ml index 11958c9108..d74c96af84 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -860,7 +860,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && - eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 + leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index bc083ed9d9..6bfbb9a9c0 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -17,7 +17,6 @@ open Constr open Context open Globnames open Termops -open Term open EConstr open Vars open Pattern @@ -280,14 +279,8 @@ let matches_core env sigma allow_bound_rels | PRel n1, Rel n2 when Int.equal n1 n2 -> subst | PSort ps, Sort s -> - - let open Glob_term in - begin match ps, ESorts.kind sigma s with - | GProp, Prop -> subst - | GSet, Set -> subst - | GType _, Type _ -> subst - | _ -> raise PatternMatchingFailure - end + if Sorts.family_equal ps (Sorts.family (ESorts.kind sigma s)) + then subst else raise PatternMatchingFailure | PApp (p, [||]), _ -> sorec ctx env subst p t diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index affed5389f..74432cc010 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -47,11 +47,18 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with -| GProp, GProp -> true +| GSProp, GSProp +| GProp, GProp | GSet, GSet -> true | GType l1, GType l2 -> List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2 -| _ -> false +| (GSProp|GProp|GSet|GType _), _ -> false + +let glob_sort_family = let open Sorts in function +| GSProp -> InSProp +| GProp -> InProp +| GSet -> InSet +| GType _ -> InType let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Decl_kinds.Explicit, Decl_kinds.Explicit -> true diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index c189a3bcb2..2f0ac76235 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -15,6 +15,8 @@ open Glob_term val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool +val glob_sort_family : 'a glob_sort_gen -> Sorts.family + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val alias_of_pat : 'a cases_pattern_g -> Name.t diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 2ca7f21e8d..d1c0a4ea2a 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -32,7 +32,7 @@ type constr_pattern = | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern - | PSort of Glob_term.glob_sort + | PSort of Sorts.family | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 13034d078a..4e3c77cb1a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Nameops -open Term open Constr open Context open Glob_term @@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> Name.equal v1 v2 && constr_pattern_eq b1 b2 && Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2 -| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2 +| PSort s1, PSort s2 -> Sorts.family_equal s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 @@ -154,10 +153,7 @@ let pattern_of_constr env sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort SProp -> PSort GSProp - | Sort Prop -> PSort GProp - | Sort Set -> PSort GSet - | Sort (Type _) -> PSort (GType []) + | Sort s -> PSort (Sorts.family s) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na.binder_name, pattern_of_constr env c,Some (pattern_of_constr env t), @@ -416,8 +412,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) - | GSort s -> - PSort s + | GSort gs -> PSort (Glob_ops.glob_sort_family gs) | GHole _ -> PMeta None | GCast (c,_) -> diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 3d97f27b16..31fed98952 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -137,3 +137,12 @@ Module WithIndex. Monomorphic Constraint i < j. Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _. End WithIndex. + +Module CumulApp. + + (* i is covariant here, and we have one parameter *) + Inductive foo@{i} (A : nat) : Type@{i+1} := mkfoo (B : Type@{i}). + + Definition bar@{i j|i<=j} := fun x : foo@{i} 0 => x : foo@{j} 0. + +End CumulApp. |