diff options
Diffstat (limited to 'proofs/proofview.ml')
| -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 569ae148a..d69ee0260 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 |