Some precisations on a few comments by Ferruccio.

[helm.git] / helm / ocaml / tactics / negationTactics.ml

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 0e3c0c142180a9f5570233f4a03528780711224c..e4cd7389813df6c35cdea841187be0c57a255208 100644 (file)
--- 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