diff options
Diffstat (limited to 'ide/coqide')
| -rw-r--r-- | ide/coqide/coq.ml | 3 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 6 |
2 files changed, 5 insertions, 4 deletions
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 57cdccce6d..0e237b74fe 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -544,6 +544,7 @@ struct let coercions = BoolOpt ["Printing"; "Coercions"] let raw_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] + let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] let existential = BoolOpt ["Printing"; "Existential"; "Instances"] let universes = BoolOpt ["Printing"; "Universes"] @@ -558,7 +559,7 @@ struct { opts = [raw_matching]; init = true; label = "Display raw _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; - { opts = [notations]; init = true; label = "Display _parentheses" }; + { opts = [parentheses]; init = true; label = "Display _parentheses" }; { opts = [all_basic]; init = false; label = "Display _all basic low-level contents" }; { opts = [existential]; init = false; diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 2adc35ae3e..ad21f663e4 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 } 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.shelved_goals = process @@ Evd.shelf sigma + ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma) } let goals () = |