diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 708788ab8..9451b0f86 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1051,7 +1051,7 @@ let contextually byhead occs f env sigma t = let match_constr_evaluable_ref sigma c evref = match EConstr.kind sigma c, evref with | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u - | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty + | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None let substlin env sigma evalref n (nowhere_except_in,locs) c = |