X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Findexing.ml;h=4eed05790fd777060db24f2d757e9b97cfd69425;hb=9262517c80e17d46b9bf9931dc879ac653a633e9;hp=8ece33e35251e9e642a95086617eea29fadf9d5b;hpb=5886d890afe8fbb3b6bae0fffdfa657b894cae3f;p=helm.git

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