diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 3ea9538f3..e33dd2e5e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1003,7 +1003,7 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> - let e = next_ident_away eq_baseid (ids_of_context env) in + let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in let discriminator = try @@ -1371,7 +1371,7 @@ let simplify_args env sigma t = | _ -> t let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = - let e = next_ident_away eq_baseid (ids_of_context env) in + let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (e,t)) env in let evdref = ref sigma in let filter (cpath, t1', t2') = |