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/ssrvernac.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/ssrvernac.ml4')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index f37452613..e3941c1c5 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. {{{ ************) +(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************) (* Syntax: *) (* if <term> is <pattern> then ... else ... *) @@ -127,7 +127,7 @@ GEXTEND Gram END (* }}} *) -(** Vernacular commands: Prenex Implicits and Search {{{ **********************) +(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -461,7 +461,7 @@ END (* }}} *) -(** View hint database and View application. {{{ ******************************) +(** View hint database and View application. *)(* {{{ ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) |