aboutsummaryrefslogtreecommitdiff
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 99c627a956..fec00c65ad 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 ac9ed5714b..ac3a388332 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 2b16023f0d..ecaba603d2 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 4ba2bc5871..bf28e0850a 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 1ca82e35c8..6cfe1421f7 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 5148461a97..a80e749d30 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 702c509dc7..9dfa808c73 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 7235fe1729..7efa6f1e01 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 241c92582a..e5950cd8d6 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 50abd351e7..984f479fb7 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 d5894b208c..89ec5f1f11 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 7362d7de56..ac610fe78d 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 049745ca9f..094b723e08 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 e025447b55..5dacfd0700 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 794169a377..bfa86b50f2 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 91f262b488..224fb1d45b 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 a4142d6949..16d0537b98 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 984696cdab..19ca913e88 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 9d8412825f..700fcd1e3a 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 4cc2eff5ad..e53ad8365a 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 faad3c50a4..424e7cc1ef 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 b505e7db7a..0cd261a82e 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 245ed0f508..334135eaf4 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 6b57b497ad..0190676084 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 c0b624110a..5fade008cf 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 02e6d1eeb5..2b95067473 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.25.1) at 2026-05-10 22:44:24 +0000