added a (for the moment) dummy field _subst to ProofengineTypes.proof.

[helm.git] / components / tactics / setoids.ml

diff --git a/components/tactics/setoids.ml b/components/tactics/setoids.ml
index 1e650cc7a047ca08e2d336c6300bb5ba2b652982..7d0e958cc40ce059e980a1b3d3a467eb2633756a 100644 (file)
--- a/components/tactics/setoids.ml
+++ b/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,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    try
     let relation_class =