+(* debug
+let matching metasenv1 metasenv2 context t1 t2 ugraph =
+ let rc1 =
+ try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph)
+ with MatchingFailure -> None
+ in
+ let rc2 =
+ try
+ Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph)
+ with MatchingFailure -> None
+ in
+ match rc1,rc2 with
+ | Some (s,m,g) , None ->
+ prerr_endline (CicPp.ppterm t1);
+ prerr_endline (CicPp.ppterm t2);
+ prerr_endline "SOLO NOI";
+ prerr_endline (CicMetaSubst.ppsubst s);
+ s,m,g
+ | None , Some _ ->
+ prerr_endline (CicPp.ppterm t1);
+ prerr_endline (CicPp.ppterm t2);
+ prerr_endline "SOLO LUI";
+ assert false
+ | None, None -> raise MatchingFailure
+ | Some (s,m,g), Some (s',m',g') ->
+ let s = List.sort (fun (i,_) (j,_) -> i - j) s in
+ let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in
+ if s <> s' then
+ begin
+ prerr_endline (CicMetaSubst.ppsubst s);
+ prerr_endline (CicMetaSubst.ppsubst s');
+ prerr_endline (CicPp.ppterm t1);
+ prerr_endline (CicPp.ppterm t2);
+ end;
+ s,m,g
+*)
+let matching = matching1;;
+