diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-02 20:28:44 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-02 20:28:44 +0000 |
| commit | b96e45b1714c12daa1127e8bf14467eea07ebe17 (patch) | |
| tree | 8e5915dc3d72d498495e49a8bbbd7c066cb71026 /translate/ppconstrnew.mli | |
| parent | 0d3a3d5650cd374eed4272a0de1e3f926a8d3c40 (diff) | |
meilleure presentation des commentaires du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/ppconstrnew.mli')
| -rw-r--r-- | translate/ppconstrnew.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index 968464f65..51c6f8b7f 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -40,7 +40,15 @@ val pr_global : Idset.t -> global_reference -> std_ppcmds val pr_tight_coma : unit -> std_ppcmds val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds +val pr_lident : identifier located -> std_ppcmds +val pr_lname : name located -> std_ppcmds + val pr_with_comments : loc -> std_ppcmds -> std_ppcmds +val pr_com_at : int -> std_ppcmds +val pr_sep_com : + (unit -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + constr_expr -> std_ppcmds val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds |