|_->assert false)(* match u *)
| Cic.MutInd (u,i,o) ->
(match UriManager.string_of_uri u with
- "cic:/Coq/Init/Logic_Type/eqT.con" ->
+ "cic:/Coq/Init/Logic_Type/eqT.ind" ->
let t0= arg1 in
let arg1= arg2 in
let arg2= List.hd(List.tl (List.tl next)) in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+debug("my_cut di "^CicPp.ppterm c^"\n");
+
+
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
(* !!!!! fix !!!!!!!!!! *)
let contradiction_tac ~status:(proof,goal)=
Tacticals.then_
- ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
+ ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
~continuation:(Tacticals.then_
~start:(Ring.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
in
tac:=(Tacticals.thens
~start:(my_cut ~term:ineq)
- ~continuations:[Tacticals.then_
+ ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)Tacticals.then_
~start:(fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal)
~continuation:(Tacticals.thens
~start:(
fun ~status ->
+ debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
~status
in
)
~continuation:(*PORTINGTacticals.id_tac*)tac2]))
;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
- tac:=(Tacticals.thens
+ (*tac:=(Tacticals.thens
~start:(PrimitiveTactics.cut_tac ~term:_False)
~continuations:[Tacticals.then_
~start:(PrimitiveTactics.intros_tac ~name:"??")
~continuation:contradiction_tac
- ;!tac])
+ ;!tac])*)
+ tac:=!tac
|_-> assert false)(*match (!lutil) *)