Do not thunk notations preemptively.

One has to rely on the 'thunk' token to produce such thunks.

3 files changed, 17 insertions, 9 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 111ef1c8eb..e0a65dde2d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -753,7 +753,7 @@ let add_generic_scope s entry arg =
   let parse = function
   | [] ->
     let scope = Extend.Aentry entry in
-    let act x = rthunk (CTacExt (dummy_loc, in_gen (rawwit arg) x)) in
+    let act x = CTacExt (dummy_loc, in_gen (rawwit arg) x) in
     Tac2entries.ScopeRule (scope, act)
   | _ -> scope_fail ()
   in
@@ -818,7 +818,7 @@ end
 let () = add_scope "self" begin function
 | [] ->
   let scope = Extend.Aself in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -826,7 +826,7 @@ end
 let () = add_scope "next" begin function
 | [] ->
   let scope = Extend.Anext in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -835,12 +835,12 @@ let () = add_scope "tactic" begin function
 | [] ->
   (** Default to level 5 parsing *)
   let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt (loc, n)] ->
   let () = if n < 0 || n > 5 then scope_fail () in
   let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -848,7 +848,7 @@ end
 let () = add_scope "ident" begin function
 | [] ->
   let scope = Extend.Aentry Tac2entries.Pltac.q_ident in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -856,7 +856,15 @@ end
 let () = add_scope "bindings" begin function
 | [] ->
   let scope = Extend.Aentry Tac2entries.Pltac.q_bindings in
-  let act tac = rthunk tac in
+  let act tac = tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "thunk" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let act e = rthunk (act e) in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
diff --git a/tests/example2.v b/tests/example2.v
index 14a6b68e18..5efbf90b34 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -1,6 +1,6 @@
 Require Import Ltac2.Ltac2.
 
-Ltac2 Notation "split" bnd(bindings) := Std.split (bnd ()).
+Ltac2 Notation "split" bnd(bindings) := Std.split bnd.
 
 Goal exists n, n = 0.
 Proof.
diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index 35546ef6c1..ece6fca06a 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -111,7 +111,7 @@ Proof.
 Fail zero (Bar "lol").
 Abort.
 
-Ltac2 Notation "refine!" c(constr) := refine c.
+Ltac2 Notation "refine!" c(thunk(constr)) := refine c.
 
 Goal True.
 Proof.