X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FnegationTactics.ml;h=e4cd7389813df6c35cdea841187be0c57a255208;hb=0f10830e4d9695ab51f8f7aefe9c61460a35597a;hp=0e3c0c142180a9f5570233f4a03528780711224c;hpb=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index 0e3c0c142..e4cd73898 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -46,7 +46,7 @@ let absurd_tac ~term = ProofEngineTypes.mk_tactic (absurd_tac ~term) ;; -(* FG: METTERE I NOMI ANCHE QUI? *) +(* 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