diff options
| author | herbelin | 2006-09-24 17:23:00 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-24 17:23:00 +0000 |
| commit | bd07a69adf72e0b888f94a0379691afcf9183975 (patch) | |
| tree | d220763565bbfb59e0a14a4fb28b95f004bb5723 | |
| parent | 97187ce18aca111c0cb1d275eec33d20854a9b53 (diff) | |
Tentative d'amélioration du message d'erreur en cas de paramètre non laissé
implicite dans une clause "in".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9174 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 68a60b16f4..bdd9fa32da 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -118,6 +118,11 @@ let error_bad_inductive_type loc = user_err_loc (loc,"",str "This should be an inductive type applied to names or \"_\"") +let error_inductive_parameter_not_implicit loc = + user_err_loc (loc,"", str + ("The parameters of inductive types do not bind in\n"^ + "the 'return' clauses; they must be replaced by '_' in the 'in' clauses.")) + (**********************************************************************) (* Dump of globalization (to be used by coqdoc) *) let token_number = ref 0 @@ -973,13 +978,12 @@ let internalise sigma globalenv env allow_soapp lvar c = if List.length l <> nindargs then error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function - | RHole _ -> Anonymous + | RHole loc -> Anonymous | RVar (_,id) -> Name id | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in let parnal,realnal = list_chop nparams nal in if List.exists ((<>) Anonymous) parnal then - user_err_loc (loc,"", - str "The parameters of inductive type must be implicit"); + error_inductive_parameter_not_implicit loc; realnal, Some (loc,ind,nparams,realnal) | None -> [], None in |