From 8eccc93ddcd94eda6b027d62d882ea256fea58ba Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 11 Jul 2016 16:41:35 +0200 Subject: removing ocamldoc-related syntax errors --- interp/notation_ops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 0f1b1a875..854e222e3 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -23,7 +23,7 @@ val subst_interpretation : val ldots_var : Id.t -(** {5 Translation back and forth between [glob_constr] and [notation_constr] *) +(** {5 Translation back and forth between [glob_constr] and [notation_constr]} *) (** Translate a [glob_constr] into a notation given the list of variables bound by the notation; also interpret recursive patterns *) @@ -40,7 +40,7 @@ val glob_constr_of_notation_constr_with_binders : Loc.t -> val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr -(** {5 Matching a notation pattern against a [glob_constr] *) +(** {5 Matching a notation pattern against a [glob_constr]} *) (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) @@ -64,5 +64,5 @@ val match_notation_constr_ind_pattern : ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (int * cases_pattern list) -(** {5 Matching a notation pattern against a [glob_constr] *) +(** {5 Matching a notation pattern against a [glob_constr]} *) -- cgit v1.2.3