diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 21:45:47 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 21:45:47 +0000 |
| commit | 1c450e282d8e6ae37f687c545776939f2d975cf3 (patch) | |
| tree | fd0f3796a07516776016234f162374942db0b1d9 /interp | |
| parent | bfc03c53882d7334e4fb327362c354397a8462ba (diff) | |
Correct enormous bug in interpretation of generalized binders: it simply
dropped all bindings appearing before it :) Bug found by Marc Lasson.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ef7ad36f1..dd94bf42d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -717,7 +717,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl) ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl)) (env,bl) nal | Generalized (b,b',t) -> - intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty) + let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in + env, b @ bl) | LocalRawDef((loc,na),def) -> ((name_fold Idset.add na ids,unb,ts,sc), (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) |