diff options
| author | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
| commit | eed90d1bd867dce59f6bf1b2bf769fff188f128b (patch) | |
| tree | cfbf3bb666b23d0ddce9ea3c370c54eb4a87a150 /engine/proofview.ml | |
| parent | 23588ea0ccacd7e0071cbbad3328d871414f37c6 (diff) | |
| parent | bbde815f8108f4641f5411d03f7a88096cc2221b (diff) | |
Merge PR#248: Adding eassert, eset, epose, etc.
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index ddfc0e39dd..29bb1ef397 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content = let info = if goal then { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark (_,Names.Name id) | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } else info |