diff options
| author | Pierre-Marie Pédrot | 2019-04-11 12:07:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-11 12:07:00 +0200 |
| commit | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (patch) | |
| tree | 73c615fe6e2853d5879eebbd034d18bdf8fd686b /library | |
| parent | 36c15766a9295d980d142da0e42aebf1309f4eb4 (diff) | |
| parent | 9fe0932a7b04eecea35f98bc2b38beebb64d476a (diff) | |
Merge PR #9909: Remove all but one call to `Global` in the pretyper
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 12 | ||||
| -rw-r--r-- | library/goptions.mli | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 1b907fd966..b9c1802a72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -57,7 +57,7 @@ module MakeTable = type key val compare : t -> t -> int val table : (string * key table_of_A) list ref - val encode : key -> t + val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -111,10 +111,10 @@ module MakeTable = class table_of_A () = object - method add x = add_option (A.encode x) - method remove x = remove_option (A.encode x) + method add x = add_option (A.encode (Global.env()) x) + method remove x = remove_option (A.encode (Global.env()) x) method mem x = - let y = A.encode x in + let y = A.encode (Global.env()) x in let answer = MySet.mem y !t in Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t @@ -142,7 +142,7 @@ struct type key = string let compare = String.compare let table = string_table - let encode x = x + let encode _env x = x let subst _ x = x let printer = str let key = A.key @@ -161,7 +161,7 @@ module type RefConvertArg = sig type t val compare : t -> t -> int - val encode : qualid -> t + val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name diff --git a/library/goptions.mli b/library/goptions.mli index b91553bf3c..9925eb9e7b 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -89,8 +89,8 @@ module MakeRefTable : (A : sig type t val compare : t -> t -> int - val encode : qualid -> t - val subst : substitution -> t -> t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name val title : string |