diff options
Diffstat (limited to 'src/tac2env.mli')
| -rw-r--r-- | src/tac2env.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/tac2env.mli b/src/tac2env.mli index 7616579d63..c7e87c5432 100644 --- a/src/tac2env.mli +++ b/src/tac2env.mli @@ -133,6 +133,9 @@ val coq_prefix : ModPath.t val std_prefix : ModPath.t (** Path where Ltac-specific datatypes are defined in Ltac2 plugin. *) +val ltac1_prefix : ModPath.t +(** Path where the Ltac1 legacy FFI is defined. *) + (** {5 Generic arguments} *) val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type |