diff options
Diffstat (limited to 'vernac/proof_using.ml')
| -rw-r--r-- | vernac/proof_using.ml | 44 |
1 files changed, 18 insertions, 26 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index f8b085f3ef..526845084a 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -18,14 +18,6 @@ module NamedDecl = Context.Named.Declaration let known_names = Summary.ref [] ~name:"proofusing-nameset" -let in_nameset = - let open Libobject in - declare_object { (default_object "proofusing-nameset") with - cache_function = (fun (_,x) -> known_names := x :: !known_names); - classify_function = (fun _ -> Dispose); - discharge_function = (fun _ -> None) - } - let rec close_fwd e s = let s' = List.fold_left (fun s decl -> @@ -73,7 +65,7 @@ let process_expr env e ty = let s = Id.Set.union v_ty (process_expr env e ty) in Id.Set.elements s -let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) +let name_set id expr = known_names := (id,expr) :: !known_names let minimize_hyps env ids = let rec aux ids = @@ -145,13 +137,13 @@ let suggest_common env ppid used ids_typ skip = let suggest_proof_using = ref false -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "suggest Proof using"; - Goptions.optkey = ["Suggest";"Proof";"Using"]; - Goptions.optread = (fun () -> !suggest_proof_using); - Goptions.optwrite = ((:=) suggest_proof_using) } +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "suggest Proof using"; + optkey = ["Suggest";"Proof";"Using"]; + optread = (fun () -> !suggest_proof_using); + optwrite = ((:=) suggest_proof_using) }) let suggest_constant env kn = if !suggest_proof_using @@ -178,15 +170,15 @@ let suggest_variable env id = let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us))) - -let _ = - Goptions.declare_stringopt_option - { Goptions.optdepr = false; - Goptions.optname = "default value for Proof using"; - Goptions.optkey = ["Default";"Proof";"Using"]; - Goptions.optread = (fun () -> Option.map using_to_string !value); - Goptions.optwrite = (fun b -> value := Option.map using_from_string b); - } +let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) + +let () = + Goptions.(declare_stringopt_option + { optdepr = false; + optname = "default value for Proof using"; + optkey = ["Default";"Proof";"Using"]; + optread = (fun () -> Option.map using_to_string !value); + optwrite = (fun b -> value := Option.map using_from_string b); + }) let get_default_proof_using () = !value |