diff options
Diffstat (limited to 'contrib/xml/doubleTypeInference.ml')
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 728c7ac9a7..d4093f002c 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -124,10 +124,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types = E.make_judge cstr (E.constant_type env c) | T.Ind ind -> - E.make_judge cstr (Inductive.type_of_inductive env ind) + E.make_judge cstr (Inductiveops.type_of_inductive env ind) | T.Construct cstruct -> - E.make_judge cstr (Inductive.type_of_constructor env cstruct) + E.make_judge cstr (Inductiveops.type_of_constructor env cstruct) | T.Case (ci,p,c,lf) -> let expectedtype = |