Very experimental commit: the type of the source is now required in LetIns

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

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index 7d0e958cc40ce059e980a1b3d3a467eb2633756a..c8ca1631763b7248addc55785a2651c6635faeee 100644 (file)
--- 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