Make eq_pattern_test/eq_test work up to the equivalence of primitive

projections with their eta-expanded constant form.

1 files changed, 5 insertions, 4 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 08cf95432a..841116a0b4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2204,17 +2204,18 @@ let generalized_name c t ids cl = function
    [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai]
    but only those at [occs] in [T] *)
 
-let generalize_goal_gen ids i ((occs,c,b),na) t (cl,evd) =
+let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) =
   let decls,cl = decompose_prod_n_assum i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in
-  let cl',evd' = subst_closed_term_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in
+  let cl',evd' = subst_closed_term_occ env evd occs c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name c t ids cl' na in
     mkProd_or_LetIn (na,b,t) cl', evd'
 
 let generalize_goal gl i ((occs,c,b),na as o) cl =
   let t = pf_type_of gl c in
-    generalize_goal_gen (pf_ids_of_hyps gl) i o t cl
+  let env = pf_env gl in
+    generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl
 
 let generalize_dep ?(with_let=false) c gl =
   let env = pf_env gl in
@@ -2275,7 +2276,7 @@ let new_generalize_gen_let lconstr =
 	(fun i ((_,c,b),_ as o) (cl, args) ->
 	  let t = Tacmach.New.pf_type_of gl c in
 	  let args = if Option.is_empty b then c :: args else args in
-	    generalize_goal_gen ids i o t cl, args)
+	    generalize_goal_gen env ids i o t cl, args)
 	0 lconstr ((concl, sigma), [])
     in
       Proofview.V82.tclEVARS sigma <*>