diff options
| author | herbelin | 2011-05-26 15:36:59 +0000 |
|---|---|---|
| committer | herbelin | 2011-05-26 15:36:59 +0000 |
| commit | d6e6c0fa15a6b1e08b8b8707ec75b6a53b1e1b3d (patch) | |
| tree | b9aacba409750fd2084230e0be7fd23fdd9edaf9 /dev/base_include | |
| parent | deb4df6668b6b1ecb6b6bb2164dddc29b1215bf1 (diff) | |
Partial fix for accepting bound variables with same name as implicit
parameters of inductive types when these variables cannot bind the
conclusion of the inductive type (done for "return" predicates but
still to be done for non strictly positive binding occurrence, as e.g. in
"Set Implicit Arguments. Inductive I A:A->Prop:=C a:(forall A, A)->I a."
which should morally be accepted but is not).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14159 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions