From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jan 2006 15:39:49 +0000 (+0000)
Subject: Dead code removed.
X-Git-Tag: make_still_working~7831
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06018c33636305c9b2b4f430091de2c3eb51e91a;p=helm.git

Dead code removed.
---

diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml
index 6b563fe6a..5e442657d 100644
--- a/helm/ocaml/tactics/inversion.ml
+++ b/helm/ocaml/tactics/inversion.ml
@@ -165,7 +165,6 @@ let inversion_tac ~term =
  let inversion_tac ~term (proof, goal) =
  let (_,metasenv,_,_) = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let (newproof, metasenv') = PEH.subst_meta_in_proof proof metano term [] in
  let uri_of_eq = HelmLibraryObjects.Logic.eq_URI in
 
  (* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che 
diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml
index 8ece33e35..4eed05790 100644
--- a/helm/ocaml/tactics/paramodulation/indexing.ml
+++ b/helm/ocaml/tactics/paramodulation/indexing.ml
@@ -1010,7 +1010,7 @@ let rec demodulation_theorem newmeta env table theorem =
       newmeta, theorem
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = 
+let demodulate_tac ~dbd ~pattern (proof,goal) = 
   let module I = Inference in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml
index 6946df1a2..0514ed503 100644
--- a/helm/ocaml/tactics/paramodulation/saturation.ml
+++ b/helm/ocaml/tactics/paramodulation/saturation.ml
@@ -2218,7 +2218,7 @@ let retrieve_and_print dbd term metasenv ugraph =
 	      | Some e -> (u, (snd e))::others_simpl
 	  ) 
   in
-  let equalities =
+  let _equalities =
     match equalities with
       | [] -> []
       | hd::tl ->