diff options
Diffstat (limited to 'gramlib/ploc.mli')
| -rw-r--r-- | gramlib/ploc.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli deleted file mode 100644 index fad883e11a..0000000000 --- a/gramlib/ploc.mli +++ /dev/null @@ -1,11 +0,0 @@ -(* camlp5r *) -(* ploc.mli,v *) -(* Copyright (c) INRIA 2007-2017 *) - -val make_unlined : int * int -> Loc.t - (** [Ploc.make_unlined] is like [Ploc.make] except that the line number - is not provided (to be used e.g. when the line number is unknown. *) - -val dummy : Loc.t - (** [Ploc.dummy] is a dummy location, used in situations when location - has no meaning. *) |