aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml44
-rw-r--r--plugins/ssrmatching/ssrmatching.mli2
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 5ed5e47f8..33b18001c 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;
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index cd5676f28..07d0f9757 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -74,7 +74,7 @@ val interp_cpattern :
pattern
(** The set of occurrences to be matched. The boolean is set to true
- * to signal the complement of this set (i.e. {-1 3}) *)
+ * to signal the complement of this set (i.e. \{-1 3\}) *)
type occ = (bool * int list) option
(** [subst e p t i]. [i] is the number of binders