diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 09:53:16 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 09:53:16 +0200 |
| commit | 8023d0de14e707d716cb4be9f583a714b10da9bd (patch) | |
| tree | f67c42761d313f8d7a3e630f3dae6a6b7230863d | |
| parent | 9f4787b7ae9ee7f19bb74db39ec7304bfa97ebd5 (diff) | |
| parent | a67605c7af04014a9773d0351f55c9a08015de89 (diff) | |
Merge PR #8060: Remove useless libobject in proof_using
| -rw-r--r-- | vernac/proof_using.ml | 10 |
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 = |