diff options
Diffstat (limited to 'engine/geninterp.mli')
| -rw-r--r-- | engine/geninterp.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 42e1e3784c..b70671a2d9 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Interpretation functions for generic arguments. *) +(** Interpretation functions for generic arguments and interpreted Ltac + values. *) open Names open Genarg |