Ltac2: mutable references are not values

SkySkimmer · Sep 25, 2023 · d108b81 · d108b81
1 parent 6ff90d8
commit d108b81
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 4 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18082-tac2pure.rst b/doc/changelog/06-Ltac2-language/18082-tac2pure.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Ltac2 mutable references are not considered values anymore
+  (`#18082 <https://github.com/coq/coq/pull/18082>`_,
+  by Gaëtan Gilbert).
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
@@ -115,8 +115,9 @@ let is_pure_constructor kn =
   | GTydDef _ -> assert false (** Type definitions have no constructors *)
 
 let rec is_value = function
-| GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
+| GTacAtm (AtmInt _) | GTacVar _ | GTacFun _ -> true
 | GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false
+| GTacRef kn -> not (Tac2env.interp_global kn).gdata_mutable
 | GTacCst (Tuple _, _, el) -> List.for_all is_value el
 | GTacCst (_, _, []) -> true
 | GTacOpn (_, el) -> List.for_all is_value el

diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
@@ -32,10 +32,10 @@ Ltac2 assert_eq n m :=
   | false => Control.throw Assertion_failure end.
 
 Ltac2 mutable x := O.
-Ltac2 y := x.
-Ltac2 Eval (assert_eq y O).
+Ltac2 y () := x.
+Ltac2 Eval (assert_eq (y()) O).
 Ltac2 Set x := (S O).
-Ltac2 Eval (assert_eq y (S O)).
+Ltac2 Eval (assert_eq (y()) (S O)).
 
 Ltac2 mutable quw := fun (n : nat) => O.
 Ltac2 Set quw := fun n =>