diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7737bdc6ce..1a45b8540b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1451,14 +1451,3 @@ let _ = if subtree_solved () then (rev_mutate top_of_tree; print_subgoals()) )) - -(*Only for debug*) -(*** -let _ = - add "PrintConstr" - (function - | [VARG_CONSTR c] -> - (fun () -> - Term.constr_display (constr_of_com empty_evd (initial_sign()) c)) - | _ -> bad_vernac_args "PrintConstr") -***) |