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 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac/comProgramFixpoint.ml')

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