diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index edd3e498d..e42a732d3 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -29,7 +29,7 @@ let pop_kn kn = let (mp,dir,l) = Names.repr_kn kn in Names.make_kn mp (pop_dirpath dir) l -let pop_con con = +let pop_con con = let (mp,dir,l) = Names.repr_con con in Names.make_con mp (pop_dirpath dir) l @@ -47,9 +47,9 @@ let share r (cstl,knl) = with Not_found -> let f,l = match r with - | IndRef (kn,i) -> + | IndRef (kn,i) -> mkInd (pop_kn kn,i), KNmap.find kn knl - | ConstructRef ((kn,i),j) -> + | ConstructRef ((kn,i),j) -> mkConstruct ((pop_kn kn,i),j), KNmap.find kn knl | ConstRef cst -> mkConst (pop_con cst), Cmap.find cst cstl in @@ -60,7 +60,7 @@ let share r (cstl,knl) = let update_case_info ci modlist = try - let ind, n = + let ind, n = match kind_of_term (share (IndRef ci.ci_ind) modlist) with | App (f,l) -> (destInd f, Array.length l) | Ind ind -> ind, 0 @@ -80,19 +80,19 @@ let expmod_constr modlist c = | Ind ind -> (try share (IndRef ind) modlist - with + with | Not_found -> map_constr substrec c) - + | Construct cstr -> (try share (ConstructRef cstr) modlist - with + with | Not_found -> map_constr substrec c) - + | Const cst -> (try share (ConstRef cst) modlist - with + with | Not_found -> map_constr substrec c) | _ -> map_constr substrec c @@ -112,7 +112,7 @@ type recipe = { d_abstract : named_context; d_modlist : work_list } -let on_body f = +let on_body f = Option.map (fun c -> Declarations.from_val (f (Declarations.force c))) let cook_constant env r = @@ -120,7 +120,7 @@ let cook_constant env r = let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in let body = on_body (fun c -> - abstract_constant_body (expmod_constr r.d_modlist c) hyps) + abstract_constant_body (expmod_constr r.d_modlist c) hyps) cb.const_body in let typ = match cb.const_type with | NonPolymorphicType t -> |