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 f81fe99efcb0b31dae0bbcd2cdd2ddaea1aee856..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 
@@ -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 =