diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/namegen.ml | 32 | ||||
| -rw-r--r-- | engine/uState.ml | 9 | ||||
| -rw-r--r-- | engine/uState.mli | 2 |
3 files changed, 22 insertions, 21 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 370f35f6ed..c4472050f8 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -219,22 +219,22 @@ let get_mangle_names = ~key:["Mangle";"Names"] ~value:false -let mangle_names_prefix = ref (Id.of_string "_0") - -let set_prefix x = mangle_names_prefix := forget_subscript x - -let () = Goptions.( - declare_string_option - { optdepr = false; - optkey = ["Mangle";"Names";"Prefix"]; - optread = (fun () -> Id.to_string !mangle_names_prefix); - optwrite = begin fun x -> - set_prefix - (try Id.of_string x - with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) - end }) - -let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id +let mangle_names_prefix = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Mangle";"Names";"Prefix"] + ~value:(Id.of_string "_0") + (fun x -> + (try + Id.of_string x + with + | CErrors.UserError _ -> + CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")) + ) |> forget_subscript + ) + (fun x -> Id.to_string x) + +let mangle_id id = if get_mangle_names () then mangle_names_prefix () else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/uState.ml b/engine/uState.ml index d532129dc5..ff85f09efa 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -176,8 +176,11 @@ let instantiate_variable l b v = exception UniversesDiffer -let drop_weak_constraints = ref false - +let drop_weak_constraints = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Cumulativity";"Weak";"Constraints"] + ~value:false let process_universe_constraints ctx cstrs = let open UnivSubst in @@ -270,7 +273,7 @@ let process_universe_constraints ctx cstrs = | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local | UWeak (l, r) -> - if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local + if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local | UEq (l, r) -> equalize_universes l r local in let local = diff --git a/engine/uState.mli b/engine/uState.mli index 3959373ead..cd1c9a174e 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -69,8 +69,6 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry (** {5 Constraints handling} *) -val drop_weak_constraints : bool ref - val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ |