X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.ml;h=c8ca1631763b7248addc55785a2651c6635faeee;hb=35e102fec6bad146fee425f299a93520e657e7c2;hp=7d0e958cc40ce059e980a1b3d3a467eb2633756a;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index 7d0e958cc..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