aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 14:38:43 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:46:31 +0000
commitb88790fc8d473af4afd8dd59af61c137068e0376 (patch)
treec7913f8da91a581b0fd88ec950bdb1b8b1be379b /plugins/ssrmatching
parent5fda90cfe7ad79ee4e32681643b40d9fd0e573ee (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/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 1f1a63dac..62c35d6df 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -70,7 +70,7 @@ let _ =
Goptions.optwrite = debug }
let pp s = !pp_ref s
-(** Utils {{{ *****************************************************************)
+(** Utils *)(* {{{ *****************************************************************)
let env_size env = List.length (Environ.named_context env)
let safeDestApp c =
match kind c with App (f, a) -> f, a | _ -> c, [| |]
@@ -179,7 +179,7 @@ let nf_evar sigma c =
(* }}} *)
-(** Profiling {{{ *************************************************************)
+(** Profiling *)(* {{{ *************************************************************)
type profiler = {
profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
reset : unit -> unit;