+let compare_statuses ~past ~present =
+ let _,_,past,_,_ = past#obj in
+ let _,_,present,_,_ = present#obj in
+ List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
+ List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
+;;
+
+(* paramodulation has only an implicit knoweledge of the symmetry of equality;
+ hence it is in trouble in proving (a = b) = (b = a) *)
+let try_sym tac status g =
+ (* put the right uri *)
+ let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in
+ let _,_,metasenv,subst,_ = status#obj in
+ let _, context, gty = List.assoc g metasenv in
+ let is_eq =
+ NCicParamod.is_equation status metasenv subst context gty
+ in
+ if is_eq then
+ try tac status g
+ with Error _ ->
+ let new_status = instantiate_with_ast status g ("",0,sym_eq) in
+ let go, _ = compare_statuses ~past:status ~present:new_status in
+ assert (List.length go = 1);
+ let ng = List.hd go in
+ tac new_status ng
+ else tac status g
+;;
+