aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-21 17:24:37 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-21 17:24:37 +0000
commitb7af7027d15afa2dee1695792a2658f0df392956 (patch)
treebebcce8f9fbb305d0bd9aa203ec843677665323b /translate
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 'translate')
-rw-r--r--translate/ppconstrnew.mli2
-rw-r--r--translate/pptacticnew.mli2
-rw-r--r--translate/ppvernacnew.mli2
3 files changed, 3 insertions, 3 deletions
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 09e21e1ce..9ebdbfb8e 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
open Pp
open Environ
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index 5f89662c7..b2e8942ad 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
open Pp
open Genarg
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli
index bcd2a7e2b..1b1639939 100644
--- a/translate/ppvernacnew.mli
+++ b/translate/ppvernacnew.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
open Pp
open Genarg