diff options
| author | Maxime Dénès | 2017-12-14 17:22:07 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-14 17:22:07 +0100 |
| commit | 84e570d7c532f16104157b806da714906fdf26b3 (patch) | |
| tree | f020dcc0e2e599ae02d045240a076900595ea056 /interp/constrexpr_ops.ml | |
| parent | 8f936f45ab95fdb72f1d596fc621faa39ddcb95e (diff) | |
| parent | 7720a01ceb7d00bc16cd96d99c27bc7696388899 (diff) | |
Merge PR #978: In printing, experimenting factorizing "match" clauses with same right-hand side.
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8b78a91b5b..7cc8de85d2 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -188,7 +188,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) = Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = - List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && + List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = @@ -260,7 +260,6 @@ let local_binders_loc bll = match bll with (* Legacy functions *) let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y let is_constructor id = try Globnames.isConstructRef @@ -292,8 +291,7 @@ let ids_of_pattern = let ids_of_pattern_list = List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) + (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty let ids_of_cases_indtype p = @@ -571,7 +569,7 @@ let expand_binders ?loc mkC bl c = let c = CAst.make ?loc @@ CCases (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) + [(Loc.tag ?loc:loc1 ([[p]], c))]) in (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) in |