diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0fa573b9a6..ea222397a8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -269,10 +269,6 @@ let allowed_sorts env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_kelim -let projection_nparams_env _ p = Projection.npars p - -let projection_nparams p = Projection.npars p - let has_dependent_elim mib = match mib.mind_record with | PrimRecord _ -> mib.mind_finite == BiFinite |