1) variables occurring only in proofs anre not relocated

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index a2e6eda07443be5d7e644136861f7520e14d3121..dd2d0a422e1fee06df487e362a3966e9b4f57c19 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -1057,7 +1057,7 @@ let superposition_left (metasenv, context, ugraph) table goal =
 (** demodulation, when the target is a goal *)
 let rec demodulation_goal env table goal =
   let goalproof,menv,_,_,left,right = open_goal goal in
-  let metasenv, context, ugraph = env in
+  let _, context, ugraph = env in
 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
   let do_right () = 
       let resright = demodulation_aux menv context ugraph table 0 right in