diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 /lib | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
syntaxe AST Inversion + commentaires ocamlweb autour de $
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/bij.mli | 2 | ||||
| -rw-r--r-- | lib/bstack.mli | 2 | ||||
| -rw-r--r-- | lib/dyn.mli | 2 | ||||
| -rw-r--r-- | lib/edit.mli | 2 | ||||
| -rw-r--r-- | lib/gmap.mli | 2 | ||||
| -rw-r--r-- | lib/gmapl.mli | 2 | ||||
| -rw-r--r-- | lib/gset.mli | 2 | ||||
| -rw-r--r-- | lib/hashcons.mli | 2 | ||||
| -rw-r--r-- | lib/options.mli | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | lib/pp_control.mli | 2 | ||||
| -rw-r--r-- | lib/profile.mli | 2 | ||||
| -rw-r--r-- | lib/stamps.mli | 2 | ||||
| -rw-r--r-- | lib/system.mli | 2 | ||||
| -rw-r--r-- | lib/tlm.mli | 2 | ||||
| -rw-r--r-- | lib/util.mli | 2 |
16 files changed, 16 insertions, 16 deletions
diff --git a/lib/bij.mli b/lib/bij.mli index 65bae1eec..7e6d23e82 100644 --- a/lib/bij.mli +++ b/lib/bij.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Bijections. *) diff --git a/lib/bstack.mli b/lib/bstack.mli index d1f9ae387..fc646f1a4 100644 --- a/lib/bstack.mli +++ b/lib/bstack.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Bounded stacks. If the depth is [None], then there is no depth limit. *) diff --git a/lib/dyn.mli b/lib/dyn.mli index 2f2bb7b80..2c0587ee6 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Dynamics. Use with extreme care. Not for kids. *) diff --git a/lib/edit.mli b/lib/edit.mli index 5926456f0..c86022e44 100644 --- a/lib/edit.mli +++ b/lib/edit.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* The type of editors. * An editor is a finite map, ['a -> 'b], which knows how to apply diff --git a/lib/gmap.mli b/lib/gmap.mli index 908bad1bc..a73bdba51 100644 --- a/lib/gmap.mli +++ b/lib/gmap.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Maps using the generic comparison function of ocaml. Same interface as the module [Map] from the ocaml standard library. *) diff --git a/lib/gmapl.mli b/lib/gmapl.mli index c3a55e8c1..23c77851b 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Maps from ['a] to lists of ['b]. *) diff --git a/lib/gset.mli b/lib/gset.mli index 645a29cad..125fbe442 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Sets using the generic comparison function of ocaml. Same interface as the module [Set] from the ocaml standard library. *) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 9665e1a86..07dd8bc2b 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Generic hash-consing. *) diff --git a/lib/options.mli b/lib/options.mli index 25c194106..d36c6a467 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Global options of the system. *) diff --git a/lib/pp.mli b/lib/pp.mli index 8906616ac..96ef3d3de 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp_control diff --git a/lib/pp_control.mli b/lib/pp_control.mli index 6c92849a7..b6d6132e0 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Parameters of pretty-printing. *) diff --git a/lib/profile.mli b/lib/profile.mli index 893bf07b9..6ba6a4489 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Profiling. *) diff --git a/lib/stamps.mli b/lib/stamps.mli index 1eb624d57..40a83feb6 100644 --- a/lib/stamps.mli +++ b/lib/stamps.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Time stamps. *) diff --git a/lib/system.mli b/lib/system.mli index 71dff73c3..a91562cea 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*s Files and load paths. Load path entries remember the original root given by the user. For efficiency, we keep the full path (field diff --git a/lib/tlm.mli b/lib/tlm.mli index 44a2adc8b..f04639750 100644 --- a/lib/tlm.mli +++ b/lib/tlm.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Tries. This module implements a data structure [('a,'b) t] mapping lists of values of type ['a] to sets (as lists) of values of type ['b]. *) diff --git a/lib/util.mli b/lib/util.mli index 1cb05ad6f..fce150e80 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp |