diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-01 18:12:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-01 18:55:28 +0200 |
| commit | 502e61ec1ac488dd430ce6654c7a6947c6f7d1c3 (patch) | |
| tree | 9270e2bbbb0d131a174301b51b6bf20731f40a2e | |
| parent | fed97ad8d6c34b6a577f8477a03200b1056dbc46 (diff) | |
Evars introduced by Proofview refining are flagged as GoalEvar. For some
reasons, some code depends on it.
| -rw-r--r-- | proofs/proofview.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 0600a9c8b..c7ffca3eb 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -860,7 +860,8 @@ struct type handle = Evd.evar_map * goal list let new_evar (evd, evs) env typ = - let (evd, ev) = Evarutil.new_evar evd env typ in + let src = (Loc.ghost, Evar_kinds.GoalEvar) in + let (evd, ev) = Evarutil.new_evar evd env ~src typ in let (evk, _) = Term.destEvar ev in let h = (evd, build_goal evk :: evs) in (h, ev) |