diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 14:28:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 14:35:34 +0200 |
| commit | ce260a0db279ce09dda70e079ae3c35b49f05ec4 (patch) | |
| tree | 21f409a6874f9f390c86d3ce6f5d4b14a49d7bdc /pretyping/evd.ml | |
| parent | 025c4f63b28671a24bd6c46f9b23a3dad76fd179 (diff) | |
Refine: proper scoping of the future goals.
In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 35ca18e4f..b8886b9b5 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1007,6 +1007,9 @@ let principal_future_goal evd = evd.principal_future_goal let reset_future_goals evd = { evd with future_goals = [] ; principal_future_goal=None } +let restore_future_goals evd gls pgl = + { evd with future_goals = gls ; principal_future_goal = pgl } + let meta_diff ext orig = Metamap.fold (fun m v acc -> if Metamap.mem m orig then acc |