diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-03 22:32:59 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-03 22:32:59 +0000 |
| commit | b1512d41c3d7065eb76eec0014376ad144414fb8 (patch) | |
| tree | add82cb35006c821bae0eb39ce695169780a6450 /toplevel | |
| parent | f55e532771a3aeddeb7d6fdad6247572af936b5b (diff) | |
Retrait de PrintConstr vers top_printers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@412 85f007b7-540e-0410-9357-904b9bb8a0f7
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 7737bdc6c..1a45b8540 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") -***) |