From 0f10830e4d9695ab51f8f7aefe9c61460a35597a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 6 Jul 2005 08:34:12 +0000 Subject: [PATCH] Some precisations on a few comments by Ferruccio. --- helm/ocaml/tactics/discriminationTactics.ml | 1 - helm/ocaml/tactics/negationTactics.ml | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) 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 -- 2.39.2