+type substitution = (int * (Cic.context * Cic.term)) list
+
+(*
+let rec deref subst =
+ let third _,_,a = a in
+ function
+ Cic.Meta(n,l) as t ->
+ (try
+ deref subst
+ (CicSubstitution.lift_meta
+ l (third (CicUtil.lookup_subst n subst)))
+ with
+ CicUtil.Subst_not_found _ -> t)
+ | t -> t
+;;
+*)
+
+let lookup_subst = CicUtil.lookup_subst
+;;
+
+
+(* clean_up_meta take a metasenv and a term and make every local context
+of each occurrence of a metavariable consistent with its canonical context,
+with respect to the hidden hipothesis *)
+
+(*
+let clean_up_meta subst metasenv t =
+ let module C = Cic in
+ let rec aux t =
+ match t with
+ C.Rel _
+ | C.Sort _ -> t
+ | C.Implicit _ -> assert false
+ | C.Meta (n,l) as t ->
+ let cc =
+ (try
+ let (cc,_) = lookup_subst n subst in cc
+ with CicUtil.Subst_not_found _ ->
+ try
+ let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc
+ with CicUtil.Meta_not_found _ -> assert false) in
+ let l' =
+ (try
+ List.map2
+ (fun t1 t2 ->
+ match t1,t2 with
+ None , _ -> None
+ | _ , t -> t) cc l
+ with
+ Invalid_argument _ -> assert false) in
+ C.Meta (n, l')
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest)
+ | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest)
+ | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.Var (uri, exp_named_subst')
+ | C.Const (uri, exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.Const (uri, exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.MutInd (uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.MutConstruct (uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ C.MutCase (uri, tyno, aux out, aux te, List.map aux pl)
+ | C.Fix (i,fl) ->
+ let fl' =
+ List.map
+ (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl
+ in
+ C.Fix (i, fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl
+ in
+ C.CoFix (i, fl')
+ in
+ aux t *)