diff options
| author | Matthieu Sozeau | 2018-10-29 22:04:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-30 11:45:05 +0100 |
| commit | 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (patch) | |
| tree | d15e9319ecc1fb41059acba55328d393a66acfb9 /vernac | |
| parent | 57a0d5091a9524d35161875a884835a573d82e0b (diff) | |
Switch to using the obligation_evar flag instead of the evar source
for the determination of evars that can be turned into obligations.
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 = |