diff options
| author | Pierre-Marie Pédrot | 2016-07-13 17:00:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-07-13 17:00:25 +0200 |
| commit | 9f003b933c2a3504683a84ed817021659e80bc8f (patch) | |
| tree | 4e9636ca44aed009d2274b03e64313c770a8b026 /interp/notation_ops.mli | |
| parent | 7217d14466bf900ec0353b6bbcb7e4d4b78ec2bf (diff) | |
| parent | 45250332a1e65d434432940a468312f2ab18a2e8 (diff) | |
Merge branch 'v8.6'
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 0f1b1a8756..854e222e30 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]} *) |