diff options
| author | Pierre-Marie Pédrot | 2020-11-02 13:02:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-02 13:02:14 +0100 |
| commit | e4575cb8e80d1cb8b65dc349e4f98432e8bda523 (patch) | |
| tree | 47e5977eeb3677a9e94a98bb9add2f1dd2bbe030 /printing/printer.ml | |
| parent | a392b0225a606b6c8fe0051f0d301d5f3b6d5cd3 (diff) | |
| parent | 05f8308dbed75ee223b4d0818f1604072cffe671 (diff) | |
Merge PR #13145: Adding support for printing goal names in CoqIDE
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index be1cc0d64a..ea718526de 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -45,6 +45,8 @@ let should_gname = ~key:["Printing";"Goal";"Names"] ~value:false +let print_goal_names = should_gname (* for export *) + (**********************************************************************) (** Terms *) |