1 let nparamod metasenv subst context t =
3 let metasenv = metasenv
8 let module B = NCicBlob.NCicBlob(C) in
9 let module Pp = Pp.Pp (B) in
10 let res,vars = B.embed t in
11 let module FU = Founif.Founif(B) in
12 let test_unification vars = function
13 | Terms.Node [_; _; lhs; rhs] ->
14 prerr_endline "Unification test :";
15 prerr_endline (Pp.pp_foterm lhs);
16 prerr_endline (Pp.pp_foterm rhs);
17 FU.unification vars [] lhs rhs
20 let subst,vars = test_unification vars res in
21 prerr_endline "Result :";
22 prerr_endline (Pp.pp_foterm res);
23 prerr_endline "Substitution :";
24 prerr_endline (Pp.pp_substitution subst)