From 9779c0bf4945693bfd37b141e2c9f0fea200ba4d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Apr 2019 14:09:42 +0200 Subject: Integrate build and documentation of Ltac2 Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions. --- user-contrib/Ltac2/Array.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 user-contrib/Ltac2/Array.v (limited to 'user-contrib/Ltac2/Array.v') diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v new file mode 100644 index 0000000000..11b64e3515 --- /dev/null +++ b/user-contrib/Ltac2/Array.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a -> 'a array := "ltac2" "array_make". +Ltac2 @external length : 'a array -> int := "ltac2" "array_length". +Ltac2 @external get : 'a array -> int -> 'a := "ltac2" "array_get". +Ltac2 @external set : 'a array -> int -> 'a -> unit := "ltac2" "array_set". -- cgit v1.2.3