diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /parsing/pcoq.mli | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
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 |