diff options
| author | Hugo Herbelin | 2016-07-19 16:20:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-19 16:20:23 +0200 |
| commit | 522bcd72a567a3ae29162519a9a9736581367251 (patch) | |
| tree | 6e382379450e80728593576d2a184de3c642e6c4 | |
| parent | f7ae4e6433e44a0b3a838847c58ab72ffffa3d48 (diff) | |
Complementing previous commit on fixes for printing binding patterns.
| -rw-r--r-- | printing/ppconstr.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index dab97d603b..935e2d076e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -379,7 +379,9 @@ end) = struct if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) | CProdN (loc,[],c) -> extract_prod_binders c - | CProdN (loc,[[_,Name id],bk,t],CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) -> + | CProdN (loc,[[_,Name id],bk,t], + CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) + when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in LocalPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> @@ -393,7 +395,9 @@ end) = struct if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) | CLambdaN (loc,[],c) -> extract_lam_binders c - | CLambdaN (loc,[[_,Name id],bk,t],CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) -> + | CLambdaN (loc,[[_,Name id],bk,t], + CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) + when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in LocalPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> |