diff --git a/src/core/inductivity.ml b/src/core/inductivity.ml
index 243667652..2e827dabb 100644
--- a/src/core/inductivity.ml
+++ b/src/core/inductivity.ml
@@ -14,3 +14,5 @@ let max ind1 ind2 =
 let is_not_inductive = ( = ) not_inductive
 
 let is_inductive = ( = ) inductive
+
+let equal = ( = )
diff --git a/src/core/inductivity.mli b/src/core/inductivity.mli
index 4a46b2991..ce8d6c5da 100644
--- a/src/core/inductivity.mli
+++ b/src/core/inductivity.mli
@@ -24,3 +24,7 @@ val is_not_inductive : t -> bool
 
 (** [is_inductive ind] is [true] if and only if [ind] is [Inductive]. *)
 val is_inductive : t -> bool
+
+(** [equal p1 p2] is [true] if and only if [p1] and [p2] are both [Explicit]
+    or [Implicit]. *)
+val equal : t -> t -> bool
diff --git a/src/core/plicity.ml b/src/core/plicity.ml
index 772a5e962..6e169d83d 100644
--- a/src/core/plicity.ml
+++ b/src/core/plicity.ml
@@ -14,3 +14,5 @@ let max p1 p2 =
 let is_explicit = ( = ) explicit
 
 let is_implicit = ( = ) implicit
+
+let equal = ( = )
diff --git a/src/core/plicity.mli b/src/core/plicity.mli
index 5eb9d9d07..596c5b463 100644
--- a/src/core/plicity.mli
+++ b/src/core/plicity.mli
@@ -30,3 +30,7 @@ val is_explicit : t -> bool
 
 (** [is_implicit p] is [true] if and only if [p] is [Implicit]. *)
 val is_implicit : t -> bool
+
+(** [equal p1 p2] is [true] if and only if [p1] and [p2] are both [Explicit]
+    or [Implicit]. *)
+val equal : t -> t -> bool