aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli2
-rw-r--r--interp/constrexpr_ops.ml8
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrintern.ml8
-rw-r--r--intf/constrexpr.ml2
-rw-r--r--parsing/g_constr.ml48
-rw-r--r--plugins/ssr/ssrvernac.ml46
-rw-r--r--pretyping/cases.ml6
-rw-r--r--printing/ppconstr.ml7
9 files changed, 24 insertions, 25 deletions
diff --git a/API/API.mli b/API/API.mli
index abbdf22b9..99ba3eea4 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2388,7 +2388,7 @@ sig
and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option
and branch_expr =
- (cases_pattern_expr list Loc.located list * constr_expr) Loc.located
+ (cases_pattern_expr list list * constr_expr) Loc.located
and binder_expr =
Names.Name.t Loc.located list * binder_kind * constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8b78a91b5..7cc8de85d 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
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bc8debd02..6704ed4b7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -967,7 +967,7 @@ and extern_local_binder scopes vars = function
(assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
- Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
+ Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl],
extern inctx scopes vars c)
and extern_notation (tmp_scope,scopes as allscopes) vars t = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 977146b2f..74ae32120 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -958,8 +958,11 @@ let rec has_duplicate = function
| [] -> None
| x::l -> if Id.List.mem x l then (Some x) else has_duplicate l
+let loc_of_multiple_pattern pl =
+ Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl))
+
let loc_of_lhs lhs =
- Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs))
+ Loc.merge_opt (loc_of_multiple_pattern (List.hd lhs)) (loc_of_multiple_pattern (List.last lhs))
let check_linearity lhs ids =
match has_duplicate ids with
@@ -1873,8 +1876,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern_local_binder_aux intern ntnvars env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
- and intern_multiple_pattern env n (loc,pl) =
+ and intern_multiple_pattern env n pl =
let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
+ let loc = loc_of_multiple_pattern pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns empty_alias idsl_pll
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index e0d2d7bf4..8bcdbcc0e 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -104,7 +104,7 @@ and case_expr = constr_expr (* expression that is being matched
* cases_pattern_expr option (* in-clause *)
and branch_expr =
- (cases_pattern_expr list Loc.located list * constr_expr) Loc.located
+ (cases_pattern_expr list list * constr_expr) Loc.located
and binder_expr =
Name.t Loc.located list * binder_kind * constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0cf96d487..db68a75e0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -267,17 +267,17 @@ GEXTEND Gram
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+ CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
| "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)])
| "if"; c=operconstr LEVEL "200"; po = return_type;
"then"; b1=operconstr LEVEL "200";
"else"; b2=operconstr LEVEL "200" ->
@@ -362,7 +362,7 @@ GEXTEND Gram
[ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
;
mult_pattern:
- [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ]
+ [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ]
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 3efb7b914..4f530a0ae 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
let no_ct = None, None and no_rt = None in
let aliasvar = function
- | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id)
+ | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id)
| _ -> None in
let mk_cnotype mp = aliasvar mp, None in
let mk_ctype mp t = aliasvar mp, Some t in
@@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in
GEXTEND Gram
GLOBAL: binder_constr;
ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]];
- ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]];
+ ssr_mpat: [[ p = pattern -> [[p]] ]];
ssr_dpat: [
[ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt
| mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt
| mp = ssr_mpat -> mp, no_ct, no_rt
] ];
ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]];
- ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
+ ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]];
binder_constr: [
[ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4f3669a2b..1207c967b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1566,11 +1566,9 @@ substituer après par les initiaux *)
(* builds the matrix of equations testing that each eqn has n patterns
* and linearizing the _ patterns.
- * Syntactic correctness has already been done in astterm *)
+ * Syntactic correctness has already been done in constrintern *)
let matx_of_eqns env eqns =
- let build_eqn (loc,(ids,lpat,rhs)) =
- let initial_lpat,initial_rhs = lpat,rhs in
- let initial_rhs = rhs in
+ let build_eqn (loc,(ids,initial_lpat,initial_rhs)) =
let avoid = ids_of_named_context_val (named_context_val env) in
let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
let rhs =
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2c03d7c8d..51735bc9e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -311,7 +311,6 @@ let tag_var = tag Tag.variable
let pr_patt = pr_patt mt
let pr_eqn pr (loc,(pl,rhs)) =
- let pl = List.map snd pl in
spc() ++ hov 4
(pr_with_comments ?loc
(str "| " ++
@@ -402,7 +401,7 @@ let tag_var = tag Tag.variable
| { v = CProdN ([],c) } ->
extract_prod_binders c
| { loc; v = CProdN ([[_,Name id],bk,t],
- { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) }
+ { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) }
when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
let bl,c = extract_prod_binders b in
CLocalPattern (loc, (p,None)) :: bl, c
@@ -418,7 +417,7 @@ let tag_var = tag Tag.variable
| CLambdaN ([],c) ->
extract_lam_binders c
| CLambdaN ([[_,Name id],bk,t],
- { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} )
+ { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} )
when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
let bl,c = extract_lam_binders b in
CLocalPattern (ce.loc,(p,None)) :: bl, c
@@ -650,7 +649,7 @@ let tag_var = tag Tag.variable
hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
latom
)
- | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
+ | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 08:31:19 +0000