diff options
| author | Maxime Dénès | 2018-02-28 10:00:31 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-28 10:00:31 +0100 |
| commit | 3a7a2b039761e6cd9aaff6be07e62c76a2781e40 (patch) | |
| tree | 7798dd7da6e8b2cfe648d976f5555b385225c9af /interp/notation_ops.ml | |
| parent | 374e105be93beb2e9353bedf5cdd700a26308ebd (diff) | |
| parent | 4e18be02a03ab478125aa6f08b30e738c3568572 (diff) | |
Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinite eta-expansion)
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c65f4785ef..9bc41a996b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1132,7 +1132,7 @@ let rec match_ inner u alp metas sigma a1 a2 = else f1,l1, f2, l2 in let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) - (match_in u alp metas sigma f1 f2) l1 l2 + (match_hd u alp metas sigma f1 f2) l1 l2 | GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) -> match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2 | GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) -> |