From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- interp/notation_ops.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'interp/notation_ops.mli') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 7283ed6f..c6770dee 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 -> -- cgit v1.2.3