diff --git a/doc/changelog/06-Ltac2-language/18082-tac2pure.rst b/doc/changelog/06-Ltac2-language/18082-tac2pure.rst new file mode 100644 index 0000000000000..8382ff798e130 --- /dev/null +++ b/doc/changelog/06-Ltac2-language/18082-tac2pure.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Ltac2 mutable references are not considered values anymore + (`#18082 `_, + by Gaƫtan Gilbert). diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index cc659330e30ca..dab190ebeed85 100644 --- 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 index 9108871e28a99..c17f9b5240bf0 100644 --- 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 =>