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 | |
| parent | 4ffb04be9b8829abb0f869fb4fd68156f4a01f95 (diff) | |
| parent | 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (diff) | |
Merge PR #8852: Use the obligation evar flag
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 3 | ||||
| -rw-r--r-- | vernac/obligations.ml | 12 |
2 files changed, 7 insertions, 8 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 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 = |