diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 452639170e..041187d84f 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -23,7 +23,7 @@ open Reductionops let type_of_inductive env ind = let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif (* Return type as quoted by the user *) let type_of_constructor env cstr = |