aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml2
-rw-r--r--checker/checker.ml2
-rw-r--r--checker/closure.ml2
-rw-r--r--checker/closure.mli2
-rw-r--r--checker/indtypes.ml2
-rw-r--r--checker/indtypes.mli2
-rw-r--r--checker/inductive.ml2
-rw-r--r--checker/inductive.mli2
-rw-r--r--checker/modops.ml2
-rw-r--r--checker/modops.mli2
-rw-r--r--checker/reduction.ml2
-rw-r--r--checker/reduction.mli2
-rw-r--r--checker/safe_typing.ml2
-rw-r--r--checker/safe_typing.mli2
-rw-r--r--checker/subtyping.ml2
-rw-r--r--checker/subtyping.mli2
-rw-r--r--checker/term.ml2
-rw-r--r--checker/type_errors.ml2
-rw-r--r--checker/type_errors.mli2
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/typeops.mli2
-rw-r--r--checker/validate.ml2
22 files changed, 0 insertions, 44 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 0a75f01375..0317416f30 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 9679 2007-02-24 15:22:07Z herbelin $ *)
-
open Pp
open Util
open Names
diff --git a/checker/checker.ml b/checker/checker.ml
index e15c37e670..9489dc94b7 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml 10153 2007-09-28 18:00:45Z glondu $ *)
-
open Pp
open Util
open System
diff --git a/checker/closure.ml b/checker/closure.ml
index c710df816e..054057d1ff 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml 9983 2007-07-12 17:15:22Z barras $ *)
-
open Util
open Pp
open Term
diff --git a/checker/closure.mli b/checker/closure.mli
index 260d159b3d..ada7ded1e3 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: closure.mli 9902 2007-06-21 17:01:21Z herbelin $ i*)
-
(*i*)
open Pp
open Names
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index de57c50a74..0b4c6fde39 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *)
-
open Util
open Names
open Univ
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index b920315ab5..12511df336 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: indtypes.mli 9831 2007-05-17 18:55:42Z herbelin $ i*)
-
(*i*)
open Names
open Univ
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 4faf99a907..54bf1bbe62 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductive.ml 10172 2007-10-04 13:02:03Z herbelin $ *)
-
open Util
open Names
open Univ
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 8e6d4ffb99..bd758772a9 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*)
-
(*i*)
open Names
open Term
diff --git a/checker/modops.ml b/checker/modops.ml
index ce2f07ab66..e6428d5ab4 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.ml 9872 2007-05-30 16:01:18Z soubiran $ i*)
-
(*i*)
open Util
open Pp
diff --git a/checker/modops.mli b/checker/modops.mli
index 4476013c67..fedcf32cbd 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
(*i*)
open Util
open Names
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 612e7562fa..776edb2436 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
-
open Util
open Names
open Term
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 81c93ee53f..02b856edcf 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reduction.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
-
(*i*)
open Term
open Environ
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 98534e08ca..e37ff370c0 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
-
open Pp
open Util
open Names
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 12fdbfce80..ded3fe47f0 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: safe_typing.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
(*i*)
open Names
open Term
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index ec1c908a60..9df49630c5 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
-
(*i*)
open Util
open Names
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 10842252e0..1b0ca5c167 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
diff --git a/checker/term.ml b/checker/term.ml
index 35ae1121e4..8d65bbe176 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
-
(* This module instantiates the structure of generic deBruijn terms to Coq *)
open Util
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index 7c01410559..bddda852d2 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
-
open Names
open Term
open Environ
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 0482f2f2a8..70971faa4c 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
-
(*i*)
open Names
open Term
diff --git a/checker/typeops.ml b/checker/typeops.ml
index e5cf6a6d6d..1007c8971c 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
-
open Util
open Names
open Univ
diff --git a/checker/typeops.mli b/checker/typeops.mli
index de160a79b8..d554af0262 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeops.mli 9427 2006-12-11 18:46:35Z bgregoir $ i*)
-
(*i*)
open Names
open Term
diff --git a/checker/validate.ml b/checker/validate.ml
index ab17aa7f82..d3d2ecb603 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(* This module defines validation functions to ensure an imported
value (using input_value) has the correct structure. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 12:15:42 +0000