diff options
| author | Pierre-Marie Pédrot | 2018-11-03 16:14:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 16:14:49 +0100 |
| commit | 228066a783a581ba2b304a12d9fe5e8decebcc48 (patch) | |
| tree | df03e7a95d544d42a44b5c464938a8925ec80cfc /vernac/comProgramFixpoint.ml | |
| parent | 4ffb04be9b8829abb0f869fb4fd68156f4a01f95 (diff) | |
| parent | 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (diff) | |
Merge PR #8852: Use the obligation evar flag
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |