+ let params' =
+ if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
+ ("paramodulation","1")::params
+ else params
+ in
+ if params = params' then
+ Tactics.auto ~dbd ~params ~universe
+ else
+ Tacticals.first
+ [Tactics.auto ~dbd ~params ~universe ;
+ Tactics.auto ~dbd ~params:params' ~universe]
+ | `Term just ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context just
+ CicUniv.empty_ugraph
+ in
+ Tactics.solve_rewrite
+ ~universe:(Universe.index Universe.empty
+ (Universe.key ty) just) ~steps:1 ()
+ (* Tactics.apply just *)
+ | `Proof ->
+ Tacticals.id_tac