diff options
| author | xclerc | 2014-02-24 11:07:21 +0100 |
|---|---|---|
| committer | xclerc | 2014-02-24 11:07:21 +0100 |
| commit | c4370e5394cc9f678250150bd5bb407629b21913 (patch) | |
| tree | aba0aac4e01f5ca2d5e0a6e2a82638fa65dc67bf | |
| parent | 6b10edbe056f38d784258b6bf3ea4b8dc472e472 (diff) | |
Fix grammatical mistake in error message (bug #3238)
| -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 e765fa8cd6..5b5775d1a3 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.")) |