X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FnegationTactics.ml;h=e4cd7389813df6c35cdea841187be0c57a255208;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;hp=ee76921b23ff0729649bed6030e1fedeffae67a6;hpb=a9af753c66a80cb4f50f32e63272f3830cba306c;p=helm.git

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index ee76921b2..e4cd73898 100644
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -46,6 +46,7 @@ let absurd_tac ~term =
    ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
+(* FG: METTERE I NOMI ANCHE QUI? CSC: in teoria si', per la intros*)
 let contradiction_tac =
  let contradiction_tac status =
   let module C = Cic in
@@ -60,8 +61,7 @@ let contradiction_tac =
 	 T.then_
            ~start:
              (EliminationTactics.elim_type_tac 
-                ~term:
-                  (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+                (C.MutInd (LibraryObjects.false_URI (), 0, [])))
            ~continuation: VariousTactics.assumption_tac))
     status
    with