diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 2 | ||||
| -rw-r--r-- | parsing/search.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 7df78fe61c..bbbbc31800 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -507,7 +507,7 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_mutual sp | ConstructRef cstr -> - let ty = Inductive.type_of_constructor env cstr in + let ty = Inductiveops.type_of_constructor env cstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> let (_,c,ty) = lookup_named id env in diff --git a/parsing/search.ml b/parsing/search.ml index de7e497b18..8435f4b4bb 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -34,7 +34,7 @@ open Nametab let print_constructors indsp fn env nconstr = for i = 1 to nconstr do - fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i)) + fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i)) done let rec head_const c = match kind_of_term c with |