change into QuestionMark default

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7b4b2d42f8..7be05ea600 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -99,9 +99,9 @@ open Program
 
 let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
   let src = Loc.tag ?loc (Evar_kinds.QuestionMark {
+      Evar_kinds.default_question_mark with
       Evar_kinds.qm_obligation=Evar_kinds.Define opaque;
       Evar_kinds.qm_name=na;
-      Evar_kinds.qm_record_field=None;
   }) in
   let evd, v = Evarutil.new_evar env !evdref ~src c in
   evdref := evd;