+let rec is_meta_closed =
+ function
+ Cic.Rel _ -> true
+ | Cic.Meta _ -> false
+ | Cic.Sort _ -> true
+ | Cic.Implicit _ -> assert false
+ | Cic.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty
+ | Cic.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest
+ | Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
+ | Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest
+ | Cic.Appl l ->
+ List.fold_right (fun x i -> i && is_meta_closed x) l true
+ | Cic.Var (_,exp_named_subst)
+ | Cic.Const (_,exp_named_subst)
+ | Cic.MutInd (_,_,exp_named_subst)
+ | Cic.MutConstruct (_,_,_,exp_named_subst) ->
+ List.fold_right (fun (_,x) i -> i && is_meta_closed x)
+ exp_named_subst true
+ | Cic.MutCase (_,_,out,te,pl) ->
+ is_meta_closed out && is_meta_closed te &&
+ List.fold_right (fun x i -> i && is_meta_closed x) pl true
+ | Cic.Fix (_,fl) ->
+ List.fold_right
+ (fun (_,_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo
+ ) fl true
+ | Cic.CoFix (_,fl) ->
+ List.fold_right
+ (fun (_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo
+ ) fl true
+;;