diff options
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index e16fcec7c..d912decff 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -73,7 +73,7 @@ let generalize_right mk typ c1 c2 = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in Refine.refine ~typecheck:false begin fun sigma -> - let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in + let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in (sigma, mkApp (x, [|c2|])) @@ -114,7 +114,7 @@ let idx = Id.of_string "x" let idy = Id.of_string "y" let mkGenDecideEqGoal rectype ops g = - let hypnames = pf_ids_of_hyps g in + let hypnames = pf_ids_set_of_hyps g in let xname = next_ident_away idx hypnames and yname = next_ident_away idy hypnames in (mkNamedProd xname rectype |