More ltac2 typed notations testing, remove now useless extra type ann…

…otation

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)

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

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).