From d310030a70c972bd6d4fd23b979a7cfd809e000f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 15:50:43 +0100
Subject: Small improvement to "fix"/"cofix" printing rule.

Set Implicit Arguments.
Set Contextual Implicit.
Inductive option A := None | Some (a:A).
Coercion some_nat := @Some nat.
Check fix f x := match x with 0 => None | n => some_nat n end.

gives:

fix f (x : nat) : option nat :=
  match x with
  | 0 => None (A:=nat)
  | S _ => some_nat x
  end

See discussion at
https://github.com/coq/coq/pull/11142/files/718c1422954794e0e33a87cf4c9111c00cc186dd#r377054717
---
 test-suite/output/Fixpoint.out | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 6879cbc3c2..60bc9cbf55 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -1,8 +1,8 @@
-fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
-list B := match l with
-          | nil => nil
-          | a :: l0 => f a :: F A B f l0
-          end
+fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
+  match l with
+  | nil => nil
+  | a :: l0 => f a :: F A B f l0
+  end
      : forall A B : Set, (A -> B) -> list A -> list B
 let fix f (m : nat) : nat := match m with
                              | 0 => 0
-- 
cgit v1.2.3