diff options
| -rw-r--r-- | pretyping/matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 0b1e05de98..d034bfae06 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -65,7 +65,7 @@ let add_binders na1 na2 (names,terms as subst) = | Name id1, Name id2 -> if List.mem_assoc id1 names then (Flags.if_verbose Pp.warning - ("Collision between bound variables of name"^string_of_id id1); + ("Collision between bound variables of name "^string_of_id id1); (names,terms)) else (if List.mem_assoc id1 terms then |