diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 68d4890fd..9b32f108c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -109,7 +109,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac let onNLastHyps n tac = onHyps (nLastHyps n) tac let afterHyp id gl = - fst (List.split_when (fun (hyp,_,_) -> id_eq hyp id) (pf_hyps gl)) + fst (List.split_when (fun (hyp,_,_) -> Id.equal hyp id) (pf_hyps gl)) (***************************************) (* Clause Tacticals *) @@ -249,7 +249,7 @@ let general_elim_then_using mk_elim let name_elim = match kind_of_term elim with | Const kn -> string_of_con kn - | Var id -> string_of_id id + | Var id -> Id.to_string id | _ -> "\b" in error ("The elimination combinator " ^ name_elim ^ " is unknown.") |