diff options
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b7c471f4a..ac54e44cc 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -71,7 +71,7 @@ let isVarf f x = let ident_global_exist id = try let ans = CRef (Libnames.Ident (Loc.ghost,id)) in - let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in + let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when Errors.noncritical e -> false |