diff options
| author | pboutill | 2011-07-15 11:40:22 +0000 |
|---|---|---|
| committer | pboutill | 2011-07-15 11:40:22 +0000 |
| commit | 5dbfe3e0ecd581cde2d6bd11210cf8702a3daf30 (patch) | |
| tree | 43d51fa6d59a8ba119007661f177f471d1ab43ae | |
| parent | d457278382c722abb4684c3689e72bd42f9c0038 (diff) | |
A correct error message for an unknown field in a record definition
fix bug 2571.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14276 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 423bff7992..a7e4648671 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -956,7 +956,7 @@ let sort_fields mode loc l completer = try Recordops.find_projection (global_reference_of_reference refer) with Not_found -> - user_err_loc (loc, "intern", str"Not a projection") + user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection") in (* elimination of the first field from the projections *) let rec build_patt l m i acc = @@ -996,6 +996,10 @@ let sort_fields mode loc l completer = | [] -> accpatt | p::q-> let refer, patt = p in + let glob_refer = try global_reference_of_reference refer + with |Not_found -> + user_err_loc (loc_of_reference refer, "intern", + str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in let rec add_patt l acc = match l with | [] -> @@ -1003,7 +1007,7 @@ let sort_fields mode loc l completer = (loc, "", str "This record contains fields of different records.") | (i, a) :: b-> - if global_reference_of_reference refer = a + if glob_refer = a then (i,List.rev_append acc l) else add_patt b ((i,a)::acc) in |