diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 11:27:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 11:27:53 +0000 |
| commit | 8eddb7aa344b1b1a6d2552576f4dee80677c4337 (patch) | |
| tree | 2853850023a2cc8f13b3246b4bdb2299efd9a698 | |
| parent | b230388e6843aea7dae6a662eee4bbe8acf8a79a (diff) | |
Bugs divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3419 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/ppconstr.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 600588ce8..987c2000d 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -277,16 +277,16 @@ let rec pr inherited a = hov 0 ( pr_opt (pr_annotation pr) po ++ hv 0 ( - str "if" ++ pr ltop c ++ spc () ++ + str "if " ++ pr ltop c ++ spc () ++ hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++ hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif - | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,_ as bd],b)]) -> + | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,CHole _ as bd],b)]) -> hov 0 ( pr_opt (pr_annotation pr) po ++ hv 0 ( str "let" ++ brk (1,1) ++ hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++ - str " =" ++ brk (1,1) ++ + str " =" ++ brk (1,2) ++ pr ltop c ++ spc () ++ str "in " ++ pr ltop b)), lletin | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) -> @@ -391,10 +391,10 @@ let gentermpr gt = with s -> wrap_exception s (* [at_top] means ids of env must be avoided in bound variables *) -(* + let gentermpr_core at_top env t = gentermpr (Termast.ast_of_constr at_top env t) -*) +(* let gentermpr_core at_top env t = pr_constr (Constrextern.extern_constr at_top env t) - +*) |