diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 14:55:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:05 +0100 |
| commit | 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 (patch) | |
| tree | 7dc6f685aa30f0b5bb3da704f1d96c7060eb19e5 /interp | |
| parent | 00bfd6fa443232bc908cfa13553e2fa1cf783ffa (diff) | |
In printing notations with "match", reasoning up to the order of clauses.
Diffstat (limited to 'interp')
| -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 602271bf6..e68e8dd97 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1163,7 +1163,7 @@ let rec match_ inner u alp metas sigma a1 a2 = let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_in u alp metas s tm1 tm2) sigma tml1 tml2 in - List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 + List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2 | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) when Int.equal (List.length nal1) (List.length nal2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in |