diff options
| author | Enrico Tassi | 2015-03-30 11:30:53 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-03-30 11:30:53 +0200 |
| commit | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (patch) | |
| tree | cc39f942a75fd621633b1ac0999bbe4b3918fcfd /interp/notation_ops.mli | |
| parent | 224d3b0e8be9b6af8194389141c9508504cf887c (diff) | |
| parent | 41e4725805588b3fffdfdc0cd5ee6859de1612b5 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'interp/notation_ops.mli')
| -rw-r--r-- | interp/notation_ops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 7283ed6f12..c6770deea2 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -25,6 +25,8 @@ val ldots_var : Id.t (** FIXME: nothing to do here *) val eq_glob_constr : glob_constr -> glob_constr -> bool +val eq_notation_constr : notation_constr -> notation_constr -> bool + (** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> |