+ else
+ try
+ let l, r = meta_convertibility_aux ([], []) t1 t2 in
+ (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
+ true
+ with NotMetaConvertible ->
+ false
+;;
+
+
+let replace_metas (* context *) term =
+ let module C = Cic in
+ let rec aux = function
+ | C.Meta (i, c) ->
+(* let irl = *)
+(* CicMkImplicit.identity_relocation_list_for_metavariable context *)
+(* in *)
+(* if c = irl then *)
+(* C.Implicit (Some (`MetaIndex i)) *)
+(* else ( *)
+(* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
+(* (String.concat "\n" *)
+(* (List.map *)
+(* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
+(* C.Meta (i, c) *)
+(* ) *)
+ C.Implicit (Some (`MetaInfo (i, c)))
+ | C.Var (u, ens) -> C.Var (u, aux_ens ens)
+ | C.Const (u, ens) -> C.Const (u, aux_ens ens)
+ | C.Cast (s, t) -> C.Cast (aux s, aux t)
+ | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
+ | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
+ | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
+ | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
+ | C.MutCase (uri, i, s, t, l) ->
+ C.MutCase (uri, i, aux s, aux t, List.map aux l)
+ | C.Fix (i, il) ->
+ let il' =
+ List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
+ C.Fix (i, il')
+ | C.CoFix (i, il) ->
+ let il' =
+ List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
+ C.CoFix (i, il')
+ | t -> t
+ and aux_ens ens =
+ List.map (fun (u, t) -> (u, aux t)) ens
+ in
+ aux term
+;;
+
+
+let restore_metas (* context *) term =
+ let module C = Cic in
+ let rec aux = function
+ | C.Implicit (Some (`MetaInfo (i, c))) ->
+(* let c = *)
+(* CicMkImplicit.identity_relocation_list_for_metavariable context *)
+(* in *)
+(* C.Meta (i, c) *)
+(* let local_context:(C.term option) list = *)
+(* Marshal.from_string mc 0 *)
+(* in *)
+(* C.Meta (i, local_context) *)
+ C.Meta (i, c)
+ | C.Var (u, ens) -> C.Var (u, aux_ens ens)
+ | C.Const (u, ens) -> C.Const (u, aux_ens ens)
+ | C.Cast (s, t) -> C.Cast (aux s, aux t)
+ | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
+ | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
+ | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
+ | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
+ | C.MutCase (uri, i, s, t, l) ->
+ C.MutCase (uri, i, aux s, aux t, List.map aux l)
+ | C.Fix (i, il) ->
+ let il' =
+ List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
+ C.Fix (i, il')
+ | C.CoFix (i, il) ->
+ let il' =
+ List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
+ C.CoFix (i, il')
+ | t -> t
+ and aux_ens ens =
+ List.map (fun (u, t) -> (u, aux t)) ens
+ in
+ aux term
+;;
+
+
+let rec restore_subst (* context *) subst =
+ List.map
+ (fun (i, (c, t, ty)) ->
+ i, (c, restore_metas (* context *) t, ty))
+ subst
+;;
+
+
+exception MatchingFailure;;
+
+let matching metasenv context t1 t2 ugraph =
+ try
+ let subst, metasenv, ugraph =
+ CicUnification.fo_unif metasenv context t1 t2 ugraph
+ in
+ let t' = CicMetaSubst.apply_subst subst t1 in
+ if not (meta_convertibility t1 t') then
+ raise MatchingFailure
+ else
+ let metas = metas_of_term t1 in
+ let fix_subst = function
+ | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+ (j, (c, Cic.Meta (i, lc), ty))
+ | s -> s
+ in
+ let subst = List.map fix_subst subst in
+ subst, metasenv, ugraph
+ with e ->
+ raise MatchingFailure