diff options
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e765fa8cd..5b5775d1a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1300,7 +1300,7 @@ let check_projection isproj nargs r = (try let n = Recordops.find_projection_nparams ref + 1 in if not (Int.equal nargs n) then - user_err_loc (loc,"",str "Projection has not the right number of explicit parameters."); + user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters."); with Not_found -> user_err_loc (loc,"",pr_global_env Id.Set.empty ref ++ str " is not a registered projection.")) |