X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.ml;h=1e650cc7a047ca08e2d336c6300bb5ba2b652982;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=f81fe99efcb0b31dae0bbcd2cdd2ddaea1aee856;hpb=7b4d519aefac94afb371a7e4da94779b40bf8608;p=helm.git

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index f81fe99ef..1e650cc7a 100644
--- a/helm/software/components/tactics/setoids.ml
+++ b/helm/software/components/tactics/setoids.ml
@@ -1816,7 +1816,7 @@ let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) =
 
 let setoid_reflexivity_tac =
  let tac ((proof,goal) as status) =
-  let (_,metasenv,_,_) = proof in
+  let (_,metasenv,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    try
     let relation_class =