diff options
| author | herbelin | 2004-02-19 15:58:17 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-19 15:58:17 +0000 |
| commit | 06a8f83186d685a98d57c133b213e83a31a9e30f (patch) | |
| tree | 70a01683fdf0d2fc3ed4004445e37275acf53562 | |
| parent | 770481a1a1b0b7dcc349ea6c04cef98c841ba3e5 (diff) | |
Bugs/insuffisances trouvees en traduisant MMode
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5361 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/ppconstrnew.ml | 2 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 2 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 3 |
3 files changed, 5 insertions, 2 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 9a86e3ffa4..f8d81c2430 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -537,6 +537,7 @@ let rec pr sep inherited a = hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)), lif +(* | COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) @@ -556,6 +557,7 @@ let rec pr sep inherited a = pr spc ltop c ++ str " in") ++ pr spc ltop b), lletin +*) | COrderedCase (_,style,po,c,bl) -> hv 0 ( str (if style=MatchStyle then "old_match " else "match ") ++ diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 63423b7b52..d663c942ac 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -240,7 +240,7 @@ let pr_hyp_location pr_id (id,occs,(hl,hl')) = if !hl' <> None then pr_hyp_location pr_id (id,occs,out_some !hl') else (if hl = InHyp && Options.do_translate () then - msgerrnl (str "Translator warning: Unable to detect if " ++ pr_id id ++ str " denotes a local definition"); + msgerrnl (h 0 (str "Translator warning: Unable to detect if " ++ pr_id id ++ spc () ++ str "denotes a local definition")); pr_hyp_location pr_id (id,occs,hl)) let pr_in pp = spc () ++ hov 0 (str "in" ++ pp) diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 7689014982..85dae24ae3 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -132,6 +132,7 @@ let pr_set_entry_type = function | ETBigint -> str "bigint" let pr_non_terminal = function + | NtQual ("constr","constr") -> str "constr" | NtQual (u,nt) -> str u ++ str" : " ++ str nt | NtShort "constrarg" -> str "constr" | NtShort nt -> str nt @@ -144,7 +145,7 @@ let strip_meta id = let pr_production_item = function | VNonTerm (loc,nt,Some p) -> pr_non_terminal nt ++ str"(" ++ pr_id (strip_meta p) ++ str")" | VNonTerm (loc,nt,None) -> pr_non_terminal nt - | VTerm s -> str s + | VTerm s -> qsnew s let pr_comment pr_c = function | CommentConstr c -> pr_c c |