diff options
| author | Pierre-Marie Pédrot | 2015-03-24 16:01:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-03-24 16:50:59 +0100 |
| commit | 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 (patch) | |
| tree | 280cfc3f316502cf6b4249f4cafe8c8c871d748c /interp/notation_ops.mli | |
| parent | d65eaaaa8cb311a0344a584df7a4b405034780b9 (diff) | |
Fixing equality of notation_constrs. Fixes bug #4136.
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 -> |