diff options
| author | Arnaud Spiwack | 2014-10-16 14:28:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 14:35:34 +0200 |
| commit | ce260a0db279ce09dda70e079ae3c35b49f05ec4 (patch) | |
| tree | 21f409a6874f9f390c86d3ce6f5d4b14a49d7bdc /pretyping | |
| 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')
| -rw-r--r-- | pretyping/evd.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 |
2 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 35ca18e4f5..b8886b9b54 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 diff --git a/pretyping/evd.mli b/pretyping/evd.mli index c15975b0ea..cc64b3594c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -301,6 +301,12 @@ val reset_future_goals : evar_map -> evar_map (** Clears the list of future goals (as well as the principal future goal). Used by the [refine] primitive of the tactic engine. *) +val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map +(** Sets the future goals (including the principal future goal) to a + previous value. Intended to be used after a local list of future + goals has been consumed. Used by the [refine] primitive of the + tactic engine. *) + (** {5 Sort variables} Evar maps also keep track of the universe constraints defined at a given |