diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 2181eb25af..4239fc8bc0 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -352,7 +352,7 @@ let dest_nf_eq env sigma t = match EConstr.kind sigma t with | App (r, [| t; x; y |]) -> let open Reductionops in let eq = Coqlib.lib_ref "core.eq.type" in - if EConstr.is_global sigma eq r then + if isRefX sigma eq r then (t, whd_all env sigma x, whd_all env sigma y) else user_err Pp.(str "Not an equality.") | _ -> |