From a67605c7af04014a9773d0351f55c9a08015de89 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 13 Jul 2018 18:34:56 +0200 Subject: Remove useless libobject in proof_using --- vernac/proof_using.ml | 10 +--------- 1 file changed, 1 insertion(+), 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 = -- cgit v1.2.3