aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/clenvtac.mli2
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof.ml2
-rw-r--r--proofs/proof.mli2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--proofs/proof_type.ml2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/proofview.ml2
-rw-r--r--proofs/proofview.mli2
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/redexpr.mli2
-rw-r--r--proofs/refiner.ml2
-rw-r--r--proofs/refiner.mli2
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--proofs/tacmach.ml2
-rw-r--r--proofs/tacmach.mli2
-rw-r--r--proofs/tactic_debug.ml2
-rw-r--r--proofs/tactic_debug.mli2
29 files changed, 0 insertions, 58 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 35db5e6ed1..0068921895 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index a97b85ed94..afda6d9315 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.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/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f977768bd6..a8162cc5a4 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 02bf86641b..760a79d4ce 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.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/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6dfbbdc121..cd05cdcd25 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Util
open Names
open Term
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index ff986f3e66..ca3bd1e802 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Names
open Term
open Environ
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a9202318df..4e5905d831 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -6,8 +6,6 @@
(* * GNU Lesscer General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Term
(* This module implements the abstract interface to goals *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 49e3c9b1ae..c7f6957662 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: goal.mli aspiwack $ *)
-
(* This module implements the abstract interface to goals *)
type goal
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7c092bb66e..93de5be692 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/proofs/logic.mli b/proofs/logic.mli
index eec3de7303..39f69ad127 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.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/proofs/pfedit.ml b/proofs/pfedit.ml
index 6da73c2f67..153354c920 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 47b741f5d5..194dd14648 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Util
open Pp
open Names
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0c298cc630..35f7b4f023 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(* Module defining the last essential tiles of interactive proofs.
The features of the Proof module are undoing and focusing.
A proof is a mutable object, it contains a proofview, and some information
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 2b1c3f5c20..5e1120f9c0 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: proof.mli aspiwack $ *)
-
(* Module defining the last essential tiles of interactive proofs.
The features of the Proof module are undoing and focusing.
A proof is a mutable object, it contains a proofview, and some information
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 420ff84325..87a8d8d1e2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(***********************************************************************)
(* *)
(* This module defines the global proof environment *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 84a61c755a..40908dfc44 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(***********************************************************************)
(* *)
(* This module defines the global proof environment *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2fffa39527..55a73c608b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ *)
-
(*i*)
open Environ
open Evd
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 7d88753021..8def611129 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Environ
open Evd
open Names
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a08941df03..427a8d6136 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(* The proofview datastructure is a pure datastructure underlying the notion
of proof (namely, a proof is a proofview which can evolve and has safety
mechanisms attached).
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index cd5520d4e5..dc205f538a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: proofview.mli aspiwack $ *)
-
(* The proofview datastructure is a pure datastructure underlying the notion
of proof (namely, a proof is a proofview which can evolve and has safety
mechanisms attached).
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index b0a01caa7b..b300977317 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 199130b5f3..581ee1dc9b 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Names
open Term
open Closure
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ffb18f2655..1abd762538 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Term
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9585600446..be4dbd9a5f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Term
open Sign
open Evd
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b56e5184e0..4cec846fd3 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
open Names
open Topconstr
open Libnames
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6dbdf17cb8..8104295199 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
open Pp
open Util
open Names
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cf704d101c..9e0ca2a3d6 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.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/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index f6b2ce4525..a3fa59e8a6 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
open Names
open Constrextern
open Pp
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index f275403152..ac3bf493a9 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,8 +6,6 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-(*i $Id$ i*)
-
open Environ
open Pattern
open Evd
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 12:23:07 +0000