diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/indrec.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/indrec.ml b/library/indrec.ml index b764f6cf7..3b02d092c 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -438,7 +438,7 @@ let type_mutind_rec env sigma indspec pt p c = let type_rec_branches recursive env sigma ct pt p c = try - let indspec = try_mutind_of env sigma ct in + let indspec = find_inductive env sigma ct in if recursive then type_mutind_rec env sigma indspec pt p c else |