From: Claudio Sacerdoti Coen 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