diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index d4b756346..6b3b177aa 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Term +open Constr open Pp open Names open Environ @@ -149,7 +149,7 @@ let print_mutual_inductive env mind mib = let get_fields = let rec prodec_rec l subst c = - match kind_of_term c with + match kind c with | Prod (na,t,c) -> let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c |