From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Jan 2003 18:40:46 +0000 (+0000)
Subject: Dead code removed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abe5665c13b45e51d972c97ad9005ecdc20d206a;p=helm.git

Dead code removed.
---

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 1df9128c1..5f6dade40 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -48,24 +48,6 @@ let assumption_tac ~status:((proof,goal) as status) =
      in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
 ;;
 
-(* Questa invece era in fourierR.ml 
-let assumption_tac ~status:(proof,goal)=
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-  let num = ref 0 in
-  let tac_list = List.map
-        ( fun x -> num := !num + 1;
-                match x with
-                  Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
-                  | _ -> ("fake",tcl_fail 1)
-        )
-        context
-  in
-  Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
-;;
-*)
-
-
 (* ANCORA DA DEBUGGARE *)
 
 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda