X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.ml;h=c8ca1631763b7248addc55785a2651c6635faeee;hb=d120acefa62d997341a84ec54cb1532e223dd661;hp=1e650cc7a047ca08e2d336c6300bb5ba2b652982;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index 1e650cc7a..c8ca16317 100644
--- a/helm/software/components/tactics/setoids.ml
+++ b/helm/software/components/tactics/setoids.ml
@@ -1745,7 +1745,7 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
    let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in 
    (* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels, 
       Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
-   Cic.LetIn (Cic.Anonymous,c2,hyp) 
+   Cic.LetIn (Cic.Anonymous,c2,assert false,hyp) 
  in 
  let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in 
  let oppdir = opposite_direction direction in 
@@ -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 =