From 58a2643cb5efc41d9b3f6718eea9ce6d506c111c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 21 Dec 2023 15:42:41 +0100
Subject: [PATCH] More ltac2 typed notations testing, remove now useless extra
 type annotation

---
 plugins/ltac2/tac2quote.ml                  |  5 +----
 test-suite/output/ltac2_typed_notations.out | 10 ++++++++++
 test-suite/output/ltac2_typed_notations.v   |  7 +++++++
 3 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml
index 0e817036303c..ae2a6385aa32 100644
--- a/plugins/ltac2/tac2quote.ml
+++ b/plugins/ltac2/tac2quote.ml
@@ -450,10 +450,7 @@ let of_constr_matching {loc;v=m} =
     of_tuple [knd; pat; e]
   in
   let e = of_list ?loc map m in
-  let tykn = pattern_core "constr_matching" in
-  let ty = CAst.make ?loc (CTypRef (AbsKn (Other tykn),[CAst.make ?loc (CTypVar Anonymous)])) in
-  CAst.make ?loc (CTacCnv (e, ty))
-
+  e
 
 (** From the patterns and the body of the branch, generate:
     - a goal pattern: (constr_match list * constr_match)
diff --git a/test-suite/output/ltac2_typed_notations.out b/test-suite/output/ltac2_typed_notations.out
index 91c0d870767a..5898783ae6d9 100644
--- a/test-suite/output/ltac2_typed_notations.out
+++ b/test-suite/output/ltac2_typed_notations.out
@@ -2,3 +2,13 @@ File "./output/ltac2_typed_notations.v", line 5, characters 9-10:
 The command has indeed failed with message:
 This expression has type bool but an expression was expected of type 
 constr
+fun (b : bool) =>
+let c := b in
+let (m : '__α Pattern.constr_matching) :=
+  [(Pattern.MatchPattern, pat:(true),
+    (fun _ => fun (_ : constr array) => true));
+    (Pattern.MatchPattern, pat:(false),
+     (fun _ => fun (_ : constr array) => false))] with 
+  (t : constr) := c in
+Pattern.one_match0 t m
+:'__α : bool
diff --git a/test-suite/output/ltac2_typed_notations.v b/test-suite/output/ltac2_typed_notations.v
index 5048223c00ee..2de4a96c76cd 100644
--- a/test-suite/output/ltac2_typed_notations.v
+++ b/test-suite/output/ltac2_typed_notations.v
@@ -7,3 +7,10 @@ Fail Ltac2 foo(b: bool): bool :=
   | false => false
   end.
 (* error used to be on the whole command *)
+
+Ltac2 Globalize fun (b: bool) =>
+  (let c := b in
+  match! c with
+  | true => true
+  | false => false
+  end : bool).