diff options
| author | Maxime Dénès | 2020-08-25 23:29:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | bd00733ef04e4c916ab4a00d80e9ee1142bcd410 (patch) | |
| tree | 375bbd123fe2703d77a973070938a022070685ff /proofs/refine.ml | |
| parent | 4a9057d1202c27cbcca22d3939da5136dbf8ad3c (diff) | |
Wrap future goals into a module
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 7f0fa587cd..51d6c923b6 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -74,14 +74,14 @@ let generic_refine ~typecheck f gl = (* Restore the [future goals] state. *) let future_goals, sigma = Evd.pop_future_goals sigma in (* Select the goals *) - let future_goals = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) future_goals in + let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> (* Nothing to do, the goal has been solved by side-effect *) sigma | Some self -> - match future_goals.Evd.future_principal with + match future_goals.Evd.FutureGoals.principal with | None -> Evd.define self c sigma | Some evk -> let id = Evd.evar_ident self sigma in @@ -91,16 +91,16 @@ let generic_refine ~typecheck f gl = | Some id -> Evd.rename evk id sigma in (* Mark goals *) - let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.future_comb in - let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.future_shelf in - let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.future_comb in + let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in + let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.FutureGoals.shelf in + let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> - Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.future_shelf <*> + Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.FutureGoals.shelf <*> Proofview.tclUNIT v end |