diff options
| author | Pierre-Marie Pédrot | 2020-11-22 16:03:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-30 18:46:50 +0100 |
| commit | 3ae0e24c7c6501abfb32e1cc11ac7c9eac379afe (patch) | |
| tree | f9c76d15a0325718fd26242551de1c29274601ee | |
| parent | bf111baffe75ebc1fc57aeb163e56a344d0632b8 (diff) | |
Adding a changelog for Ltac1.lambda.
| -rw-r--r-- | doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst new file mode 100644 index 0000000000..26b72de2aa --- /dev/null +++ b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst @@ -0,0 +1,6 @@ +- **Added:** + A function Ltac1.lambda allowing to embed Ltac2 functions + into Ltac1 runtime values + (`#13442 <https://github.com/coq/coq/pull/13442>`_, + fixes `#12871 <https://github.com/coq/coq/issues/12871>`_, + by Pierre-Marie Pédrot). |