diff options
| author | herbelin | 2003-11-17 11:07:30 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-17 11:07:30 +0000 |
| commit | 0679c28226c42aad41af8b68dbbfb7f55aa0ef6a (patch) | |
| tree | 9239df408a7f8a4ae717b132bb83e6a620c7a02e | |
| parent | 58102e06630d174655116d03a2281e730bf8e914 (diff) | |
Un ident filtre est liant seulement si une variable deja liee (sinon bug dans les Notation avec Cases - en particulier)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4926 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 44a0d3b1f7..b1ff0d6236 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -650,8 +650,9 @@ let internalise sigma env allow_soapp lvar c = | _ -> RApp (loc, c, args)) | CCases (loc, (po,rtnpo), tms, eqns) -> let tms,rtnids = List.fold_right (fun (tm,indnalo) (inds,ids) -> - let typ,ids = intern_return_type env indnalo ids in - (intern env tm,ref typ)::inds,ids) + let tm' = intern env tm in + let typ,ids = intern_return_type env indnalo tm' ids in + (tm',ref typ)::inds,ids) tms ([],ids) in let rtnpo = option_app (intern_type (rtnids,tmp_scope,scopes)) rtnpo in @@ -714,7 +715,7 @@ let internalise sigma env allow_soapp lvar c = let env_ids = List.fold_right Idset.add eqn_ids ids in (loc, eqn_ids,pl,intern (env_ids,tmp_scope,scopes) rhs) - and intern_return_type (_,_,scopes as env) (na,t) ids = + and intern_return_type (vars,_,scopes as env) (na,t) tm ids = let ids,typ = match t with | Some t -> let tids = names_of_cases_indtype t in @@ -734,6 +735,9 @@ let internalise sigma env allow_soapp lvar c = end | None -> ids, None in + let na = match tm, na with + | RVar (_,id), Anonymous when Idset.mem id vars -> Name id + | _ -> na in (na,typ), name_fold Idset.add na ids and iterate_prod loc2 env ty body = function |