diff options
| author | herbelin | 2005-01-21 17:24:37 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-21 17:24:37 +0000 |
| commit | b7af7027d15afa2dee1695792a2658f0df392956 (patch) | |
| tree | bebcce8f9fbb305d0bd9aa203ec843677665323b /kernel | |
| parent | accec4fc961d85ef21e73e690dedc36ce4c25f46 (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 'kernel')
| -rw-r--r-- | kernel/conv_oracle.mli | 2 | ||||
| -rw-r--r-- | kernel/esubst.mli | 2 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 2 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/vconv.mli | 8 |
5 files changed, 12 insertions, 4 deletions
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 7fc3dabcda..6e09ce6f08 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Names diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 9f795d8577..cd9c169070 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*s Compact representation of explicit relocations. \\ [ELSHFT(l,n)] == lift of [n], then apply [lift l]. diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 89491e2f91..0a3220293b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -8,7 +8,7 @@ (*i $Id$ i*) -(*s Mod_subst *) +(*s [Mod_subst] *) open Names open Term diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index cfcc7bd585..702e79ecc3 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Declarations diff --git a/kernel/vconv.mli b/kernel/vconv.mli index fa6026509f..4aed5d05fa 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (*i*) open Names open Term |