From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jul 2005 08:34:12 +0000 (+0000)
Subject: Some precisations on a few comments by Ferruccio.
X-Git-Tag: V_0_7_1~77
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f10830e4d9695ab51f8f7aefe9c61460a35597a;hp=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git

Some precisations on a few comments by Ferruccio.
---

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 76b733734..590b482c7 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -204,7 +204,6 @@ exception TwoDifferentSubtermsFound of int
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
-(* FG: METTERE I NOMI ANCHE QUI? *)
 let discriminate'_tac ~term =
  let discriminate'_tac ~term status = 
   let (proof, goal) = status in
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