diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3998d71b..1fe8c122 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 8926 2006-06-08 20:23:17Z herbelin $ i*) +(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*) open Util open Names @@ -184,6 +184,7 @@ module Tactic : val simple_intropattern : Genarg.intro_pattern_expr 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 val tactic : raw_tactic_expr Gram.Entry.e val tactic_eoi : raw_tactic_expr Gram.Entry.e end @@ -196,6 +197,13 @@ module Vernac_ : val command : vernac_expr Gram.Entry.e val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e + + (* MMode *) + + val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e + + (*/ MMode *) + val vernac_eoi : vernac_expr Gram.Entry.e end |