Dead code removed.

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 1df9128c168ca1fad6e9213be480e0c45e78a7d7..5f6dade405eeb62df65c1c82a9a1c1ced6f46401 100644 (file)
--- 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