diff options
| author | herbelin | 2003-01-19 16:26:21 +0000 |
|---|---|---|
| committer | herbelin | 2003-01-19 16:26:21 +0000 |
| commit | db14ee0eeeac1d833dbd32b3cfd030576dafa3d5 (patch) | |
| tree | b8964cda333737b642a8dfd6bc8e10c08b1f49a3 | |
| parent | 470fcab24a5109d076eab5272afec8612f265e89 (diff) | |
Rétablissement pr_pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3527 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/ppconstr.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 544a9fed5a..57e8136322 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -212,7 +212,7 @@ let pr_recursive fix pr_decl id = function | [] -> anomaly "(co)fixpoint with no definition" | d1::dl -> hov 0 ( - str fix ++ spc () ++ pr_id id ++ brk (0,2) ++ str "{" ++ + str fix ++ spc () ++ pr_id id ++ brk (1,2) ++ str "{" ++ (v 0 ( (hov 0 (pr_decl d1)) ++ (prlist (fun fix -> fnl () ++ hov 0 (str "with" ++ pr_decl fix)) @@ -335,7 +335,7 @@ let rec pr inherited a = let pr_constr = pr ltop -let pr_pattern x = (* gentermpr*) failwith "pr_pattern: TODO" +let pr_pattern = pr_constr let pr_qualid qid = str (string_of_qualid qid) @@ -416,3 +416,4 @@ let gentermpr_core at_top env t = let gentermpr_core at_top env t = pr_constr (Constrextern.extern_constr at_top env t) *) + |