diff options
| author |  mrmr1993 <mr_1993@hotmail.co.uk> | 2018-03-03 14:38:43 +0000 |
|---|---|---|
| committer | mrmr1993 <mr_1993@hotmail.co.uk> | 2018-03-05 14:46:31 +0000 |
| commit | b88790fc8d473af4afd8dd59af61c137068e0376 (patch) | |
| tree | c7913f8da91a581b0fd88ec950bdb1b8b1be379b /plugins/ssr/ssrparser.ml4 | |
| parent | 5fda90cfe7ad79ee4e32681643b40d9fd0e573ee (diff) | |
Separate vim/emacs fold markers from ocamldoc comments
ocamldoc chokes on the markers {{{ and }}} because { and } are part of
its syntax
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 70f73c1fe..2bed8b624 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint | [ ] -> [ nohint ] END -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) @@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr let old_tac = V82.tactic -(** Name generation {{{ *******************************************************) +(** Name generation *)(* {{{ *******************************************************) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) @@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag) (* We must not anonymize context names discharged by the "in" tactical. *) -(** Tactical extensions. {{{ **************************************************) +(** Tactical extensions. *)(* {{{ **************************************************) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) |