From 26f47b04122e79b37bce0692e4d1f1559cfef700 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 2 Mar 2014 18:11:29 +0100 Subject: Adding an equality function over glob_constr --- pretyping/glob_ops.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'pretyping/glob_ops.mli') diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 4e8224879..5195b98c8 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -20,6 +20,10 @@ open Glob_term (** Equalities *) val glob_sort_eq : glob_sort -> glob_sort -> bool +val cases_pattern_eq : cases_pattern -> cases_pattern -> bool + +val glob_constr_eq : glob_constr -> glob_constr -> bool + (** Operations on [glob_constr] *) val cases_pattern_loc : cases_pattern -> Loc.t -- cgit v1.2.3