diff options
Diffstat (limited to 'pretyping/namegen.mli')
| -rw-r--r-- | pretyping/namegen.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index e3ab7d03e..889f8ec8c 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: namegen.mli 12549 2009-12-01 12:05:57Z herbelin {% $ %} *) - open Names open Term open Environ |