diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-11 16:41:35 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-12 10:08:32 +0200 |
| commit | 8eccc93ddcd94eda6b027d62d882ea256fea58ba (patch) | |
| tree | 451b114244a7a64585afbaf00d014d05ef935326 /interp/notation_ops.mli | |
| parent | 8cd4ad9e333169c2a9c222cb34a2199ccba56fa4 (diff) | |
removing ocamldoc-related syntax errors
Diffstat (limited to 'interp/notation_ops.mli')
| -rw-r--r-- | interp/notation_ops.mli | 6 |
1 files 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]} *) |