diff options
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r-- | printing/printmod.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index e0b1d55be..3973c2db6 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Context open Termops open Reduction @@ -90,7 +89,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -144,7 +143,7 @@ let print_record env mind mib = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in |