diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 12:34:30 +0100 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 12:34:30 +0100 |
commit | 78bad016e389cd78635d40281bfefd7136733b7e (patch) | |
tree | 51f90da34d2444734868d7954412ac08ddc0f5c6 /printing/printmod.ml | |
parent | f8eb2ed4ddbe2199187696f51c42734014f4d9d0 (diff) | |
parent | 9d991d36c07efbb6428e277573bd43f6d56788fc (diff) |
merge
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 |