diff options
Diffstat (limited to 'toplevel/vernacinterp.mli')
| -rw-r--r-- | toplevel/vernacinterp.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index e0c34dc9..7adc7493 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -6,18 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacinterp.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Tacexpr (*i*) (* Interpretation of extended vernac phrases. *) - + val disable_drop : exn -> exn val vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit -val overwriting_vinterp_add : +val overwriting_vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit val vinterp_init : unit -> unit |