diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 20:38:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-25 13:20:54 +0200 |
| commit | b39465da31bfd488dfad4ea4627186f9a1843e56 (patch) | |
| tree | ecb154c909121d3e2eccf5885bd4b22d817a8866 /proofs/proofview.ml | |
| parent | 9973cd2ca529076388710e90f2c46180581397cf (diff) | |
VarInstance are also goals.
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 |