diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 72205e2bbc..c424fe1226 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1217,7 +1217,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) if Array.for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined') + Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') rels_params then l := param::!l |