diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-17 15:45:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-17 15:45:34 +0000 |
| commit | 717cc0231fe121cf2e6917b582374bbf67e0b676 (patch) | |
| tree | adefe3535fe3bfddf8ed90f91b09213859f18eb1 | |
| parent | c68eca79f7c86703cd468721dcd5288b60c281f7 (diff) | |
Divers bugs d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4665 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/pptacticnew.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 3e50cdb09..0dbc08250 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -421,11 +421,11 @@ and pr_atom1 env = function | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> - hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ cut() ++ + hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ str"with " ++ prlist_with_sep spc (pr_fix_tac env) l) | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> - hov 1 (str "cofix" ++ spc () ++ pr_id id ++ cut () ++ + hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l) | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c) | TacTrueCut (None,c) -> @@ -562,7 +562,7 @@ and pr_atom1 env = function (* Equality and inversion *) | TacInversion (DepInversion (k,c,ids),hyp) -> - hov 1 (str "dependent " ++ pr_induction_kind k ++ + hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ pr_with_names ids ++ pr_with_constr (pr_constr env) c) | TacInversion (NonDepInversion (k,cl,ids),hyp) -> @@ -571,7 +571,7 @@ and pr_atom1 env = function pr_with_names ids ++ pr_simple_clause pr_ident cl) | TacInversion (InversionUsing (c,cl),hyp) -> hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ - str "using" ++ spc () ++ pr_constr env c ++ + spc () ++ str "using" ++ spc () ++ pr_constr env c ++ pr_simple_clause pr_ident cl) in |