4 files changed, 43 insertions, 10 deletions

diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out
index 7c80a6065f..28beee90b2 100644
--- a/test-suite/output/RecordMissingField.out
+++ b/test-suite/output/RecordMissingField.out
@@ -1,4 +1,16 @@
-File "stdin", line 8, characters 5-22:
-Error: Cannot infer field y2p of record point2d in environment:
-p : point2d
-
+The command has indeed failed with message:
+The following term contains unresolved implicit arguments:
+  (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |})
+More precisely: 
+- ?y2p: Cannot infer field y2p of record point2d in environment:
+  p : point2d
+The command has indeed failed with message:
+The following term contains unresolved implicit arguments:
+  (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |})
+More precisely: 
+- ?n: Cannot infer this placeholder of type "nat" in
+  environment:
+  p : point2d
+  n : nat
+- ?y2p: Cannot infer field y2p of record point2d in environment:
+  p : point2d
diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v
index 84f1748fa0..8ca721564b 100644
--- a/test-suite/output/RecordMissingField.v
+++ b/test-suite/output/RecordMissingField.v
@@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **)
 
 Record point2d := mkPoint { x2p: nat; y2p: nat }.
 
-
-Definition increment_x (p: point2d) : point2d :=
+Fail Definition increment_x (p: point2d) : point2d :=
   {| x2p := x2p p + 1; |}.
+
+(* Here there is also an unresolved implicit, which should give an
+   understadable error as well *)
+Fail Definition increment_x (p: point2d) : point2d :=
+  {| x2p := x2p p + (fun n => _) 1; |}.
diff --git a/vernac/declare.ml b/vernac/declare.ml
index eedbee852b..66537c2978 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -642,14 +642,32 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   dref
 
 (* Preparing proof entries *)
+let error_unresolved_evars env sigma t evars =
+  let pr_unresolved_evar e =
+    hov 2 (str"- " ++ Printer.pr_existential_key sigma e ++  str ": " ++
+      Himsg.explain_pretype_error env sigma
+        (Pretype_errors.UnsolvableImplicit (e,None)))
+  in
+  CErrors.user_err (hov 0 begin
+    str "The following term contains unresolved implicit arguments:"++ fnl () ++
+    str "  " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++
+    str "More precisely: " ++ fnl () ++
+    v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements evars))
+  end)
+
+let check_evars_are_solved env sigma t =
+  let t = EConstr.of_constr t in
+  let evars = Evarutil.undefined_evars_of_term sigma t in
+  if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
 
 let prepare_definition ~info ~opaque ~body ~typ sigma =
   let { Info.poly; udecl; inline; _ } = info in
   let env = Global.env () in
-  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
       sigma (fun nf -> nf body, Option.map nf typ)
   in
+  Option.iter (check_evars_are_solved env sigma) types;
+  check_evars_are_solved env sigma body;
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   let entry = definition_entry ~opaque ~inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index c5a8afbad5..3001d0d206 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -117,8 +117,7 @@ end
    normalized w.r.t. the passed [evar_map] [sigma]. Universes should
    be handled properly, including minimization and restriction. Note
    that [sigma] is checked for unresolved evars, thus you should be
-   careful not to submit open terms or evar maps with stale,
-   unresolved existentials *)
+   careful not to submit open terms *)
 val declare_definition
   :  info:Info.t
   -> cinfo:EConstr.t option CInfo.t