diff options
Diffstat (limited to 'toplevel/discharge.ml')
-rw-r--r-- | toplevel/discharge.ml | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 615730910..e24d5e74f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -7,22 +7,23 @@ (************************************************************************) open Names -open Errors +open CErrors open Util -open Context open Term open Vars -open Entries open Declarations open Cooking +open Entries +open Context.Rel.Declaration (********************************) (* Discharging mutual inductive *) -let detype_param = function - | (Name id,None,p) -> id, LocalAssum p - | (Name id,Some p,_) -> id, LocalDef p - | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable") +let detype_param = + function + | LocalAssum (Name id, p) -> id, LocalAssumEntry p + | LocalDef (Name id, p,_) -> id, LocalDefEntry p + | _ -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace @@ -37,8 +38,8 @@ let detype_param = function let abstract_inductive hyps nparams inds = let ntyp = List.length inds in - let nhyp = named_context_length hyps in - let args = instance_from_named_context (List.rev hyps) in + let nhyp = Context.Named.length hyps in + let args = Context.Named.to_instance (List.rev hyps) in let args = Array.of_list args in let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in let inds' = @@ -53,7 +54,7 @@ let abstract_inductive hyps nparams inds = (* To be sure to be the same as before, should probably be moved to process_inductive *) let params' = let (_,arity,_,_,_) = List.hd inds' in let (params,_) = decompose_prod_n_assum nparams' arity in - List.map detype_param params + List.map detype_param params in let ind'' = List.map @@ -100,7 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = Array.to_list mip.mind_consnames, Array.to_list lc)) mib.mind_packets in - let sechyps' = map_named_context (expmod_constr modlist) sechyps in + let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in @@ -115,5 +116,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs + mind_entry_universes = univs; } |