From cf8944bd201b743ebd524aadc279f771156d1a1b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Thu, 21 Dec 2023 15:39:11 +0100
Subject: [PATCH] Turn ltac2 typed notations on by default
Fix #17477
---
doc/stdlib/index-list.html.template | 1 +
plugins/ltac2/tac2intern.ml | 2 +-
sysinit/coqargs.ml | 1 +
test-suite/output/ltac2_check_globalize.out | 7 ++++---
test-suite/output/ltac2_check_globalize.v | 2 ++
test-suite/output/ltac2_typed_notations.out | 4 ++++
test-suite/output/ltac2_typed_notations.v | 9 +++++++++
user-contrib/Ltac2/Compat/Coq818.v | 2 ++
user-contrib/Ltac2/Compat/Coq819.v | 3 +++
9 files changed, 27 insertions(+), 4 deletions(-)
create mode 100644 test-suite/output/ltac2_typed_notations.out
create mode 100644 test-suite/output/ltac2_typed_notations.v
create mode 100644 user-contrib/Ltac2/Compat/Coq819.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index e57cfd7e8c05..f9c5eccfc597 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -710,6 +710,7 @@ through the Require Import command.
theories/Compat/Coq819.v
theories/Compat/Coq820.v
user-contrib/Ltac2/Compat/Coq818.v
+ user-contrib/Ltac2/Compat/Coq819.v
Array:
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index 870c58a3d82b..5c4457835eeb 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1724,7 +1724,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
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index a465dfdefc6c..0a6efbf5259e 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -242,6 +242,7 @@ let get_compat_file = function
let get_compat_files v =
let coq_compat = get_compat_file v in
match v with
+ | "8.19" -> coq_compat :: ["Ltac2.Compat.Coq819"]
| "8.18" | "8.17" -> coq_compat :: ["Ltac2.Compat.Coq818"]
| _ -> [coq_compat]
diff --git a/test-suite/output/ltac2_check_globalize.out b/test-suite/output/ltac2_check_globalize.out
index cf70cba87c4f..b5a8f75bbb23 100644
--- a/test-suite/output/ltac2_check_globalize.out
+++ b/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:(()))
diff --git a/test-suite/output/ltac2_check_globalize.v b/test-suite/output/ltac2_check_globalize.v
index 72ffc0d62f83..cbeea4f06581 100644
--- a/test-suite/output/ltac2_check_globalize.v
+++ b/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.
diff --git a/test-suite/output/ltac2_typed_notations.out b/test-suite/output/ltac2_typed_notations.out
new file mode 100644
index 000000000000..91c0d870767a
--- /dev/null
+++ b/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
diff --git a/test-suite/output/ltac2_typed_notations.v b/test-suite/output/ltac2_typed_notations.v
new file mode 100644
index 000000000000..5048223c00ee
--- /dev/null
+++ b/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 *)
diff --git a/user-contrib/Ltac2/Compat/Coq818.v b/user-contrib/Ltac2/Compat/Coq818.v
index f97a43c0d28c..d0b4b8576c06 100644
--- a/user-contrib/Ltac2/Compat/Coq818.v
+++ b/user-contrib/Ltac2/Compat/Coq818.v
@@ -1,5 +1,7 @@
Local Set Warnings "-masking-absolute-name".
+Require Export Ltac2.Compat.Coq819.
+
Require Ltac2.Array.
Module Export Ltac2.
diff --git a/user-contrib/Ltac2/Compat/Coq819.v b/user-contrib/Ltac2/Compat/Coq819.v
new file mode 100644
index 000000000000..f1345eb96d60
--- /dev/null
+++ b/user-contrib/Ltac2/Compat/Coq819.v
@@ -0,0 +1,3 @@
+Require Ltac2.Init.
+
+#[export] Unset Ltac2 Typed Notations.