Merge PR #8852: Use the obligation evar flag

7 files changed, 31 insertions, 18 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 3a77a2b440..b3848e1b5b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -483,6 +483,8 @@ let is_typeclass_evar evd evk =
   let flags = evd.evar_flags in
   Evar.Set.mem evk flags.typeclass_evars
 
+let get_obligation_evars evd = evd.evar_flags.obligation_evars
+
 let set_obligation_evar evd evk =
   let flags = evd.evar_flags in
   let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
diff --git a/engine/evd.mli b/engine/evd.mli
index b0e3c2b869..be54bebcd7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -262,6 +262,9 @@ val get_typeclass_evars : evar_map -> Evar.Set.t
 val is_typeclass_evar : evar_map -> Evar.t -> bool
 (** Is the evar declared resolvable for typeclass resolution *)
 
+val get_obligation_evars : evar_map -> Evar.Set.t
+(** The set of obligation evars *)
+
 val set_obligation_evar : evar_map -> Evar.t -> evar_map
 (** Declare an evar as an obligation *)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index f720e5195d..181efa0ade 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -366,12 +366,18 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
     else
       str "TYPECLASSES:" ++ brk (0, 1) ++
       prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
+  and obligations =
+    let evars = Evd.get_obligation_evars sigma in
+    if Evar.Set.is_empty evars then mt ()
+    else
+      str "OBLIGATIONS:" ++ brk (0, 1) ++
+      prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
   in
-  evs ++ svs ++ cstrs ++ typeclasses ++ metas
+  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas
 
 let pr_evar_list env sigma l =
   let open Evd in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e15c00f7dc..e21c2fda85 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -104,6 +104,7 @@ let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env ev
       Evar_kinds.qm_name=na;
   }) in
   let evd, v = Evarutil.new_evar env !evdref ~src c in
+  let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in
   evdref := evd;
   v
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 55817f1b76..24767ca4d1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -457,6 +457,15 @@ let pretype_sort ?loc sigma = function
 let new_type_evar env sigma loc =
   new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
 
+let mark_obligation_evar sigma k evc =
+  if Flags.is_program_mode () then
+    match k with
+    | Evar_kinds.QuestionMark _
+    | Evar_kinds.ImplicitArg (_, _, false) ->
+      Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+    | _ -> sigma
+  else sigma
+
 (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [sigma] and *)
 (* the type constraint tycon *)
@@ -510,15 +519,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         | Some ty -> sigma, ty
         | None -> new_type_evar env sigma loc in
       let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
-      let sigma =
-        if Flags.is_program_mode () then
-          match k with
-          | Evar_kinds.QuestionMark _
-          | Evar_kinds.ImplicitArg (_, _, false) ->
-            Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val))
-          | _ -> sigma
-        else sigma
-      in
+      let sigma = mark_obligation_evar sigma k uj_val in
       sigma, { uj_val; uj_type = ty }
 
   | GHole (k, _naming, Some arg) ->
@@ -1039,6 +1040,7 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
        | None ->
          let sigma, s = new_sort_variable univ_flexible_alg sigma in
          let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
+         let sigma = mark_obligation_evar sigma knd utj_val in
          sigma, { utj_val; utj_type = s})
   | _ ->
       let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index cea8af3f05..fe8ef1f0e0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -178,7 +178,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     let sigma, h_e_term = Evarutil.new_evar env sigma
         ~src:(Loc.tag @@ Evar_kinds.QuestionMark {
             Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false;
-        }) wf_proof in
+          }) wf_proof in
+    let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma h_e_term)) in
     sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
   in
   let sigma, def = Typing.solve_evars env sigma def in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index fbf552e649..5c1384fba7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -37,13 +37,11 @@ let succfix (depth, fixrels) =
 
 let check_evars env evm =
   Evar.Map.iter
-  (fun key evi ->
-   let (loc,k) = evar_source key evm in
-     match k with
-     | Evar_kinds.QuestionMark _
-     | Evar_kinds.ImplicitArg (_,_,false) -> ()
-     | _ ->
-       Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
+    (fun key evi ->
+       if Evd.is_obligation_evar evm key then ()
+       else
+         let (loc,k) = evar_source key evm in
+         Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
   (Evd.undefined_map evm)
 
 type oblinfo =