diff options
31 files changed, 452 insertions, 271 deletions
diff --git a/dev/bench/render_results b/dev/bench/render_results index 72affd70b2..bd4308837b 100755 --- a/dev/bench/render_results +++ b/dev/bench/render_results @@ -76,25 +76,13 @@ let run_and_read cmd = ;; let ( %> ) f g x = g (f x) -;; let run = run_and_read %> snd -;; module Float = struct let nan = Pervasives.nan end -module Tuple4 = struct - - let first (x,_,_,_) = x - let second (_,y,_,_) = y - let third (_,_,z,_) = z - let fourth (_,_,_,z) = z - -end -;; - module List = struct include List @@ -149,6 +137,151 @@ module String = struct end ;; +module Table : +sig + type header = string + type row = string list list + val print : header list -> row list -> string +end = +struct + type header = string + + type row = string list list + + let val_padding = 2 + (* Padding between data in the same row *) + let row_padding = 1 + (* Padding between rows *) + + let homogeneous b = if b then () else failwith "Heterogeneous data" + + let vert_split (ls : 'a list list) = + let split l = match l with + | [] -> failwith "vert_split" + | x :: l -> (x, l) + in + let ls = List.map split ls in + List.split ls + + let rec last = function + | [] -> assert false + | [x] -> [], x + | x :: l -> + let (l, y) = last l in + (x :: l, y) + + let justify n s = + let len = String.length s in + let () = assert (len <= n) in + let lft = (n - len) / 2 in + let rgt = n - lft - len in + String.make lft ' ' ^ s ^ String.make rgt ' ' + + let justify_row layout data = + let map n s = + let len = String.length s in + let () = assert (len <= n) in + (* Right align *) + let pad = n - len in + String.make pad ' ' ^ s + in + let data = List.map2 map layout data in + String.concat (String.make val_padding ' ') data + + let angle hkind vkind = match hkind, vkind with + | `Lft, `Top -> "┌" + | `Rgt, `Top -> "┐" + | `Mid, `Top -> "┬" + | `Lft, `Mid -> "├" + | `Rgt, `Mid -> "┤" + | `Mid, `Mid -> "┼" + | `Lft, `Bot -> "└" + | `Rgt, `Bot -> "┘" + | `Mid, `Bot -> "┴" + + let print_separator vkind col_size = + let rec dashes n = if n = 0 then "" else "─" ^ dashes (n - 1) in + let len = List.length col_size in + let pad = dashes row_padding in + let () = assert (0 < len) in + let map n = dashes n in + angle `Lft vkind ^ pad ^ + String.concat (pad ^ angle `Mid vkind ^ pad) (List.map map col_size) ^ + pad ^ angle `Rgt vkind + + let print_blank col_size = + let len = List.length col_size in + let () = assert (0 < len) in + let pad = String.make row_padding ' ' in + let map n = String.make n ' ' in + "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) (List.map map col_size) ^ pad ^ "│" + + let print_row row = + let len = List.length row in + let () = assert (0 < len) in + let pad = String.make row_padding ' ' in + "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) row ^ pad ^ "│" + + (* Invariant : all rows must have the same shape *) + + let print (headers : header list) (rows : row list) = + (* Sanitize input *) + let ncolums = List.length headers in + let shape = ref None in + let check row = + let () = homogeneous (List.length row = ncolums) in + let rshape : int list = List.map (fun data -> List.length data) row in + match !shape with + | None -> shape := Some rshape + | Some s -> homogeneous (rshape = s) + in + let () = List.iter check rows in + (* Compute layout *) + let rec layout n (rows : row list) = + if n = 0 then [] + else + let (col, rows) = vert_split rows in + let ans = layout (n - 1) rows in + let data = ref None in + let iter args = + let size = List.map String.length args in + match !data with + | None -> data := Some size + | Some s -> + data := Some (List.map2 (fun len1 len2 -> max len1 len2) s size) + in + let () = List.iter iter col in + let data = match !data with None -> [] | Some s -> s in + data :: ans + in + let layout = layout ncolums rows in + let map hd shape = + let data_size = match shape with + | [] -> 0 + | n :: shape -> List.fold_left (fun accu n -> accu + n + val_padding) n shape + in + max (String.length hd) data_size + in + let col_size = List.map2 map headers layout in + (* Justify the data *) + let headers = List.map2 justify col_size headers in + let rows = List.map (fun row -> List.map2 justify col_size (List.map2 justify_row layout row)) rows in + (* Print the table *) + let rows, last = last rows in + let sep = print_separator `Mid col_size in + let rows = List.concat @@ List.map (fun r -> [print_row r; sep]) rows in + let lines = + print_separator `Top col_size :: + print_row headers :: + print_blank col_size :: + rows @ + print_row last :: + print_separator `Bot col_size :: + [] + in + String.concat "\n" lines +end + (******************************************************************************) (* END Copied from batteries, to remove *) (******************************************************************************) @@ -203,10 +336,6 @@ let proportional_difference_of_integers new_value old_value = else float_of_int (new_value - old_value) /. float_of_int old_value *. 100.0 in -let count_number_of_digits_before_decimal_point = - log10 %> floor %> int_of_float %> succ %> max 1 -in - (* parse the *.time and *.perf files *) coq_opam_packages |> List.map @@ -259,138 +388,39 @@ coq_opam_packages (* Below we take the measurements and format them to stdout. *) +|> List.map begin fun (package_name, new_t, old_t, perc) -> + + let precision = 2 in + let prf f = Printf.sprintf "%.*f" precision f in + let pri n = Printf.sprintf "%d" n in + + [ + [ package_name ]; + [ prf new_t.user_time; prf old_t.user_time; prf perc.user_time ]; + [ pri new_t.num_cycles; pri old_t.num_cycles; prf perc.num_cycles ]; + [ pri new_t.num_instr; pri old_t.num_instr; prf perc.num_instr ]; + [ pri new_t.num_mem; pri old_t.num_mem; prf perc.num_mem ]; + [ pri new_t.num_faults; pri old_t.num_faults; prf perc.num_faults ]; + ] + + end + |> fun measurements -> - let precision = 2 in - - (* the labels that we will print *) - let package_name__label = "package_name" in - let new__label = "NEW" in - let old__label = "OLD" in - let proportional_difference__label = "PDIFF" in - - (* the lengths of labels that we will print *) - let new__label__length = String.length new__label in - let proportional_difference__label__length = String.length proportional_difference__label in - - (* widths of individual columns of the table *) - let package_name__width = - max (measurements |> List.map (Tuple4.first %> String.length) |> List.max) - (String.length package_name__label) in - - let llf proj = - let lls = count_number_of_digits_before_decimal_point (List.max proj) + 1 + precision in - max lls new__label__length in - - let lli proj = - let lls = count_number_of_digits_before_decimal_point (float_of_int (List.(max proj))) + 1 + precision in - max lls new__label__length in - - let new_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.second measurements in - let old_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.third measurements in - - let llp proj = - let lls = - count_number_of_digits_before_decimal_point List.(max List.(map abs_float proj)) + 2 + precision in - max lls proportional_difference__label__length in - - let perc_timing_width = reduce_pkg_timings llp llp @@ List.map Tuple4.fourth measurements in - - (* print the table *) - let rec make_dashes = function - | 0 -> "" - | count -> "─" ^ make_dashes (pred count) - in - - let vertical_separator left_glyph middle_glyph right_glyph = - sprintf "%s─%s─%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s\n" - left_glyph - (make_dashes package_name__width) - middle_glyph - (make_dashes new_timing_width.user_time) - (make_dashes old_timing_width.user_time) - (make_dashes perc_timing_width.user_time) - middle_glyph - (make_dashes new_timing_width.num_cycles) - (make_dashes old_timing_width.num_cycles) - (make_dashes perc_timing_width.num_cycles) - middle_glyph - (make_dashes new_timing_width.num_instr) - (make_dashes old_timing_width.num_instr) - (make_dashes perc_timing_width.num_instr) - middle_glyph - (make_dashes new_timing_width.num_mem) - (make_dashes old_timing_width.num_mem) - (make_dashes perc_timing_width.num_mem) - middle_glyph - (make_dashes new_timing_width.num_faults) - (make_dashes old_timing_width.num_faults) - (make_dashes perc_timing_width.num_faults) - right_glyph - in - - let center_string string width = - let string_length = String.length string in - let width = max width string_length in - let left_hfill = (width - string_length) / 2 in - let right_hfill = width - left_hfill - string_length in - String.make left_hfill ' ' ^ string ^ String.make right_hfill ' ' - in - printf "\n"; - print_string (vertical_separator "┌" "┬" "┐"); - "│" ^ String.make (1 + package_name__width + 1) ' ' ^ "│" - ^ center_string "user time [s]" (1 + new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ^ "│" - ^ center_string "CPU cycles" (1 + new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) ^ "│" - ^ center_string "CPU instructions" (1 + new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ^ "│" - ^ center_string "max resident mem [KB]" (1 + new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ^ "│" - ^ center_string "mem faults" (1 + new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) - ^ "│\n" |> print_string; - printf "│%*s │ %*s│ %*s│ %*s│ %*s│ %*s│\n" - (1 + package_name__width) "" - (new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) "" - (new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) "" - (new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) "" - (new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) "" - (new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) ""; - printf "│ %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │\n" - package_name__width package_name__label - new_timing_width.user_time new__label - old_timing_width.user_time old__label - perc_timing_width.user_time proportional_difference__label - new_timing_width.num_cycles new__label - old_timing_width.num_cycles old__label - perc_timing_width.num_cycles proportional_difference__label - new_timing_width.num_instr new__label - old_timing_width.num_instr old__label - perc_timing_width.num_instr proportional_difference__label - new_timing_width.num_mem new__label - old_timing_width.num_mem old__label - perc_timing_width.num_mem proportional_difference__label - new_timing_width.num_faults new__label - old_timing_width.num_faults old__label - perc_timing_width.num_faults proportional_difference__label; - measurements |> List.iter - (fun (package_name, new_t, old_t, perc) -> - print_string (vertical_separator "├" "┼" "┤"); - printf "│ %*s │ %*.*f %*.*f %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │\n" - package_name__width package_name - new_timing_width.user_time precision new_t.user_time - old_timing_width.user_time precision old_t.user_time - perc_timing_width.user_time precision perc.user_time - new_timing_width.num_cycles new_t.num_cycles - old_timing_width.num_cycles old_t.num_cycles - perc_timing_width.num_cycles precision perc.num_cycles - new_timing_width.num_instr new_t.num_instr - old_timing_width.num_instr old_t.num_instr - perc_timing_width.num_instr precision perc.num_instr - new_timing_width.num_mem new_t.num_mem - old_timing_width.num_mem old_t.num_mem - perc_timing_width.num_mem precision perc.num_mem - new_timing_width.num_faults new_t.num_faults - old_timing_width.num_faults old_t.num_faults - perc_timing_width.num_faults precision perc.num_faults); - -print_string (vertical_separator "└" "┴" "┘"); + let headers = [ + ""; + "user time [s]"; + "CPU cycles"; + "CPU instructions"; + "max resident mem [KB]"; + "mem faults"; + ] in + + let descr = ["NEW"; "OLD"; "PDIFF"] in + let top = [ [ "package_name" ]; descr; descr; descr; descr; descr ] in + + printf "%s%!" (Table.print headers (top :: measurements)) +; (* ejgallego: disable this as it is very verbose and brings up little info in the log. *) if false then begin diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst new file mode 100644 index 0000000000..8d681361e8 --- /dev/null +++ b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst @@ -0,0 +1,13 @@ +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 <https://github.com/coq/coq/pull/11841>`_, + fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, + by Hugo Herbelin). diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index f7ce7f1c6c..aa754ab63d 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -490,10 +490,10 @@ We need some infrastructure for that. Definition id {T} {t : T} (x : phantom t) := x. Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5cbd2e400e..df73de846f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -603,7 +603,7 @@ Here is the basic example of a notation using a binder: .. coqtop:: in Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) - (at level 200, x ident, A at level 200, right associativity). + (at level 200, x name, A at level 200, right associativity). The binding variables in the right-hand side that occur as a parameter of the notation (here :g:`x`) dynamically bind all the occurrences @@ -616,8 +616,9 @@ application of the notation: Check sigma z : nat, z = 0. -Note the :n:`@syntax_modifier x ident` in the declaration of the -notation. It tells to parse :g:`x` as a single identifier. +Note the :n:`@syntax_modifier x name` in the declaration of the +notation. It tells to parse :g:`x` as a single identifier (or as the +unnamed variable :g:`_`). Binders bound in the notation and parsed as patterns ++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -655,7 +656,7 @@ variable. Here is an example showing the difference: Notation "'subset_bis' ' p , P" := (sig (fun p => P)) (at level 200, p strict pattern). Notation "'subset_bis' p , P " := (sig (fun p => P)) - (at level 200, p ident). + (at level 200, p name). .. coqtop:: all @@ -675,18 +676,19 @@ the following: .. coqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) - (at level 0, x at level 99 as ident). + (at level 0, x at level 99 as name). This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the constant :g:`sumbool` (see :ref:`specification`). -Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning +Then, in the rule, ``x name`` is replaced by ``x at level 99 as name`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for -:g:`sumbool`), but that this term has actually to be an identifier. +:g:`sumbool`), but that this term has actually to be a name, i.e. an +identifier or :g:`_`. The notation :g:`{ x | P }` is already defined in the standard -library with the ``as ident`` :n:`@syntax_modifier`. We cannot redefine it but +library with the ``as name`` :n:`@syntax_modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. @@ -702,12 +704,12 @@ Then, the following works: Check {(x,y) such that x+y=0}. To enforce that the pattern should not be used for printing when it -is just an identifier, one could have said +is just a name, one could have said ``p at level 99 as strict pattern``. -Note also that in the absence of a ``as ident``, ``as strict pattern`` or +Note also that in the absence of a ``as name``, ``as strict pattern`` or ``as pattern`` :n:`@syntax_modifier`\s, the default is to consider sub-expressions occurring -in binding position and parsed as terms to be ``as ident``. +in binding position and parsed as terms to be ``as name``. Binders bound in the notation and parsed as general binders +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -768,7 +770,7 @@ binding position. Here is an example: Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. Notation "▢_ n P" := (force n (fun n => P)) - (at level 0, n ident, P at level 9, format "▢_ n P"). + (at level 0, n name, P at level 9, format "▢_ n P"). .. coqtop:: all @@ -946,16 +948,31 @@ position of :g:`x`: (at level 10, f global, a1, an at level 9). In addition to ``global``, one can restrict the syntax of a -sub-expression by using the entry names ``ident`` or ``pattern`` +sub-expression by using the entry names ``ident``, ``name`` or ``pattern`` already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: + .. todo: these two Set Warnings and the note should be removed when + ident is reactivated with its literal meaning. + +.. coqtop:: none + + Set Warnings "-deprecated-ident-entry". + .. coqtop:: in Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +.. coqtop:: none + + Set Warnings "+deprecated-ident-entry". + +.. note:: As of version 8.13, the entry ``ident`` is a deprecated + alias for ``name``. In the future, it is planned to strictly + parse an identifier (excluding :g:`_`). + .. _custom-entries: Custom entries @@ -1113,6 +1130,31 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. +Another special situation is when parsing global references or +identifiers. To indicate that a custom entry should parse identifiers, +use the following form: + +.. coqtop:: none + + Reset Initial. + Declare Custom Entry expr. + +.. coqtop:: in + + Notation "x" := x (in custom expr at level 0, x ident). + +Similarly, to indicate that a custom entry should parse global references +(i.e. qualified or non qualified identifiers), use the following form: + +.. coqtop:: none + + Reset Initial. + Declare Custom Entry expr. + +.. coqtop:: in + + Notation "x" := x (in custom expr at level 0, x global). + .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar @@ -1142,6 +1184,7 @@ Here are the syntax elements used by the various notation commands. | only printing | format @string {? @string } explicit_subentry ::= ident + | name | global | bigint | strict pattern {? at level @natural } @@ -1151,6 +1194,7 @@ Here are the syntax elements used by the various notation commands. | custom @ident {? at @level } {? @binder_interp } | pattern {? at level @natural } binder_interp ::= as ident + | as name | as pattern | as strict pattern level ::= level @natural @@ -1188,6 +1232,27 @@ Here are the syntax elements used by the various notation commands. due to legacy notation in the Coq standard library. It can be turned on with the ``-w disj-pattern-notation`` flag. +.. note:: + + As of version 8.13, the entry ``ident`` is a deprecated alias for + ``name``. In the future, it is planned to strictly parse an + identifier (to the exclusion of :g:`_`). If the intent was to use + ``ident`` as an identifier (excluding :g:`_`), just silence the warning with + :n:`Set Warnings "-deprecated-ident-entry"` and it should automatically + get its intended meaning in version 8.15. + + Similarly, ``as ident`` is a deprecated alias for ``as name``, which + will only accept an identifier in the future. If the + intent was to use ``as ident`` as an identifier + (excluding :g:`_`), just silence the warning with + :n:`Set Warnings "-deprecated-as-ident-kind"`. + + However, this deprecation does not apply to custom entries, where it + already denotes an identifier, as expected. + + .. todo: the note above should be removed at the end of deprecation + phase of ident + .. .. _Scopes: Notation scopes diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index cdee623850..d01f66c6d7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1420,6 +1420,7 @@ syntax_modifiers: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "binder" @@ -1440,6 +1441,7 @@ at_level_opt: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c27169d432..f62dd8f731 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1579,6 +1579,7 @@ syntax_modifier: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "strict" "pattern" OPT ( "at" "level" natural ) @@ -1591,6 +1592,7 @@ explicit_subentry: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8bd77abc4a..0645636255 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -976,6 +976,9 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) +let cases_pattern_of_id {loc;v=id} = + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + let cases_pattern_of_name {loc;v=na} = let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) @@ -991,16 +994,20 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in + let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder NtnBinderParsedAsConstr AsName -> + let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> - let onlyident = (x = NtnParsedAsIdent) in + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> + let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in let binders,binders' = bind id (onlyident,scl) binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> diff --git a/interp/notation.ml b/interp/notation.ml index b5951a9c59..c35ba44aa5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -62,10 +62,11 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsName, NtnParsedAsName -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 | NtnParsedAsBinder, NtnParsedAsBinder -> true -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false +| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f51d3bfdfb..036970ce37 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -881,7 +881,7 @@ let is_onlybinding_meta id metas = let is_onlybinding_pattern_like_meta isvar id metas = try match Id.List.assoc id metas with | _,NtnTypeBinder (NtnBinderParsedAsConstr - (AsIdentOrPattern | AsStrictPattern)) -> true + (AsNameOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) | _,NtnTypeBinder NtnParsedAsBinder -> not isvar | _ -> false @@ -1533,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) = let v = glob_constr_of_cases_pattern (Global.env()) pat in (((vars,v),scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 29db23cc54..c541a19bfd 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes type constr_as_binder_kind = | AsIdent - | AsIdentOrPattern + | AsName + | AsNameOrPattern | AsStrictPattern type notation_binder_source = @@ -76,6 +77,8 @@ type notation_binder_source = | NtnParsedAsPattern of bool (* This accepts only ident *) | NtnParsedAsIdent + (* This accepts only name *) + | NtnParsedAsName (* This accepts ident, or pattern, or both *) | NtnBinderParsedAsConstr of constr_as_binder_kind (* This accepts ident, _, and quoted pattern *) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 17feeb9b5a..c9326615dc 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -263,7 +263,7 @@ let assoc_defined id env = match Environ.lookup_named id env with * before the term is computed. *) -(* Norm means the term is fully normalized and cannot create a redex +(* Ntrl means the term is fully normalized and cannot create a redex when substituted Cstr means the term is in head normal form and that it can create a redex when substituted (i.e. constructor, fix, lambda) @@ -271,10 +271,10 @@ let assoc_defined id env = match Environ.lookup_named id env with create a redex when substituted Red is used for terms that might be reduced *) -type red_state = Norm | Cstr | Whnf | Red +type red_state = Ntrl | Cstr | Whnf | Red let neutr = function - | Whnf|Norm -> Whnf + | Whnf|Ntrl -> Whnf | Red|Cstr -> Red type optrel = Unknown | KnownR | KnownI @@ -293,13 +293,13 @@ module Mark : sig val neutr : t -> t - val set_norm : t -> t + val set_ntrl : t -> t end = struct type t = int let[@inline] of_state = function - | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 + | Ntrl -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 let[@inline] of_relevance = function | Unknown -> 0 @@ -315,15 +315,15 @@ end = struct | _ -> assert false let[@inline] red_state x = match x land 0b1100 with - | 0b0000 -> Norm + | 0b0000 -> Ntrl | 0b0100 -> Cstr | 0b1000 -> Whnf | 0b1100 -> Red | _ -> assert false - let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *) + let[@inline] neutr x = x lor 0b1000 (* Whnf|Ntrl -> Whnf | Red|Cstr -> Red *) - let[@inline] set_norm x = x land 0b0011 + let[@inline] set_ntrl x = x land 0b0011 end let mark = Mark.mark @@ -358,10 +358,10 @@ and fterm = and finvert = Univ.Instance.t * fconstr array let fterm_of v = v.term -let set_norm v = v.mark <- Mark.set_norm v.mark -let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false +let set_ntrl v = v.mark <- Mark.set_ntrl v.mark +let is_val v = match Mark.red_state v.mark with Ntrl -> true | Cstr | Whnf | Red -> false -let mk_atom c = {mark=mark Norm Unknown;term=FAtom c} +let mk_atom c = {mark=mark Ntrl Unknown;term=FAtom c} let mk_red f = {mark=mark Red Unknown;term=f} (* Could issue a warning if no is still Red, pointing out that we loose @@ -448,7 +448,7 @@ let rec lft_fconstr n ft = let r = Mark.relevance ft.mark in match ft.term with | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft - | FRel i -> {mark=mark Norm r;term=FRel(i+n)} + | FRel i -> {mark=mark Ntrl r;term=FRel(i+n)} | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))} | FFix(fx,e) -> {mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))} @@ -466,7 +466,7 @@ let lift_fconstr_vect k v = let clos_rel e i = match expand_rel i e with | Inl(n,mt) -> lift_fconstr n mt - | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k} + | Inr(k,None) -> {mark=mark Ntrl Unknown; term= FRel k} | Inr(k,Some p) -> lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)} @@ -488,7 +488,7 @@ let compact_stack head stk = (* Put an update mark in the stack, only if needed *) let zupdate info m s = let share = info.i_cache.i_share in - if share && begin match Mark.red_state m.mark with Red -> true | Norm | Whnf | Cstr -> false end + if share && begin match Mark.red_state m.mark with Red -> true | Ntrl | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -514,8 +514,8 @@ let mk_clos e t = | Rel i -> clos_rel e i | Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) } | Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) } - | Meta _ | Sort _ -> {mark = mark Norm KnownR; term = FAtom t } - | Ind kn -> {mark = mark Norm KnownR; term = FInd kn } + | Meta _ | Sort _ -> {mark = mark Ntrl KnownR; term = FAtom t } + | Ind kn -> {mark = mark Ntrl KnownR; term = FInd kn } | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } | Int i -> {mark = mark Cstr Unknown; term = FInt i} | Float f -> {mark = mark Cstr Unknown; term = FFloat f} @@ -734,11 +734,11 @@ let strip_update_shift_app_red head stk = strip_rec [] head 0 stk let strip_update_shift_app head stack = - assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); + assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true); strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); + assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -787,7 +787,7 @@ let rec eta_expand_stack = function | Zshift _ | Zupdate _ | Zprimitive _ as e) :: s -> e :: eta_expand_stack s | [] -> - [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]] + [Zshift 1; Zapp [|{mark=mark Ntrl Unknown; term= FRel 1}|]] (* Get the arguments of a native operator *) let rec skip_native_args rargs nargs = @@ -968,7 +968,7 @@ module FNativeEntries = | FArray (_u,t,_ty) -> t | _ -> raise Not_found - let dummy = {mark = mark Norm KnownR; term = FRel 0} + let dummy = {mark = mark Ntrl KnownR; term = FRel 0} let current_retro = ref Retroknowledge.empty let defined_int = ref false @@ -978,7 +978,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_int63 with | Some c -> defined_int := true; - fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + fint := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } | None -> defined_int := false let defined_float = ref false @@ -988,7 +988,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_float64 with | Some c -> defined_float := true; - ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + ffloat := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } | None -> defined_float := false let defined_bool = ref false @@ -1039,7 +1039,7 @@ module FNativeEntries = fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) }; fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }; let (icmp, _) = cEq in - fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) } + fcmp := { mark = mark Ntrl KnownR; term = FInd (Univ.in_punivs icmp) } | None -> defined_cmp := false let defined_f_cmp = ref false @@ -1327,19 +1327,19 @@ let rec knr info tab m stk = let rargs, a, nargs, stk = get_native_args1 op c stk in kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) else - (* Similarly to fix, partially applied primitives are not Norm! *) + (* Similarly to fix, partially applied primitives are not Ntrl! *) (m, stk) - | Undef _ | OpaqueDef _ -> (set_norm m; (m,stk))) + | Undef _ | OpaqueDef _ -> (set_ntrl m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info tab (VarKey id) with | Def v -> kni info tab v stk | Primitive _ -> assert false - | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) + | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk))) | FFlex(RelKey k) when red_set info.i_flags fDELTA -> (match ref_value_cache info tab (RelKey k) with | Def v -> kni info tab v stk | Primitive _ -> assert false - | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) + | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk))) | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in @@ -1523,9 +1523,9 @@ let norm_val info tab v = with_stats (lazy (kl info tab v)) let whd_stack infos tab m stk = match Mark.red_state m.mark with -| Whnf | Norm -> +| Whnf | Ntrl -> (** No need to perform [kni] nor to unlock updates because - every head subterm of [m] is [Whnf] or [Norm] *) + every head subterm of [m] is [Whnf] or [Ntrl] *) knh infos m stk | Red | Cstr -> let k = kni infos tab m stk in diff --git a/parsing/extend.ml b/parsing/extend.ml index 94c3768116..7d2ed9aed0 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -32,6 +32,7 @@ let production_level_eq lev1 lev2 = type 'a constr_entry_key_gen = | ETIdent + | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *) | ETGlobal | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) @@ -55,6 +56,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list type binder_target = ForBinder | ForTerm type constr_prod_entry_key = + | ETProdIdent (* Parsed as an ident *) | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) diff --git a/parsing/extend.mli b/parsing/extend.mli index b698415fd6..3cea45c3f5 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -27,6 +27,7 @@ val production_level_eq : production_level -> production_level -> bool type 'a constr_entry_key_gen = | ETIdent + | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *) | ETGlobal | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) @@ -50,6 +51,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list type binder_target = ForBinder | ForTerm type constr_prod_entry_key = + | ETProdIdent (* Parsed as an ident *) | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 21ec80abbc..da4a50b674 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -399,7 +399,11 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2 | MLfloat f1, MLfloat f2 -> Float64.equal f1 f2 -| _, _ -> false +| MLparray (t1,def1), MLparray (t2, def2) -> Array.equal eq_ml_ast t1 t2 && eq_ml_ast def1 def2 +| (MLrel _|MLapp _|MLlam _|MLletin _|MLglob _|MLcons _ + |MLtuple _|MLcase _|MLfix _|MLexn _|MLdummy _|MLaxiom + | MLmagic _| MLuint _| MLfloat _|MLparray _), _ + -> false and eq_ml_pattern p1 p2 = match p1, p2 with | Pcons (gr1, p1), Pcons (gr2, p2) -> diff --git a/test-suite/bugs/closed/bug_13453.v b/test-suite/bugs/closed/bug_13453.v new file mode 100644 index 0000000000..4d0e435df7 --- /dev/null +++ b/test-suite/bugs/closed/bug_13453.v @@ -0,0 +1,6 @@ +Require Extraction. + +Primitive array := #array_type. + +Definition a : array nat := [| 0%nat | 0%nat |]. +Extraction a. diff --git a/test-suite/bugs/closed/bug_7967.v b/test-suite/bugs/closed/bug_7967.v index 2c8855fd54..987a820831 100644 --- a/test-suite/bugs/closed/bug_7967.v +++ b/test-suite/bugs/closed/bug_7967.v @@ -1,2 +1,6 @@ Set Universe Polymorphism. Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A. + +(* A similar bug *) +Context (C := ltac:(let y := constr:(Type) in exact nat)). +Check C@{}. diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v index bb43edbe74..93ed94df39 100644 --- a/test-suite/bugs/closed/bug_9517.v +++ b/test-suite/bugs/closed/bug_9517.v @@ -2,6 +2,7 @@ Declare Custom Entry expr. Declare Custom Entry stmt. Notation "x" := x (in custom stmt, x ident). Notation "x" := x (in custom expr, x ident). +Notation "'_'" := _ (in custom expr). Notation "1" := 1 (in custom expr). diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index bcb2468792..05712eaac7 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -62,7 +62,7 @@ Check `(∀ n p : A, n=p). Notation "'let'' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (f ident, x closed binder, y closed binder, at level 200, + (f name, x closed binder, y closed binder, at level 200, right associativity). Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. @@ -93,7 +93,7 @@ End A. Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (f ident, x closed binder, y closed binder, at level 200, + (f name, x closed binder, y closed binder, at level 200, right associativity). Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. @@ -104,7 +104,7 @@ Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. (* Old request mentioned again on coq-club 20/1/2012 *) Notation "# x : T => t" := (fun x : T => t) - (at level 0, t at level 200, x ident). + (at level 0, t at level 200, x name). Check # x : nat => x. Check # _ : nat => 2. @@ -116,7 +116,7 @@ Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). Check (exist (Q x) y conj). (* Check bug #4854 *) -Notation "% i" := (fun i : nat => i) (at level 0, i ident). +Notation "% i" := (fun i : nat => i) (at level 0, i name). Check %i. Check %j. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 04a91c14d9..6c714fc624 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -305,7 +305,7 @@ Module E. Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) - (at level 200, x ident, A at level 200, p at level 200, right associativity, + (at level 200, x name, A at level 200, p at level 200, right associativity, format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ebc1426fc8..ce488fe18d 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -327,6 +327,7 @@ Module P. Module NotationMixedTermBinderAsIdent. + Set Warnings "-deprecated-ident-entry". (* We do want ident! *) Notation "▢_ n P" := (pseudo_force n (fun n => P)) (at level 0, n ident, P at level 9, format "▢_ n P"). Check exists p, ▢_p (p >= 1). diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 023705e169..5247c7b56a 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -309,9 +309,9 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) : type_scope. Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) - (at level 200, x ident, p at level 200, right associativity) : type_scope. + (at level 200, x name, p at level 200, right associativity) : type_scope. Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q)) - (at level 200, x ident, A at level 200, p at level 200, right associativity, + (at level 200, x name, A at level 200, p at level 200, right associativity, format "'[' 'exists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. @@ -489,18 +489,18 @@ Module EqNotations. := (match H as p in (_ = y) return P with | eq_refl => H' end) - (at level 10, H' at level 10, y ident, p ident, + (at level 10, H' at level 10, y name, p name, format "'[' 'rew' 'dependent' [ 'fun' y p => P ] '/ ' H in '/' H' ']'"). Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'" := (match H as p in (_ = y) return P with | eq_refl => H' end) - (at level 10, H' at level 10, y ident, p ident, only parsing). + (at level 10, H' at level 10, y name, p name, only parsing). Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'" := (match eq_sym H as p in (_ = y) return P with | eq_refl => H' end) - (at level 10, H' at level 10, y ident, p ident, + (at level 10, H' at level 10, y name, p name, format "'[' 'rew' 'dependent' <- [ 'fun' y p => P ] '/ ' H in '/' H' ']'"). Notation "'rew' 'dependent' [ P ] H 'in' H'" := (match H as p in (_ = y) return P y p with diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 84d40035bf..1a2c4ba171 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -96,19 +96,19 @@ Module Generic. (* begin hide *) (* Notations used in the proof. Hidden in coqdoc. *) -Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity). +Reserved Notation "'∀₁' x : A , B" (at level 200, x name, A at level 200,right associativity). Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200). -Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'λ₁' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₁' x" (at level 5, left associativity). -Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity). -Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'∀₂' A , F" (at level 200, A name, right associativity). +Reserved Notation "'λ₂' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity). -Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity). +Reserved Notation "'∀₀' x : A , B" (at level 200, x name, A at level 200,right associativity). Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200). -Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'λ₀' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₀' x" (at level 5, left associativity). -Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity). -Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'∀₀¹' A : U , F" (at level 200, A name, right associativity). +Reserved Notation "'λ₀¹' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity). (* end hide *) diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 9c8508bf39..b2bdd8099a 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -18,7 +18,7 @@ Set Implicit Arguments. Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) - (x ident, y ident, at level 10) : type_scope. + (x name, y name, at level 10) : type_scope. Declare Scope program_scope. Delimit Scope program_scope with prg. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index d1cefeb552..a563dcbf95 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -335,19 +335,19 @@ Reserved Notation "[ 'predType' 'of' T ]" (at level 0, Reserved Notation "[ 'pred' : T | E ]" (at level 0, format "'[hv' [ 'pred' : T | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x | E ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x | E ]" (at level 0, x name, format "'[hv' [ 'pred' x | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x name, format "'[hv' [ 'pred' x : T | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x name, format "'[hv' [ 'pred' x | '/ ' E1 & '/ ' E2 ] ']'"). -Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x name, format "'[hv' [ 'pred' x : T | '/ ' E1 & E2 ] ']'"). -Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x name, format "'[hv' [ 'pred' x 'in' A ] ']'"). -Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x name, format "'[hv' [ 'pred' x 'in' A | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x name, format "'[hv' [ 'pred' x 'in' A | '/ ' E1 & '/ ' E2 ] ']'"). Reserved Notation "[ 'qualify' x | P ]" (at level 0, x at level 99, @@ -363,17 +363,17 @@ Reserved Notation "[ 'qualify' 'an' x | P ]" (at level 0, x at level 99, Reserved Notation "[ 'qualify' 'an' x : T | P ]" (at level 0, x at level 99, format "'[hv' [ 'qualify' 'an' x : T | '/ ' P ] ']'"). -Reserved Notation "[ 'rel' x y | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A & B ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A ] ']'"). Reserved Notation "[ 'mem' A ]" (at level 0, format "[ 'mem' A ]"). diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index d0508bef2e..dc81b5cca7 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -110,7 +110,7 @@ Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200, Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200, c, R, vT, vF at level 200). Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200, - c, R, vT, vF at level 200, x ident). + c, R, vT, vF at level 200, x name). Reserved Notation "x : T" (at level 100, right associativity, format "'[hv' x '/ ' : T ']'"). diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v index e1442e1da2..ba66e04e4a 100644 --- a/theories/ssr/ssrfun.v +++ b/theories/ssr/ssrfun.v @@ -236,19 +236,19 @@ Reserved Notation "'fun' => E" (at level 200, format "'fun' => E"). Reserved Notation "[ 'fun' : T => E ]" (at level 0, format "'[hv' [ 'fun' : T => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x => E ]" (at level 0, - x ident, format "'[hv' [ 'fun' x => '/ ' E ] ']'"). + x name, format "'[hv' [ 'fun' x => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x : T => E ]" (at level 0, - x ident, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'"). + x name, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x y => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' x y => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' x y => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x y : T => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'"). Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'"). Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0, - x ident, y ident, format "[ 'fun' ( x : T ) ( y : U ) => E ]" ). + x name, y name, format "[ 'fun' ( x : T ) ( y : U ) => E ]" ). Reserved Notation "f =1 g" (at level 70, no associativity). Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90). @@ -259,33 +259,33 @@ Reserved Notation "f \; g" (at level 60, right associativity, format "f \; '/ ' g"). Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99, - x ident, format "{ 'morph' f : x / a >-> r }"). + x name, format "{ 'morph' f : x / a >-> r }"). Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99, - x ident, format "{ 'morph' f : x / a }"). + x name, format "{ 'morph' f : x / a }"). Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99, - x ident, y ident, format "{ 'morph' f : x y / a >-> r }"). + x name, y name, format "{ 'morph' f : x y / a >-> r }"). Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'morph' f : x y / a }"). + x name, y name, format "{ 'morph' f : x y / a }"). Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99, - x ident, format "{ 'homo' f : x / a >-> r }"). + x name, format "{ 'homo' f : x / a >-> r }"). Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99, - x ident, format "{ 'homo' f : x / a }"). + x name, format "{ 'homo' f : x / a }"). Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99, - x ident, y ident, format "{ 'homo' f : x y / a >-> r }"). + x name, y name, format "{ 'homo' f : x y / a >-> r }"). Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'homo' f : x y / a }"). + x name, y name, format "{ 'homo' f : x y / a }"). Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'homo' f : x y /~ a }"). + x name, y name, format "{ 'homo' f : x y /~ a }"). Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99, - x ident, format "{ 'mono' f : x / a >-> r }"). + x name, format "{ 'mono' f : x / a >-> r }"). Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99, - x ident, format "{ 'mono' f : x / a }"). + x name, format "{ 'mono' f : x / a }"). Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99, - x ident, y ident, format "{ 'mono' f : x y / a >-> r }"). + x name, y name, format "{ 'mono' f : x y / a >-> r }"). Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'mono' f : x y / a }"). + x name, y name, format "{ 'mono' f : x y / a }"). Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'mono' f : x y /~ a }"). + x name, y name, format "{ 'mono' f : x y /~ a }"). Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T"). Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'"). diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 9e850ff1c7..f8f2193e03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -257,9 +257,10 @@ let context ~poly l = let sigma = Evd.from_env env in let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) - let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in + let sigma, ctx = Evarutil.finalize ~abort_on_undefined_evars:false + sigma (fun nf -> List.map (RelDecl.map_constr_het nf) ctx) in (* reorder, evar-normalize and add implicit status *) let ctx = List.rev_map (fun d -> let {binder_name=name}, b, t = RelDecl.to_tuple d in @@ -267,8 +268,6 @@ let context ~poly l = | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") | Name id -> id in - let b = Option.map (EConstr.to_constr sigma) b in - let t = EConstr.to_constr sigma t in let impl = let open Glob_term in let search x = match x.CAst.v with | Some (Name id',max) when Id.equal name id' -> diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index ad6ac8d3f3..9fe3e2f7ab 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -246,6 +246,7 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = +| TTIdent : ('self, lident) entry | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry @@ -364,6 +365,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p)) | TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder)) | TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false) +| TTIdent -> MayRecNo (Pcoq.Symbol.nterm Prim.identref) | TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name) | TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder) | TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder) @@ -372,6 +374,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global) let interp_entry forpat e = match e with +| ETProdIdent -> TTAny TTIdent | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint @@ -382,6 +385,9 @@ let interp_entry forpat e = match e with | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) +let cases_pattern_expr_of_id { CAst.loc; v = id } = + CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) + let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None | Name id -> CPatAtom (Some (qualid_of_ident ?loc id)) @@ -398,6 +404,11 @@ let push_constr subst v = { subst with constrs = v :: subst.constrs } let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> match e with | TTConstr _ -> push_constr subst v +| TTIdent -> + begin match forpat with + | ForConstr -> { subst with binders = (cases_pattern_expr_of_id v, Glob_term.Explicit) :: subst.binders } + | ForPattern -> push_constr subst (cases_pattern_expr_of_id v) + end | TTName -> begin match forpat with | ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 116cfc6413..5c329f60a9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -531,6 +531,10 @@ let warn_deprecated_include_type = CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" (fun () -> strbrk "Include Type is deprecated; use Include instead") +let warn_deprecated_as_ident_kind = + CWarnings.create ~name:"deprecated-as-ident-kind" ~category:"deprecated" + (fun () -> strbrk "grammar kind \"as ident\" no longer accepts \"_\"; use \"as name\" instead to accept \"_\", too, or silence the warning if you actually intended to accept only identifiers.") + } (* Modules and Sections *) @@ -1242,7 +1246,13 @@ GRAMMAR EXTEND Gram ] ] ; explicit_subentry: - [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } + [ [ (* Warning to be turn into an error at the end of deprecation phase (for 8.14) *) + IDENT "ident" -> { ETName false } + (* To be activated at the end of transitory phase (for 8.15) + | IDENT "ident" -> { ETIdent } + *) + | IDENT "name" -> { ETName true } (* Boolean to remove at the end of transitory phase *) + | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } @@ -1261,8 +1271,9 @@ GRAMMAR EXTEND Gram | -> { DefaultLevel } ] ] ; binder_interp: - [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent } - | "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern } + [ [ "as"; IDENT "ident" -> { warn_deprecated_as_ident_kind (); Notation_term.AsIdent } + | "as"; IDENT "name" -> { Notation_term.AsName } + | "as"; IDENT "pattern" -> { Notation_term.AsNameOrPattern } | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ] ; END diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8759798331..06eb330958 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -340,11 +340,11 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec,side = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint -> + | ETConstr _ | ETGlobal | ETBigint | ETIdent -> UnpMetaVar (prec,side) - | ETPattern _ | ETIdent -> + | ETPattern _ | ETName _ -> UnpBinderMetaVar (prec,NotQuotedPattern) - | ETBinder _ -> + | ETBinder isopen -> UnpBinderMetaVar (prec,QuotedPattern) (* Heuristics for building default printing rules *) @@ -631,7 +631,8 @@ let include_possible_similar_trailing_pattern typ etyps sl l = try_aux 0 l let prod_entry_type = function - | ETIdent -> ETProdName + | ETIdent -> ETProdIdent + | ETName _ -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint | ETBinder o -> ETProdOneBinder o @@ -891,6 +892,11 @@ let default = { end +(* To be turned into a fatal warning in 8.14 *) +let warn_deprecated_ident_entry = + CWarnings.create ~name:"deprecated-ident-entry" ~category:"deprecated" + (fun () -> strbrk "grammar entry \"ident\" permitted \"_\" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use \"name\" instead.") + let interp_modifiers modl = let open NotationMods in let rec interp subtyps acc = function | [] -> subtyps, acc @@ -952,6 +958,13 @@ let interp_modifiers modl = let open NotationMods in let subtyps,mods = interp [] default modl in (* interpret item levels wrt to main entry *) let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in + (* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *) + let mods = + { mods with etyps = List.map (function + | (id,ETName false) -> + if mods.custom = InConstrEntry then (warn_deprecated_ident_entry (); (id,ETName true)) + else (id,ETIdent) + | x -> x) mods.etyps } in { mods with etyps = extra_etyps@mods.etyps } let check_infix_modifiers modifiers = @@ -1000,7 +1013,7 @@ let set_entry_type from n etyps (x,typ) = | ETConstr (s,bko,n), InternalProd -> ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x + | (ETIdent | ETName _ | ETBigint | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> ETConstr (from,None,(make_lev n from,typ)) in (x,typ) @@ -1023,7 +1036,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder | ETConstr _ | ETBigint | ETGlobal - | ETIdent | ETPattern _ -> NtnInternTypeAny + | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = List.map (fun (_, e) -> internalization_type_of_entry_type e) typs @@ -1043,6 +1056,7 @@ let make_interpretation_type isrec isonlybinding default_if_binding = function | ETConstr (_,None,_) -> NtnTypeConstr (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent + | ETName _ -> NtnTypeBinder NtnParsedAsName | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> @@ -1063,7 +1077,7 @@ let subentry_of_constr_prod_entry from_level = function | _ -> InConstrEntrySomeLevel let make_interpretation_vars - (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent) + (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsName) recvars level allvars typs = let eq_subscope (sc1, l1) (sc2, l2) = Option.equal String.equal sc1 sc2 && @@ -1159,7 +1173,7 @@ let find_precedence custom lev etyps symbols onlyprint = user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () - | (ETIdent | ETBigint | ETGlobal), _ -> + | (ETIdent | ETName _ | ETBigint | ETGlobal), _ -> begin match lev with | None -> ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0) @@ -1798,7 +1812,7 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing interp_notation_constr env nenv c in let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in - let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in + let interp = make_interpretation_vars ~default_if_binding:AsNameOrPattern [] 0 acvars (List.map in_pat vars) in let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in let also_in_cases_pattern = has_no_binders_type vars in let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 4cee4f7a47..01873918aa 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -187,13 +187,16 @@ let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel let pr_constr_as_binder_kind = let open Notation_term in function | AsIdent -> spc () ++ keyword "as ident" - | AsIdentOrPattern -> spc () ++ keyword "as pattern" + | AsName -> spc () ++ keyword "as name" + | AsNameOrPattern -> spc () ++ keyword "as pattern" | AsStrictPattern -> spc () ++ keyword "as strict pattern" let pr_strict b = if b then str "strict " else mt () let pr_set_entry_type pr = function | ETIdent -> str"ident" + | ETName false -> str"ident" (* temporary *) + | ETName true -> str"name" | ETGlobal -> str"global" | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko @@ -268,9 +271,9 @@ let pr_reference_or_constr pr_c = function | HintsConstr c -> pr_c c let pr_hint_mode = let open Hints in function - | ModeInput -> str"+" - | ModeNoHeadEvar -> str"!" - | ModeOutput -> str"-" + | ModeInput -> str"+" + | ModeNoHeadEvar -> str"!" + | ModeOutput -> str"-" let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } = pr_opt (fun x -> str"|" ++ int x) pri ++ |