diff options
| author | Hugo Herbelin | 2014-10-23 20:38:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-25 13:20:54 +0200 |
| commit | b39465da31bfd488dfad4ea4627186f9a1843e56 (patch) | |
| tree | ecb154c909121d3e2eccf5885bd4b22d817a8866 | |
| parent | 9973cd2ca529076388710e90f2c46180581397cf (diff) | |
VarInstance are also goals.
| -rw-r--r-- | proofs/proofview.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 569ae148ae..d69ee0260b 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -888,7 +888,9 @@ struct let mark_as_goal evd content = let info = Evd.find evd content in let info = - { info with Evd.evar_source = (fst (info.Evd.evar_source),Evar_kinds.GoalEvar) } + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } in let info = Typeclasses.mark_unresolvable info in Evd.add evd content info |