aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-13 18:34:56 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-13 18:34:56 +0200
commita67605c7af04014a9773d0351f55c9a08015de89 (patch)
treeed4f0a89b8b3c88bc8707510aff19fe60ca71ec1 /vernac
parentbd0a681350b1bc8947d6d7603dc6a9759f0c7897 (diff)
Remove useless libobject in proof_using
Diffstat (limited to 'vernac')
-rw-r--r--vernac/proof_using.ml10
1 files changed, 1 insertions, 9 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 74e53bef1..3e2bd9872 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 =