(fun _ metasenv ugraph -> ty,metasenv,ugraph))
;;
-let by_term_we_proved ~dbd t ty id ty' =
+let by_term_we_proved ~dbd ~universe t ty id ty' =
let just =
match t with
- None -> Tactics.auto ~dbd ~params:[] (* da sistemare *) ~universe:Universe.empty
+ None -> Tactics.auto ~dbd ~params:[] ~universe
| Some t -> Tactics.apply t
in
match id with
~continuations:[ continuation ; just ]
;;
-let bydone ~dbd t =
+let bydone ~dbd ~universe t =
let just =
match t with
- None -> Tactics.auto ~dbd ~params:[] ~universe:Universe.empty
+ None -> Tactics.auto ~dbd ~params:[] ~universe
| Some t -> Tactics.apply t
in
just
let andelim = existselim;;
-let rewritingstep ~dbd lhs rhs just conclude =
+let rewritingstep ~dbd ~universe lhs rhs just conclude =
let aux ((proof,goal) as status) =
let (curi,metasenv,proofbo,proofty) = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
let just =
match just with
- None ->
- Tactics.auto ~dbd
- ~params:["paramodulation","1"; "timeout","3"] ~universe:Universe.empty
- | Some just -> Tactics.apply just
+ `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
match lhs with
None ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- just]) status
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]) status
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- just]
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]
]) status)
| Some lhs ->
match conclude with
let thesisbecomes t =
let ty = None in
- (*BUG here: missing check on t *)
match ty with
- None -> Tacticals.id_tac
+ None ->
+ Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
+ (fun _ metasenv ugraph -> t,metasenv,ugraph)
| Some ty ->
+ (*BUG here: missing check on t *)
Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
(fun _ metasenv ugraph -> ty,metasenv,ugraph)
;;