Dead code removed.

diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml
index 6b563fe6a0fae9451f2e7a5a0f2da9c85e54910e..5e442657d26c52578e7f32b67d5f1e79acb184d8 100644 (file)
--- 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 8ece33e35251e9e642a95086617eea29fadf9d5b..4eed05790fd777060db24f2d757e9b97cfd69425 100644 (file)
--- 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 6946df1a2be57257dfa53cabe519830f27960381..0514ed5033f732389b8221cf903a5ab10118995f 100644 (file)
--- 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 ->