diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 28 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 11 |
2 files changed, 19 insertions, 20 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 3da1ab7439..0ace11839e 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -69,19 +69,23 @@ let rename_arguments local r names = let arguments_names r = GlobRef.Map.find r !name_table -let rec rename_prod c = function - | [] -> c - | (Name _ as n) :: tl -> - (match kind_of_type c with - | ProdType (_, s, t) -> mkProd (n, s, rename_prod t tl) - | _ -> c) - | _ :: tl -> - match kind_of_type c with - | ProdType (n, s, t) -> mkProd (n, s, rename_prod t tl) - | _ -> c - let rename_type ty ref = - try rename_prod ty (arguments_names ref) + let name_override old_name override = + match override with + | Name _ as x -> x + | Anonymous -> old_name in + let rec rename_type_aux c = function + | [] -> c + | rename :: rest as renamings -> + match kind_of_type c with + | ProdType (old, s, t) -> + mkProd (name_override old rename, s, rename_type_aux t rest) + | LetInType(old, s, b, t) -> + mkLetIn (old ,s, b, rename_type_aux t renamings) + | CastType (t,_) -> rename_type_aux t renamings + | SortType _ -> c + | AtomicType _ -> c in + try rename_type_aux ty (arguments_names ref) with Not_found -> ty let rename_type_of_constant env c = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e6e1530e36..ed28cc7725 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option { (* Functions to deal with impossible cases *) (*******************************************) let impossible_default_case env = - let type_of_id = - let open Names.GlobRef in - match Coqlib.lib_ref "core.IDProp.type" with - | ConstRef c -> c - | VarRef _ | IndRef _ | ConstructRef _ -> assert false - in + let type_of_id = Coqlib.lib_ref "core.IDProp.type" in let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in - let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (type_of_id, u), ctx) + let (_, u) = Constr.destRef c in + Some (c, Constr.mkRef (type_of_id, u), ctx) let coq_unit_judge = let open Environ in |