From 1f9670eb2e372ac02382b16be481e0bbda2d4691 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 10 Apr 2010 15:53:28 +0000
Subject: 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
---
 interp/constrintern.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index dac435e7fd..2b16023f0d 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))
-- 
cgit v1.2.3