aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/subtyping.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/subtyping.mli')
-rw-r--r--checker/subtyping.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 10842252e..1b0ca5c16 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
(*i*)
open Univ
open Term