diff options
| author | Hugo Herbelin | 2017-01-05 19:54:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-01-05 20:13:00 +0100 |
| commit | 65816f94ba427edf8999bf42633d0aad064e8ce4 (patch) | |
| tree | 80c9b34a1c2ba5af338a1409473475c5af277890 | |
| parent | 63ca4aac83ced14b9b8065ef43e29f7c2dfd331c (diff) | |
Fixing a little bug in printing cofix with no arguments.
| -rw-r--r-- | printing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Fixpoint.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Fixpoint.v | 5 |
3 files changed, 7 insertions, 2 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e21bfa007d..31d87f0ff1 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -418,7 +418,7 @@ end) = struct let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in - pr_id id ++ str" " ++ + pr_id id ++ (if bl = [] then mt () else str" ") ++ hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index a13ae4624a..6879cbc3c2 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -10,3 +10,5 @@ let fix f (m : nat) : nat := match m with end in f 0 : nat Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1) + = cofix inf : Inf := {| projS := inf |} + : Inf diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 8afa50ba57..fafb478bad 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,4 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. - +CoInductive Inf := S { projS : Inf }. +Definition expand_Inf (x : Inf) := S (projS x). +CoFixpoint inf := S inf. +Eval compute in inf. |