aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ca64a856e..2b1c9da35 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1147,6 +1147,7 @@ let bind_eq = function
| (Name _,Name _) -> true
| _ -> false
+(* TODO: Fix and CoFix also contain bound names *)
let eqop_mod_names = function
| OpLambda n0, OpLambda n1 -> bind_eq (n0,n1)
| OpProd n0, OpProd n1 -> bind_eq (n0,n1)