aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES1
-rw-r--r--doc/refman/RefMan-syn.tex2
-rw-r--r--parsing/g_vernac.ml412
-rw-r--r--parsing/ppvernac.ml15
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/rawterm_to_relation.ml2
-rw-r--r--plugins/interface/name_to_ast.ml2
-rw-r--r--plugins/interface/xlate.ml7
-rw-r--r--plugins/subtac/subtac_command.ml2
-rw-r--r--plugins/subtac/subtac_command.mli4
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/command.mli12
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml4
-rw-r--r--toplevel/vernacexpr.ml8
16 files changed, 45 insertions, 40 deletions
diff --git a/CHANGES b/CHANGES
index 0eb237a97..be07cfe7b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,7 @@ Notations
- Abbreviations now use implicit arguments and arguments scopes for printing.
- Abbreviations to pure names now strictly behave like the name they refer to
(make redirections of qualified names easier).
+- The "where" clause now supports multiple notations per defined object.
Vernacular commands
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ed54ecb67..548c25985 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -463,7 +463,7 @@ Locate "'exists' _ , _".
\nelist{{\cofixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
\\
{\declnotation} & ::= &
- \zeroone{{\tt where} {\str} {\tt :=} {\term} \zeroone{:{\scope}}} .
+ \zeroone{{\tt where} \nelist{{\str} {\tt :=} {\term} \zeroone{:{\scope}}}{\tt and}}.
\\
\\
{\modifiers}
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c21185c51..a0ee06683 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -167,7 +167,7 @@ GEXTEND Gram
cfs = [ ":="; l = constructor_list_or_record_decl -> l
| -> RecordDecl (None, []) ] ->
let (recf,indf) = b in
- VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),None])
+ VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]])
] ]
;
typeclass_context:
@@ -236,10 +236,14 @@ GEXTEND Gram
[ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
| -> None ] ]
;
+ one_decl_notation:
+ [ [ ntn = ne_string; ":="; c = constr;
+ scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
+ ;
decl_notation:
- [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr;
- scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ]
- ;
+ [ [ "where"; l = LIST1 one_decl_notation SEP IDENT "and" -> l
+ | -> [] ] ]
+ ;
(* Inductives and records *)
inductive_definition:
[ [ id = identref; oc = opt_coercion; indpar = binders_let;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6449add92..9e7bd10e7 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -288,10 +288,9 @@ let pr_type_option pr_c = function
| CHole (loc, k) -> mt()
| _ as c -> brk(0,2) ++ str":" ++ pr_c c
-let pr_decl_notation prc =
- pr_opt (fun (ntn,c,scopt) -> fnl () ++
- str "where " ++ qs ntn ++ str " := " ++ prc c ++
- pr_opt (fun sc -> str ": " ++ str sc) scopt)
+let pr_decl_notation prc (ntn,c,scopt) =
+ fnl () ++ str "where " ++ qs ntn ++ str " := " ++ prc c ++
+ pr_opt (fun sc -> str ": " ++ str sc) scopt
let pr_vbinders l =
hv 0 (pr_binders l)
@@ -432,7 +431,7 @@ let pr_record_field (x, ntn) =
| None ->
hov 1 (pr_lname id ++ str" :=" ++ spc() ++
pr_lconstr b)) in
- prx ++ pr_decl_notation pr_constr ntn
+ prx ++ prlist (pr_decl_notation pr_constr) ntn
in
let pr_record_decl b c fs =
pr_opt pr_lident c ++ str"{" ++
@@ -617,7 +616,7 @@ let rec pr_vernac = function
pr_and_type_binders_arg indpar ++ spc() ++
Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
str" :=") ++ pr_constructor_list k lc ++
- pr_decl_notation pr_constr ntn
+ prlist (pr_decl_notation pr_constr) ntn
in
hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
++
@@ -655,7 +654,7 @@ let rec pr_vernac = function
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++
- pr_decl_notation pr_constr ntn
+ prlist (pr_decl_notation pr_constr) ntn
in
let start = if b then "Boxed Fixpoint" else "Fixpoint" in
hov 1 (str start ++ spc() ++
@@ -670,7 +669,7 @@ let rec pr_vernac = function
pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
spc() ++ pr_lconstr_expr c ++
str" :=" ++ brk(1,1) ++ pr_lconstr def ++
- pr_decl_notation pr_constr ntn
+ prlist (pr_decl_notation pr_constr) ntn
in
let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
hov 1 (str start ++ spc() ++
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 77389681b..bd3f7e8ec 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -527,7 +527,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
raise (UserError("",str "Cannot find argument " ++
Ppconstr.pr_id id))
in
- (name,annot,args,types,body),(None:Vernacexpr.decl_notation option)
+ (name,annot,args,types,body),([]:Vernacexpr.decl_notation list)
| (name,None,args,types,body),recdef ->
let names = (Topconstr.names_of_local_assums args) in
if is_one_rec recdef && List.length names > 1 then
@@ -537,7 +537,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
else
let loc, na = List.hd names in
(name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
- (None:Vernacexpr.decl_notation option)
+ ([]:Vernacexpr.decl_notation list)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
("Cannot use mutual definition with well-founded recursion or measure")
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 04e36d945..c69e04b93 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -904,7 +904,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
} in *)
let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
- let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in
+ let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 752e546c8..f69dd2fe6 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -1338,7 +1338,7 @@ let do_build_inductive
((dummy_loc,relnames.(i)),
rel_params,
Some rel_arities.(i),
- ext_rel_constructors),None
+ ext_rel_constructors),[]
in
let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
let rel_inds = Array.to_list ext_rel_constructors in
diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml
index 142116ade..b87d95a82 100644
--- a/plugins/interface/name_to_ast.ml
+++ b/plugins/interface/name_to_ast.ml
@@ -110,7 +110,7 @@ let convert_one_inductive sp tyi =
(((false,(dummy_loc,basename sp)),
convert_env(List.rev params),
Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw ,
- Constructors (convert_constructors envpar cstrnames cstrtypes)), None);;
+ Constructors (convert_constructors envpar cstrnames cstrtypes)), []);;
(* This function converts a Mutual inductive definition to a Coqast.t.
It is obtained directly from print_mutual in pretty.ml. However, all
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 435130ae6..7b35f4021 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1555,13 +1555,14 @@ let xlate_comment = function
(CT_coerce_NUM_to_FORMULA(CT_int_encapsulator (string_of_int n)));;
let translate_opt_notation_decl = function
- None -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none)
- | Some(s, f, sc) ->
+ [] -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none)
+ | [s, f, sc] ->
let tr_sc =
match sc with
None -> ctv_ID_OPT_NONE
| Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in
- CT_decl_notation(CT_string s, xlate_formula f, tr_sc);;
+ CT_decl_notation(CT_string s, xlate_formula f, tr_sc)
+ | _ -> xlate_error "TODO: multiple where clause";;
let xlate_level = function
Extend.NumLevel n -> CT_coerce_INT_to_INT_OR_NEXT(CT_int n)
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 007013d40..b61299a06 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -431,7 +431,7 @@ let interp_recursive fixkind l boxed =
(* Get interpretation metadatas *)
let impls = Constrintern.compute_full_internalization_env env Constrintern.Recursive [] fixnames fixtypes fiximps in
- let notations = List.fold_right Option.List.cons ntnl [] in
+ let notations = List.flatten ntnl in
(* Interp bodies with rollback because temp use of notations/implicit *)
let fixdefs =
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index c9064ec82..71c93266d 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -54,7 +54,7 @@ val build_wellfounded :
Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
val build_recursive :
- (fixpoint_expr * decl_notation option) list -> bool -> unit
+ (fixpoint_expr * decl_notation list) list -> bool -> unit
val build_corecursive :
- (cofixpoint_expr * decl_notation option) list -> bool -> unit
+ (cofixpoint_expr * decl_notation list) list -> bool -> unit
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 67660cab3..d59b16d82 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -331,7 +331,7 @@ let extract_mutual_inductive_declaration_components indl =
let params = extract_params indl in
let coes = extract_coercions indl in
let indl = extract_inductive indl in
- (params,indl), coes, List.fold_right Option.List.cons ntnl []
+ (params,indl), coes, List.flatten ntnl
let declare_mutual_inductive_with_eliminations isrecord mie impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
@@ -581,13 +581,13 @@ let extract_fixpoint_components l =
let wfl = List.map (fun (_,wf,_,_,_) -> fst wf) fixl in
let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
{fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
- fixl, List.fold_right Option.List.cons ntnl [], wfl
+ fixl, List.flatten ntnl, wfl
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
List.map (fun ((_,id),bl,typ,def) ->
{fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
- List.fold_right Option.List.cons ntnl []
+ List.flatten ntnl
let do_fixpoint l b =
let fixl,ntns,wfl = extract_fixpoint_components l in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 05ee67d79..e42580c2b 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -71,7 +71,7 @@ type structured_inductive_expr =
local_binder list * structured_one_inductive_expr list
val extract_mutual_inductive_declaration_components :
- (one_inductive_expr * decl_notation option) list ->
+ (one_inductive_expr * decl_notation list) list ->
structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
(* Typing mutual inductive definitions *)
@@ -94,7 +94,7 @@ val declare_mutual_inductive_with_eliminations :
(* Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
- (one_inductive_expr * decl_notation option) list -> bool -> unit
+ (one_inductive_expr * decl_notation list) list -> bool -> unit
(*************************************************************************)
(* Fixpoints and cofixpoints *)
@@ -110,12 +110,12 @@ type structured_fixpoint_expr = {
(co)fixpoints declarations *)
val extract_fixpoint_components :
- (fixpoint_expr * decl_notation option) list ->
+ (fixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list *
(* possible structural arg: *) lident option list
val extract_cofixpoint_components :
- (cofixpoint_expr * decl_notation option) list ->
+ (cofixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
(* Typing fixpoints and cofixpoint_expr *)
@@ -144,10 +144,10 @@ val declare_cofixpoint :
(* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
- (fixpoint_expr * decl_notation option) list -> bool -> unit
+ (fixpoint_expr * decl_notation list) list -> bool -> unit
val do_cofixpoint :
- (cofixpoint_expr * decl_notation option) list -> bool -> unit
+ (cofixpoint_expr * decl_notation list) list -> bool -> unit
(* Utils *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5ed989438..0353261b9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -49,7 +49,7 @@ let interp_fields_evars evars env nots l =
in
let d = (i,b',t') in
let impls' = set_internalization_env_params impls [] in
- Option.iter (Metasyntax.set_notation_for_interpretation impls') no;
+ List.iter (Metasyntax.set_notation_for_interpretation impls') no;
(push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], []) nots l
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e3aa41354..60e38d97f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -401,13 +401,13 @@ let vernac_inductive finite infer indl =
| _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
match indl with
- | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] ->
+ | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record (match b with Class true -> Class false | _ -> b)
finite infer id bl c oc fs
| [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
let f =
let (coe, ((loc, id), ce)) = l in
- ((coe, AssumExpr ((loc, Name id), ce)), None)
+ ((coe, AssumExpr ((loc, Name id), ce)), [])
in vernac_record (Class true) finite infer id bl c None [f]
| [ ( id , bl , c , Class true, _), _ ] ->
Util.error "Definitional classes must have a single method"
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c590202e5..8a70e7626 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -159,7 +159,7 @@ type decl_notation = string * constr_expr * scope_name option
type simple_binder = lident list * constr_expr
type class_binder = lident * constr_expr list
type 'a with_coercion = coercion_flag * 'a
-type 'a with_notation = 'a * decl_notation option
+type 'a with_notation = 'a * decl_notation list
type constructor_expr = (lident * constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
| Constructors of constructor_expr list
@@ -223,9 +223,9 @@ type vernac_expr =
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
| VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
- | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation option) list
- | VernacFixpoint of (fixpoint_expr * decl_notation option) list * bool
- | VernacCoFixpoint of (cofixpoint_expr * decl_notation option) list * bool
+ | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
+ | VernacFixpoint of (fixpoint_expr * decl_notation list) list * bool
+ | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list * bool
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:42:39 +0000