diff options
| author | Gaëtan Gilbert | 2017-10-31 17:04:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 23f84f37c674a07e925925b7e0d50d7ee8414093 (patch) | |
| tree | 7e470de5769c994d8df37c44fed12cf299d5b194 /vernac/indschemes.ml | |
| parent | 75508769762372043387c67a9abe94e8f940e80a (diff) | |
Add relevance marks on binders.
Kernel should be mostly correct, higher levels do random stuff at
times.
Diffstat (limited to 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 28ee3d184f..1e733acc59 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -228,17 +228,20 @@ let declare_one_case_analysis_scheme ind = let kinds_from_prop = [InType,rect_scheme_kind_from_prop; InProp,ind_scheme_kind_from_prop; - InSet,rec_scheme_kind_from_prop] + InSet,rec_scheme_kind_from_prop; + InSProp,sind_scheme_kind_from_prop] let kinds_from_type = [InType,rect_dep_scheme_kind_from_type; InProp,ind_dep_scheme_kind_from_type; - InSet,rec_dep_scheme_kind_from_type] + InSet,rec_dep_scheme_kind_from_type; + InSProp,sind_dep_scheme_kind_from_type] let nondep_kinds_from_type = [InType,rect_scheme_kind_from_type; InProp,ind_scheme_kind_from_type; - InSet,rec_scheme_kind_from_type] + InSet,rec_scheme_kind_from_type; + InSProp,sind_scheme_kind_from_type] let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in |