diff options
| author | Enrico Tassi | 2014-12-28 11:43:01 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-28 11:43:01 +0100 |
| commit | 0276f8357a2ea1d83cb6b85b86b8b3f5a1e4579d (patch) | |
| tree | 1fbf3c67762b2358f7166ca8c05565d4c1bcf33e | |
| parent | aeb5daa2efdb2d0f2c75670e11d409f24528c54a (diff) | |
remove debug prints (leftover)
| -rw-r--r-- | proofs/proof_using.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
2 files changed, 1 insertions, 6 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)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cd1dad6940..4dc9ea4b20 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -849,7 +849,6 @@ let vernac_set_end_tac tac = let vernac_set_used_variables e = let tys = List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in - Pp.(msg_warning (prlist_with_sep spc Printer.pr_constr tys)); let l = Proof_using.process_expr (Global.env ()) e tys in let vars = Environ.named_context (Global.env ()) in List.iter (fun id -> |