diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 98686fb1b..56106928e 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -15,7 +15,6 @@ open Util open Pp open Term open Vars -open Context open Termops open Declarations open Names @@ -103,7 +102,7 @@ let mkFullInd (ind,u) n = context_chop (nparams-nparrec) mib.mind_params_ctxt in if nparrec > 0 then mkApp (mkIndU (ind,u), - Array.of_list(extended_rel_list (nparrec+n) lnamesparrec)) + Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec)) else mkIndU (ind,u) let check_bool_is_defined () = @@ -138,7 +137,7 @@ let build_beq_scheme mode kn = | Name s -> Id.of_string ("eq_"^(Id.to_string s)) | Anonymous -> Id.of_string "eq_A" in - let ext_rel_list = extended_rel_list 0 lnamesparrec in + let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in let lift_cnt = ref 0 in let eqs_typ = List.map (fun aa -> let a = lift !lift_cnt aa in @@ -234,7 +233,7 @@ let build_beq_scheme mode kn = Cn => match Y with ... end |] part *) let ci = make_case_info env (fst ind) MatchStyle in let constrs n = get_constructors env (make_ind_family (ind, - extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in + Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in |