diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c540a4a1f..d0dca036e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -194,7 +194,6 @@ let build_dependent_constructor cs = let build_dependent_inductive env ((ind, params) as indf) = let arsign,_ = get_arity env indf in - let (mib,mip) = Inductive.lookup_mind_specif env ind in let nrealargs = List.length arsign in applist (mkInd ind, |