From 5f314036e4d5c23bd68d492ab22b8859b38b5f8c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 8 Dec 2019 17:44:45 +0100
Subject: Take "Implicit Types" into account when printing terms.

---
 test-suite/output/ImplicitTypes.out | 26 ++++++++++++++++++++++++++
 test-suite/output/ImplicitTypes.v   | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+)
 create mode 100644 test-suite/output/ImplicitTypes.out
 create mode 100644 test-suite/output/ImplicitTypes.v

(limited to 'test-suite')

diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
new file mode 100644
index 0000000000..824c260e92
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.out
@@ -0,0 +1,26 @@
+forall b, b = b
+     : Prop
+forall b : nat, b = b
+     : Prop
+forall b : bool, @eq bool b b
+     : Prop
+forall b : bool, b = b
+     : Prop
+forall b c : bool, b = c
+     : Prop
+forall c b : bool, b = c
+     : Prop
+forall b1 b2, b1 = b2
+     : Prop
+fun b => b = b
+     : bool -> Prop
+fix f b (n : nat) {struct n} : bool :=
+  match n with
+  | 0 => b
+  | S p => f b p
+  end
+     : bool -> nat -> bool
+∀ b c : bool, b = c
+     : Prop
+∀ b1 b2, b1 = b2
+     : Prop
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
new file mode 100644
index 0000000000..dbc83f9229
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.v
@@ -0,0 +1,37 @@
+Implicit Types b : bool.
+Check forall b, b = b.
+
+(* Check the type is not used if not the reserved one *)
+Check forall b:nat, b = b.
+
+(* Check full printing *)
+Set Printing All.
+Check forall b, b = b.
+Unset Printing All.
+
+(* Check printing of type *)
+Unset Printing Use Implicit Types.
+Check forall b, b = b.
+Set Printing Use Implicit Types.
+
+(* Check factorization: we give priority on factorization over implicit type *)
+Check forall b c, b = c.
+Check forall c b, b = c.
+
+(* Check factorization of implicit types *)
+Check forall b1 b2, b1 = b2.
+
+(* Check in "fun" *)
+Check fun b => b = b.
+
+(* Check in binders *)
+Check fix f b n := match n with 0 => b | S p => f b p end.
+
+(* Check in notations *)
+Module Notation.
+  Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+    (at level 200, x binder, y binder, right associativity,
+    format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+  Check forall b c, b = c.
+  Check forall b1 b2, b1 = b2.
+End Notation.
-- 
cgit v1.2.3