diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /parsing/pcoq.mli | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 44a3686e..525727ce 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 10987 2008-05-26 12:28:36Z herbelin $ i*) +(*i $Id: pcoq.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) open Util open Names @@ -188,7 +188,7 @@ module Tactic : val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e - val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e + val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e val tactic_expr : raw_tactic_expr Gram.Entry.e val binder_tactic : raw_tactic_expr Gram.Entry.e @@ -229,7 +229,7 @@ val find_position : val synchronize_level_positions : unit -> unit -val register_empty_levels : bool -> Compat.token Gramext.g_symbol list -> +val register_empty_levels : bool -> int list -> (Gramext.position option * Gramext.g_assoc option * string option * Gramext.g_assoc option) list |