Turn ltac2 typed notations on by default

Fix coq#17477

plugins/ltac2/tac2intern.ml

@@ -1714,7 +1714,7 @@ let debug_globalize_allow_ext ids tac =
 
 let { Goptions.get = typed_notations } =
   Goptions.declare_bool_option_and_ref
-    ~key:["Ltac2";"Typed";"Notations"] ~value:false ()
+    ~key:["Ltac2";"Typed";"Notations"] ~value:true ()
 
 let intern_notation_data ids body =
   if typed_notations () then

test-suite/output/ltac2_check_globalize.out

@@ -4,7 +4,7 @@ fun x => x : 'a -> 'a
 () ()
 (1, 2) 3
 let x := () in x ()
-File "./output/ltac2_check_globalize.v", line 20, characters 32-33:
+File "./output/ltac2_check_globalize.v", line 22, characters 32-33:
 The command has indeed failed with message:
 This expression has type unit. It is not a function and cannot be applied.
 let x := fun x => x in let _ := x 1 in let _ := x "" in ()
@@ -13,11 +13,11 @@ let accu := { contents := []} in
 (let x := fun x => accu.(contents) := (x :: accu.(contents)) in
  let _ := x 1 in let _ := x "" in ());
 accu.(contents)
-File "./output/ltac2_check_globalize.v", line 36, characters 0-144:
+File "./output/ltac2_check_globalize.v", line 38, characters 0-144:
 The command has indeed failed with message:
 This expression has type string but an expression was expected of type 
 int
-let m :=
+let (m : '__α Pattern.goal_matching) :=
   [(([(None, (Pattern.MatchPattern, pat:(_)))],
      (Pattern.MatchPattern, pat:(_))),
     (fun h =>
@@ -27,4 +27,5 @@ let m :=
      (fun _ => fun _ => fun _ => fun _ => fun _ => ()))] : _
     Pattern.goal_matching in
 Pattern.lazy_goal_match0 false m
+:'__α
 constr:(ltac2:(()))

test-suite/output/ltac2_check_globalize.v

@@ -1,5 +1,7 @@
 Require Import Ltac2.Ltac2.
 
+Unset Ltac2 Typed Notations.
+
 Ltac2 Notation "foo" := ().
 
 Ltac2 Globalize foo.

test-suite/output/ltac2_typed_notations.out

@@ -0,0 +1,4 @@
+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

test-suite/output/ltac2_typed_notations.v

@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Fail Ltac2 foo(b: bool): bool :=
+  let c := b in
+  match! c with
+  | true => true
+  | false => false
+  end.
+(* error used to be on the whole command *)