aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrextern.mli2
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/coqlib.mli2
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli3
-rw-r--r--interp/genarg.ml2
-rw-r--r--interp/genarg.mli2
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/implicit_quantifiers.mli2
-rw-r--r--interp/modintern.ml2
-rw-r--r--interp/modintern.mli2
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation.mli2
-rw-r--r--interp/ppextend.ml2
-rw-r--r--interp/ppextend.mli2
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/smartlocate.ml2
-rw-r--r--interp/smartlocate.mli2
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--interp/syntax_def.mli2
-rw-r--r--interp/topconstr.ml2
-rw-r--r--interp/topconstr.mli2
26 files changed, 0 insertions, 53 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 99c627a95..fec00c65a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(*i*)
open Pp
open Util
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ac9ed5714..ac3a38833 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Util
open Names
open Term
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2b16023f0..ecaba603d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Flags
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4ba2bc587..bf28e0850 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Names
open Term
open Sign
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 1ca82e35c..6cfe1421f 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Util
open Pp
open Names
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5148461a9..a80e749d3 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Names
open Libnames
open Nametab
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 702c509dc..9dfa808c7 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(* Dump of globalization (to be used by coqdoc) *)
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 7235fe172..7efa6f1e0 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -6,9 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(** {% $ %}Id: dumpglob.mli 11252 2008-07-24 11:16:48Z notin {% $ %} *)
-
-
val open_glob_file : string -> unit
val close_glob_file : unit -> unit
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 241c92582..e5950cd8d 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 50abd351e..984f479fb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Util
open Names
open Term
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d5894b208..89ec5f1f1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
(*i*)
open Names
open Decl_kinds
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 7362d7de5..ac610fe78 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Names
open Decl_kinds
open Term
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 049745ca9..094b723e0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/interp/modintern.mli b/interp/modintern.mli
index e025447b5..5dacfd070 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Declarations
open Environ
open Entries
diff --git a/interp/notation.ml b/interp/notation.ml
index 794169a37..bfa86b50f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(*i*)
open Util
open Pp
diff --git a/interp/notation.mli b/interp/notation.mli
index 91f262b48..224fb1d45 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Util
open Pp
open Bigint
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index a4142d694..16d0537b9 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ *)
-
(*i*)
open Pp
open Util
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 984696cda..19ca913e8 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Pp
open Names
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 9d8412825..700fcd1e3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
(* Reserved names *)
open Util
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 4cc2eff5a..e53ad8365 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Util
open Names
open Rawterm
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index faad3c50a..424e7cc1e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -11,8 +11,6 @@
(* This file provides high-level name globalization functions *)
-(* $Id:$ *)
-
(* *)
open Pp
open Util
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index b505e7db7..0cd261a82 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(** {% $ %}Id:{% $ %} *)
-
open Util
open Names
open Libnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 245ed0f50..334135eaf 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Util
open Pp
open Names
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 6b57b497a..019067608 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Util
open Names
open Topconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c0b624110..5fade008c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(*i*)
open Pp
open Util
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 02e6d1eeb..2b9506747 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Pp
open Util
open Names
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 01:52:04 +0000