diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_using.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 144646f3e8..d4e97a23ff 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -60,11 +60,7 @@ and full_set env = set_of_list env (List.map pi1 (named_context env)) let process_expr env e ty = let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in - let l = Id.Set.elements s in - Pp.msg_warning Pp.(str(to_string e) ++ spc() ++ str "-> "++ -(* prlist_with_sep spc Ppconstr.pr_constr ty ++ spc() ++ *) - prlist_with_sep spc Nameops.pr_id l); - l + Id.Set.elements s let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) |