diff options
| author | Matthieu Sozeau | 2016-05-25 13:49:50 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-06 14:38:05 +0200 |
| commit | f77c2b488ca552b2316d4ebab1c051cb5a1347ab (patch) | |
| tree | 1efb41cfb54c9b06b70971b788e928e430c7e58c /toplevel | |
| parent | a7ed091b6842cc78f0480504e84c3cfa261860bd (diff) | |
Renaming to more generic has_dependent_elim test
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/indschemes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ecee2e540c..f9e6c207c3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind = let kind = inductive_sort_family mip in let dep = if kind == InProp then case_scheme_kind_from_prop - else if Inductiveops.is_primitive_record_without_eta mib then + else if not (Inductiveops.has_dependent_elim mib) then case_scheme_kind_from_type else case_dep_scheme_kind_from_type in let kelim = elim_sorts (mib,mip) in @@ -250,14 +250,14 @@ let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let from_prop = kind == InProp in - let primwithouteta = Inductiveops.is_primitive_record_without_eta mib in + let depelim = Inductiveops.has_dependent_elim mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> if Sorts.List.mem sort kelim then Some kind else None) (if from_prop then kinds_from_prop - else if primwithouteta then nondep_kinds_from_type - else kinds_from_type) in + else if depelim then kinds_from_type + else nondep_kinds_from_type) in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims |