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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/coqide/idetop.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 2adc35ae3e..751bddc7c4 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -220,12 +220,12 @@ let process_goal_diffs diff_goal_map oldp nsigma ng = let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } -let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process = +let export_pre_goals Proof.{ sigma; goals; stack; shelf } process = let process = List.map (process sigma) in { Interface.fg_goals = process goals ; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack ; Interface.shelved_goals = process shelf - ; Interface.given_up_goals = process given_up + ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma) } let goals () = |