diff options
23 files changed, 192 insertions, 67 deletions
diff --git a/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh new file mode 100644 index 0000000000..8b0f86d951 --- /dev/null +++ b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11602" ] || [ "$CI_BRANCH" = "master+support-only-parsing-where-clause" ]; then + + equations_CI_REF=master+adapt-coq-pr11602-only-parsing-where-notation + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst new file mode 100644 index 0000000000..1d30d16664 --- /dev/null +++ b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst @@ -0,0 +1,6 @@ +- **Added:** + Notations declared with the ``where`` clause in the declaration of + inductive types, coinductive types, record fields, fixpoints and + cofixpoints now support the ``only parsing`` modifier + (`#11602 <https://github.com/coq/coq/pull/11602>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst new file mode 100644 index 0000000000..3dd103b115 --- /dev/null +++ b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax :n:`pose proof (@ident:=@term)` as an + alternative to :n:`pose proof @term as @ident`, following the model of + :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof` + (`#11522 <https://github.com/coq/coq/pull/11522>`_, + by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst new file mode 100644 index 0000000000..d2af6a4ca7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + Deprecated the declaration of arbitrary terms as hints. Global + references are now mandatory. + (`#7791 <https://github.com/coq/coq/pull/7791>`_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6c1d83b3b8..b9e181dd94 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -24,7 +24,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. - field : `ident` [ `binders` ] : `type` [ where `notation` ] + field : `ident` [ `binders` ] : `type` [ `decl_notations` ] : `ident` [ `binders` ] [: `type` ] := `term` .. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition } @@ -35,8 +35,10 @@ expressions. In this sense, the :cmd:`Record` construction allows defining the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`. - Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the - order of the fields is important. Finally, :token:`binders` are parameters of the record. + Notice that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. The record can depend as a whole on parameters :token:`binders` + and each field can also depend on its own :token:`binders`. Finally, notations can be attached to + fields using the :n:`decl_notations` annotation. :cmd:`Record` and :cmd:`Structure` are synonyms. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a0ce20c79..2bfd810ea1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1452,6 +1452,19 @@ Controlling the proof flow While :tacn:`pose proof` expects that no existential variables are generated by the tactic, :tacn:`epose proof` removes this constraint. +.. tacv:: pose proof (@ident := @term) + + This is an alternative syntax for :n:`assert (@ident := @term)` and + :n:`pose proof @term as @ident`, following the model of :n:`pose + (@ident := @term)` but dropping the value of :token:`ident`. + +.. tacv:: epose proof (@ident := @term) + + This is an alternative syntax for :n:`eassert (@ident := @term)` + and :n:`epose proof @term as @ident`, following the model of + :n:`epose (@ident := @term)` but dropping the value of + :token:`ident`. + .. tacv:: enough (@ident : @type) :name: enough @@ -3761,18 +3774,18 @@ automatically created. Local is useless since hints do not survive anyway to the closure of sections. - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve - This command adds :n:`simple apply @term` to the hint list with the head - symbol of the type of :n:`@term`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@term` does not start with a product the tactic added in the hint list - is :n:`exact @term`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @term` is also stored in - the hints list. If the inferred type of :n:`@term` contains a dependent + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent quantification on a variable which occurs only in the premisses of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list @@ -3780,32 +3793,32 @@ automatically created. typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable + The head symbol of the type of :n:`@qualid` is a bound variable such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} : @ident + .. cmdv:: Hint Resolve {+ @qualid} : @ident - Adds each :n:`Hint Resolve @term`. + Adds each :n:`Hint Resolve @qualid`. - .. cmdv:: Hint Resolve -> @term : @ident + .. cmdv:: Hint Resolve -> @qualid : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentioned + the hint will be used as :n:`apply <- @qualid`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Hint Resolve <- @term + .. cmdv:: Hint Resolve <- @qualid Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term : @ident + .. cmdv:: Hint Immediate @qualid : @ident :name: Hint Immediate - This command adds :n:`simple apply @term; trivial` to the hint list associated + This command adds :n:`simple apply @qualid; trivial` to the hint list associated with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are not solved immediately by the :tacn:`trivial` tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited @@ -3813,12 +3826,12 @@ automatically created. never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` itself. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint :undocumented: - .. cmdv:: Hint Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @qualid} : @ident - Adds each :n:`Hint Immediate @term`. + Adds each :n:`Hint Immediate @qualid`. .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9b4d7cf5fa..fd95a5cef4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -909,10 +909,10 @@ notations are given below. The optional :production:`scope` is described in notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. : [Local] Reserved Notation `string` [(`modifiers`)] . - : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. + : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. : [Local] Declare Custom Entry `ident`. modifiers : `modifier`, … , `modifier` modifier : at level `num` @@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in .. prodn:: decl_notations ::= where @decl_notation {* and @decl_notation } - decl_notation ::= @string := @term1_extended {? : @ident } + decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident } .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. diff --git a/engine/namegen.ml b/engine/namegen.ml index bcc8c34a4d..d2c37fb716 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -259,15 +259,17 @@ let visible_ids sigma (nenv, c) = let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (GlobRef.Set_env.mem g gseen) then - begin - try let gseen = GlobRef.Set_env.add g gseen in - let short = Nametab.shortest_qualid_of_global Id.Set.empty g in - let dir, id = repr_qualid short in - let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in + let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with + | short -> + let dir, id = repr_qualid short in + if DirPath.is_empty dir then Id.Set.add id ids else ids + | exception Not_found -> + (* This may happen if given pathological terms or when manipulating + open modules *) + ids + in accu := (gseen, vseen, ids) - with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> () - end | Rel p -> let (gseen, vseen, ids) = !accu in if p > n && not (Int.Set.mem p vseen) then diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 3e4c7ba782..8e1e5559af 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -589,6 +589,16 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } + + (* Alternative syntax for "pose proof c as id by tac" *) + | IDENT "pose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "epose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) } | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e49f5abb8c..e3f2f18b44 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -528,9 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> + let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info ~poly:false - (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) + h) hints) else [] in diff --git a/tactics/hints.ml b/tactics/hints.ml index 86aa046586..731792e34e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1325,6 +1325,13 @@ let project_hint ~poly pri l2r r = let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" + ) + let interp_hints ~poly = fun h -> let env = Global.env () in @@ -1349,7 +1356,9 @@ let interp_hints ~poly = | HintsReference c -> let gr = global_with_alias c in (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> (PathAny, poly, f poly c) + | HintsConstr c -> + let () = warn_deprecated_hint_constr () in + (PathAny, poly, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = diff --git a/tactics/hints.mli b/tactics/hints.mli index 9c9f0b7708..7bb17489bf 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -181,7 +181,7 @@ type hnf = bool type hint_term = | IsGlobRef of GlobRef.t - | IsConstr of constr * Univ.ContextSet.t + | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"] type hints_entry = | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8ff571ae55..ff2556c5dc 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x Arguments foo _%type_scope Arguments Foo _%type_scope +myprod unit bool + : Set diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 9eec9a7dad..db1276cb6c 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set := (* Check printing of let-ins *) #[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. + +(* Check where clause *) +Reserved Notation "x ** y" (at level 40, left associativity). +Inductive myprod A B := + mypair : A -> B -> A ** B + where "A ** B" := (myprod A B) (only parsing). + +Check unit ** bool. diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out new file mode 100644 index 0000000000..6015fe32f9 --- /dev/null +++ b/test-suite/output/bug_8206.out @@ -0,0 +1,5 @@ +File "stdin", line 11, characters 0-23: +Error: Signature components for label homework do not match: expected type +"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type +"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0". + diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v new file mode 100644 index 0000000000..8d4e73dfac --- /dev/null +++ b/test-suite/output/bug_8206.v @@ -0,0 +1,11 @@ +Module Type Sig. + Parameter add: nat -> nat -> nat. + Axiom homework: forall (a b: nat), add a b = add b a. +End Sig. + +Module Impl. + Definition add(a b: nat) := plus a b. + Axiom homework: forall (a b: nat), add 0 b = add b 0. +End Impl. + +Module M : Sig := Impl. diff --git a/test-suite/success/pose.v b/test-suite/success/pose.v new file mode 100644 index 0000000000..17007915fe --- /dev/null +++ b/test-suite/success/pose.v @@ -0,0 +1,9 @@ +(* Test syntax *) + +Goal 0=0. +pose proof (a := I). +Fail clearbody a. +epose proof (b := fun _ => eq_refl). +Fail clearbody b. +exact (b a). +Qed. diff --git a/vernac/classes.ml b/vernac/classes.ml index b92c9e9b71..16b9e07fb2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -60,7 +60,9 @@ let add_instance check inst = let local = is_local_for_hint inst in add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path + List.iter (fun (path, pri, c) -> + let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in + add_instance_hint h path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 37b584f8d9..c1414c552a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -44,11 +44,12 @@ let quoted_attributes = Entry.create "vernac:quoted_attributes" let class_rawexpr = Entry.create "vernac:class_rawexpr" let thm_token = Entry.create "vernac:thm_token" let def_body = Entry.create "vernac:def_body" -let decl_notation = Entry.create "vernac:decl_notation" +let decl_notations = Entry.create "vernac:decl_notations" let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" let section_subset_expr = Entry.create "vernac:section_subset_expr" let scope_delimiter = Entry.create "vernac:scope_delimiter" +let only_parsing = Entry.create "vernac:only_parsing" let make_bullet s = let open Proof_bullet in @@ -176,7 +177,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GRAMMAR EXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl univ_decl; + record_field decl_notations rec_definition ident_decl univ_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -376,15 +377,17 @@ GRAMMAR EXTEND Gram [ [ IDENT "Eval"; r = red_expr; "in" -> { Some r } | -> { None } ] ] ; - one_decl_notation: - [ [ ntn = ne_lstring; ":="; c = constr; - scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,scopt) } ] ] + decl_notation: + [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing; + scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> + { { decl_ntn_string = ntn; decl_ntn_interp = c; + decl_ntn_only_parsing = b; decl_ntn_scope = scopt } } ] ] ; decl_sep: [ [ IDENT "and" -> { () } ] ] ; - decl_notation: - [ [ "where"; l = LIST1 one_decl_notation SEP decl_sep -> { l } + decl_notations: + [ [ "where"; l = LIST1 decl_notation SEP decl_sep -> { l } | -> { [] } ] ] ; (* Inductives and records *) @@ -396,7 +399,7 @@ GRAMMAR EXTEND Gram [ [ oc = opt_coercion; id = ident_decl; indpar = binders; extrapar = OPT [ "|"; p = binders -> { p } ]; c = OPT [ ":"; c = lconstr -> { c } ]; - lc=opt_constructors_or_fields; ntn = decl_notation -> + lc=opt_constructors_or_fields; ntn = decl_notations -> { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ] ; constructor_list_or_record_decl: @@ -423,14 +426,14 @@ GRAMMAR EXTEND Gram [ [ id_decl = ident_decl; bl = binders_fixannot; rtype = type_cstr; - body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations -> { let binders, rec_order = bl in {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; corec_definition: [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; - body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} } ]] ; @@ -466,7 +469,7 @@ GRAMMAR EXTEND Gram record_field: [ [ attr = LIST0 quoted_attributes ; bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; - rf_notation = decl_notation -> { + rf_notation = decl_notations -> { let rf_canonical = attr |> List.flatten |> parse canonical_field in let rf_subclass, rf_decl = bd in rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] @@ -1145,7 +1148,7 @@ GRAMMAR EXTEND Gram (* Grammar extensions *) GRAMMAR EXTEND Gram - GLOBAL: syntax; + GLOBAL: syntax only_parsing; syntax: [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index fedebc9700..33fd14a731 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1654,13 +1654,23 @@ let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in (* Notations with only interpretation *) -let add_notation_interpretation env ({CAst.loc;v=df},c,sc) = - let df' = add_notation_interpretation_core ~local:false df env c sc false false None in +let add_notation_interpretation env decl_ntn = + let + { decl_ntn_string = { CAst.loc ; v = df }; + decl_ntn_interp = c; + decl_ntn_only_parsing = onlyparse; + decl_ntn_scope = sc } = decl_ntn in + let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in Dumpglob.dump_notation (loc,df') sc true -let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) = +let set_notation_for_interpretation env impls decl_ntn = + let + { decl_ntn_string = { CAst.v = df }; + decl_ntn_interp = c; + decl_ntn_only_parsing = onlyparse; + decl_ntn_scope = sc } = decl_ntn in (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index e3e733a4b7..d76820b033 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -37,12 +37,12 @@ val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : - env -> (lstring * constr_expr * scope_name option) -> unit + env -> decl_notation -> unit (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : env -> Constrintern.internalization_env -> - (lstring * constr_expr * scope_name option) -> unit +val set_notation_for_interpretation : + env -> Constrintern.internalization_env -> decl_notation -> unit (** Add only the parsing/printing rule of a notation *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 33d9e3d98a..84ae04e4cc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -297,11 +297,6 @@ open Pputils | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ({loc; v=ntn},c,scopt) = - fnl () ++ keyword "where " ++ qs ntn ++ str " := " - ++ Flags.without_option Flags.beautify prc c ++ - pr_opt (fun sc -> str ": " ++ str sc) scopt - let pr_binders_arg = let env = Global.env () in let sigma = Evd.from_env env in @@ -418,6 +413,21 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") + let pr_only_parsing_clause onlyparsing = + pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []) + + let pr_decl_notation prc decl_ntn = + let open Vernacexpr in + let + { decl_ntn_string = {CAst.loc;v=ntn}; + decl_ntn_interp = c; + decl_ntn_only_parsing = onlyparsing; + decl_ntn_scope = scopt } = decl_ntn in + fnl () ++ keyword "where " ++ qs ntn ++ str " := " + ++ Flags.without_option Flags.beautify prc c + ++ pr_only_parsing_clause onlyparsing + ++ pr_opt (fun sc -> str ": " ++ str sc) scopt + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in @@ -1057,7 +1067,7 @@ let string_of_definition_object_kind = let open Decls in function hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) + pr_only_parsing_clause onlyparsing) ) | VernacArguments (q, args, more_implicits, mods) -> return ( diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 22aaab2a68..7169ea834a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -128,7 +128,12 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type decl_notation = lstring * constr_expr * scope_name option +type decl_notation = + { decl_ntn_string : lstring + ; decl_ntn_interp : constr_expr + ; decl_ntn_only_parsing : bool + ; decl_ntn_scope : scope_name option + } type 'a fix_expr_gen = { fname : lident |