diff options
| author | Pierre-Marie Pédrot | 2020-08-27 16:23:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 16:23:44 +0200 |
| commit | 2062f9cd5ce3c17c128186d1e9e2193528941e5c (patch) | |
| tree | edd7cf41caeedae18d60dc5c859e2532884ab80a /vernac/classes.ml | |
| parent | 829d7ac10175c41eaf3ce8ad9531abeab713dcba (diff) | |
| parent | bd00733ef04e4c916ab4a00d80e9ee1142bcd410 (diff) | |
Merge PR #12499: Clean future goals
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index f454c389dc..82a1e32a14 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -358,8 +358,9 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code the refinement manually.*) - let gls = List.rev (Evd.future_goals sigma) in - let sigma = Evd.reset_future_goals sigma in + let future_goals, sigma = Evd.pop_future_goals sigma in + let gls = List.rev_append future_goals.Evd.FutureGoals.shelf (List.rev future_goals.Evd.FutureGoals.comb) in + let sigma = Evd.push_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Declare.Info.make ~hook ~kind ~udecl ~poly () in |