- if c = Utils.Incomparable then
- begin
- let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
- let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
- (* prerr_endline "incomparable";
- prerr_endline (string_of_int (List.length expansionsl));
- prerr_endline (string_of_int (List.length expansionsr));
- *)
- List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
- @
- List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
- end
- else
- match c with
- | Utils.Gt -> (* prerr_endline "GT"; *)
- let big,small,possmall = l,r,Utils.Right in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map
- (build_newgoal context goal possmall Equality.SuperpositionLeft)
- expansions
- | Utils.Lt -> (* prerr_endline "LT"; *)
- let big,small,possmall = r,l,Utils.Left in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map
- (build_newgoal context goal possmall Equality.SuperpositionLeft)
- expansions
- | Utils.Eq -> []
- | _ ->
- prerr_endline
- ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
- assert false
+ let newgoals =
+ if c = Utils.Incomparable then
+ begin
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ (* prerr_endline "incomparable";
+ prerr_endline (string_of_int (List.length expansionsl));
+ prerr_endline (string_of_int (List.length expansionsr));
+ *)
+ List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+ end
+ else
+ match c with
+ | Utils.Gt -> (* prerr_endline "GT"; *)
+ let big,small,possmall = l,r,Utils.Right in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Lt -> (* prerr_endline "LT"; *)
+ let big,small,possmall = r,l,Utils.Left in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Eq -> []
+ | _ ->
+ prerr_endline
+ ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+ assert false
+ in
+ (* rinfresco le meta *)
+ List.fold_right
+ (fun g (max,acc) ->
+ let max,g = Equality.fix_metas_goal max g in max,g::acc)
+ newgoals (maxmeta,[])