diff options
author | 2010-04-10 15:53:28 +0000 | |
---|---|---|
committer | 2010-04-10 15:53:28 +0000 | |
commit | 1f9670eb2e372ac02382b16be481e0bbda2d4691 (patch) | |
tree | 86c6bf00c23f6b72c9aeb429e359b195afdd6e67 | |
parent | c6b7976677b943fbe8fa88a3e01e4b549e95ea90 (diff) |
Partially fixed bug #2231 (an inductive parameter name was internally
used as a binding name in the return predicate of a Let/If case
analysis causing a surprising error message; solved the problem by not
checking for this kind of internal variables when the return predicate
is anyway not given by the user; ideally, it should be detected that
in the arguments of the inductive type, the parameter names can be
reused w/o provoking captures - which are bad if the argument is
implicit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12917 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | interp/constrintern.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index dac435e7f..2b16023f0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -871,8 +871,7 @@ let locate_if_isevar loc na = function let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = if List.mem id indnames then errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ - pr_id id ++ strbrk " must not be used as a bound variable in the type \ -of its constructor.") + pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function | Anonymous -> @@ -1175,15 +1174,17 @@ let internalise sigma globalenv env allow_patvar lvar c = | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in - let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = Option.map (intern_type env'') po in + let p' = Option.map (fun p -> + let env'' = List.fold_left (push_name_env lvar) env ids in + intern_type env'' p) po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in - let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = Option.map (intern_type env'') po in + let p' = Option.map (fun p -> + let env'' = List.fold_left (push_name_env lvar) env ids in + intern_type env'' p) po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) |