diff options
| author | aspiwack | 2011-04-06 13:40:39 +0000 |
|---|---|---|
| committer | aspiwack | 2011-04-06 13:40:39 +0000 |
| commit | bdac8f996a89701f74a5fcb649ec12bc3aaa9d07 (patch) | |
| tree | 00be772e7409ed6c56581550a830ebd3bf1a29b4 /plugins/decl_mode | |
| parent | 7a7a09378e492b5b2dc87e3a8e502e842ca1faf5 (diff) | |
Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.
Patch submitted by Tom Prince.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 63d46e2608..a133089f8f 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -397,7 +397,7 @@ GLOBAL: proof_instr; | i = intro_step -> i ]] ; proof_instr : - [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]] + [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]] ; END;; |