+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+ let just =
+ match just with
+ `Auto params ->
+ let params =
+ if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
+ ("paramodulation","1")::params
+ else params in
+ let params =
+ if not (List.exists (fun (k,_) -> k = "timeout") params) then
+ ("timeout","3")::params
+ else params
+ in
+ Tactics.auto ~dbd ~params ~universe
+ | `Term just -> Tactics.apply just
+ in
+ let plhs,prhs,prepare =
+ match lhs with
+ None ->
+ let plhs,prhs =
+ match gty with
+ Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
+ | _ -> assert false
+ in
+ plhs,prhs,
+ (fun continuation ->
+ ProofEngineTypes.apply_tactic continuation status)
+ | Some (None,lhs) ->
+ let plhs,prhs =
+ match gty with
+ Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
+ | _ -> assert false
+ in
+ (*CSC: manca check plhs convertibile con lhs *)
+ plhs,prhs,
+ (fun continuation ->
+ ProofEngineTypes.apply_tactic continuation status)
+ | Some (Some name,lhs) ->
+ let newmeta = CicMkImplicit.new_meta metasenv [] in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let plhs = lhs in
+ let prhs = Cic.Meta(newmeta,irl) in
+ plhs,prhs,
+ (fun continuation ->
+ let metasenv = (newmeta, context, ty)::metasenv in
+ let mk_fresh_name_callback =
+ fun metasenv context _ ~typ ->
+ FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
+ (Cic.Name name) ~typ
+ in
+ let proof = curi,metasenv,proofbo,proofty in
+ let proof,goals =
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens
+ ~start:(Tactics.cut ~mk_fresh_name_callback
+ (Cic.Appl [eq ; ty ; lhs ; prhs]))
+ ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
+ in
+ let goals =
+ match goals with
+ [g1;g2] -> [g2;newmeta;g1]
+ | _ -> assert false
+ in
+ proof,goals)