diff options
| author | Maxime Dénès | 2019-04-25 14:09:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-07 10:02:56 +0200 |
| commit | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (patch) | |
| tree | 26f563e3ad9562bdeb67efe8ff55be5de7fc55e2 /user-contrib/Ltac2/tac2extffi.mli | |
| parent | 392d40134c9cd7dee882e31da96369dd09fbbb45 (diff) | |
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.
Diffstat (limited to 'user-contrib/Ltac2/tac2extffi.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2extffi.mli | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2extffi.mli b/user-contrib/Ltac2/tac2extffi.mli new file mode 100644 index 0000000000..f5251c3d0d --- /dev/null +++ b/user-contrib/Ltac2/tac2extffi.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Tac2ffi +open Tac2types + +val qhyp : quantified_hypothesis repr + +val bindings : bindings repr + +val constr_with_bindings : constr_with_bindings repr |