From 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 Oct 2018 22:04:38 +0100
Subject: Switch to using the obligation_evar flag instead of the evar source

for the determination of evars that can be turned into obligations.
---
 vernac/comProgramFixpoint.ml |  3 ++-
 vernac/obligations.ml        | 12 +++++-------
 2 files changed, 7 insertions(+), 8 deletions(-)

(limited to 'vernac')

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 =
-- 
cgit v1.2.3