aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorherbelin2005-01-21 17:24:37 +0000
committerherbelin2005-01-21 17:24:37 +0000
commitb7af7027d15afa2dee1695792a2658f0df392956 (patch)
treebebcce8f9fbb305d0bd9aa203ec843677665323b /proofs
parentaccec4fc961d85ef21e73e690dedc36ce4c25f46 (diff)
Compatibilité ocamlweb pour cible doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r--proofs/redexpr.mli2
-rw-r--r--proofs/tacexpr.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index a0b7100b6b..7146f7f5e0 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
open Names
open Term
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 12fa2b950a..9889fcb0b9 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
open Names
open Topconstr