-(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
- di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
- parametri della equality_replace vengono passati al contrario? Oppure la
- tattica usa i parametri al contrario?
- CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac
- ~continuations:[Tacticals.then_
- ~start:(
- fun ~status:(proof,goal as status) ->
- debug("ECCOCI\n");
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=
- goal) metasenv in
- debug("ty = "^CicPp.ppterm ty^"\n");
- let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
- ~status in
- debug("fine ECCOCI\n");
- r)
- ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
-*)