diff options
| author | herbelin | 2001-09-19 16:55:41 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-19 16:55:41 +0000 |
| commit | f83572bc45b9ab6b72688eb22d125896541ccf16 (patch) | |
| tree | 37e08a39ea53751d9fdd7dff4449f4125e3f7bfd /kernel/typeops.ml | |
| parent | 3607bb83605ff596445e0f18016d1fbb3d66d584 (diff) | |
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 317cc199d6..3e8de823a6 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -302,7 +302,7 @@ let is_correct_arity env sigma kelim (c,pj) indf t = | IsProd (_,a1,a2), _ -> let k = whd_betadeltaiota env sigma a2 in let ksort = match kind_of_term k with - | IsSort s -> elimination_of_sort s + | IsSort s -> family_of_sort s | _ -> raise (Arity None) in let ind = build_dependent_inductive indf in let univ = @@ -316,7 +316,7 @@ let is_correct_arity env sigma kelim (c,pj) indf t = raise (Arity None) | k, ki -> let ksort = match k with - | IsSort s -> elimination_of_sort s + | IsSort s -> family_of_sort s | _ -> raise (Arity None) in if List.exists ((=) ksort) kelim then (false, pt'), u @@ -326,9 +326,9 @@ let is_correct_arity env sigma kelim (c,pj) indf t = try srec (pj.uj_type,t) Constraint.empty with Arity kinds -> let create_sort = function - | ElimOnProp -> prop - | ElimOnSet -> spec - | ElimOnType -> Type (Univ.new_univ ()) in + | InProp -> prop + | InSet -> spec + | InType -> Type (Univ.new_univ ()) in let listarity = (List.map (fun s -> make_arity env true indf (create_sort s)) kelim) @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim) |