diff options
| author | Gaëtan Gilbert | 2017-09-20 19:45:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-25 14:18:35 +0100 |
| commit | 280c922fc55b57c430cad721c83650a796a375fd (patch) | |
| tree | 5f0c9c20a75532ba134bbde6f428facefceb5125 /intf | |
| parent | c93d5094bff73498ec8fc02837e16cc5ce9103b6 (diff) | |
Allow local universe renaming in Print.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 9aef4b1312..96bcba5e8b 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -40,6 +40,8 @@ type goal_reference = | NthGoal of int | GoalId of Id.t +type univ_name_list = Name.t Loc.located list + type printable = | PrintTables | PrintFullContext @@ -54,7 +56,7 @@ type printable = | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of reference or_by_notation + | PrintName of reference or_by_notation * univ_name_list option | PrintGraph | PrintClasses | PrintTypeClasses @@ -70,7 +72,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * goal_selector option + | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option |