- (CicMetaSubst.apply_subst subst' t,
- CicMetaSubst.apply_subst subst' ty,
- CicMetaSubst.apply_subst_metasenv subst' metasenv')
+ let substituted_t = CicMetaSubst.apply_subst subst' t in
+ let substituted_ty = CicMetaSubst.apply_subst subst' ty in
+ let substituted_metasenv =
+ CicMetaSubst.apply_subst_metasenv subst' metasenv'
+ in
+ let cleaned_t =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+ let cleaned_ty =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+ let cleaned_metasenv =
+ List.map
+ (function (n,context,ty) ->
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
+ let context' =
+ List.map
+ (function
+ None -> None
+ | Some (n, Cic.Decl t) ->
+ Some (n,
+ Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
+ | Some (n, Cic.Def (bo,ty)) ->
+ let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
+ let ty' =
+ match ty with
+ None -> None
+ | Some ty ->
+ Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ in
+ Some (n, Cic.Def (bo',ty'))
+ ) context
+ in
+ (n,context',ty')
+ ) substituted_metasenv
+ in
+ (cleaned_t,cleaned_ty,cleaned_metasenv)
+