diff options
49 files changed, 407 insertions, 364 deletions
diff --git a/Makefile.doc b/Makefile.doc index a8703b0acf..9da175f0e5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -246,16 +246,16 @@ $(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/too # user-contrib/*/*.mlg omitted for now (e.g. ltac2) PLUGIN_MLGS := $(wildcard plugins/*/*.mlg) OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg -DOC_MLGS := */*.mlg $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) -DOC_EDIT_MLGS := doc/tools/docgram/*.edit_mlg -DOC_RSTS := doc/sphinx/*/*.rst +DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) +DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) +DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS) $(SHOW)'DOC_GRAM' $(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS) #todo: add a dependency of sphinx on updated_rsts when we're ready -doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: $(DOC_GRAM) $(DOC_EDIT_MLGS) +doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: doc/tools/docgram/fullGrammar $(DOC_GRAM) $(DOC_EDIT_MLGS) $(SHOW)'DOC_GRAM_RSTS' $(HIDE)$(DOC_GRAM) -check-cmds $(DOC_MLGS) $(DOC_RSTS) diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index ad2f2f93e7..9620e7bc8c 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -7,69 +7,76 @@ set -e dev/tools/check-overlays.sh -if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh || - ! git diff-index --check --cached HEAD >/dev/null 2>&1 ; +# Can we check and fix formatting? +# NB: we will ignore errors from ocamlformat as it fails when +# encountering OCaml syntax errors +ocamlformat=$(command -v ocamlformat || echo true) +if [ "$ocamlformat" = true ] then - 1>&2 echo "Auto fixing whitespace issues..." + 1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting." +fi - # We fix whitespace in the index and in the working tree - # separately to preserve non-added changes. - index=$(mktemp "git-fix-ws-index.XXXXXX") - fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX") - tree=$(mktemp "git-fix-ws-tree.XXXXXX") - 1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." - 1>&2 echo "If an error destroys your changes you can recover using them." - 1>&2 echo "(The files are cleaned up on success.)" - 1>&2 echo #newline +1>&2 echo "Auto fixing whitespace and formatting issues..." - git diff-index -p --cached HEAD > "$index" - git diff-index -p HEAD > "$tree" +# We fix whitespace in the index and in the working tree +# separately to preserve non-added changes. +index=$(mktemp "git-fix-ws-index.XXXXXX") +fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX") +tree=$(mktemp "git-fix-ws-tree.XXXXXX") +1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." +1>&2 echo "If an error destroys your changes you can recover using them." +1>&2 echo "(The files are cleaned up on success.)" +1>&2 echo #newline - # reset work tree and index - # NB: untracked files which were not added are untouched - git apply --whitespace=nowarn --cached -R "$index" - git apply --whitespace=nowarn -R "$tree" +git diff-index -p --cached HEAD > "$index" +git diff-index -p HEAD > "$tree" - # Fix index - # For end of file newlines we must go through the worktree - 1>&2 echo "Fixing staged changes..." - git apply --cached --whitespace=fix "$index" - git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself - git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git add -u - 1>&2 echo #newline +# reset work tree and index +# NB: untracked files which were not added are untouched +git apply --whitespace=nowarn --cached -R "$index" +git apply --whitespace=nowarn -R "$tree" - # reset work tree - git diff-index -p --cached HEAD > "$fixed_index" - # If all changes were bad whitespace changes the patch is empty - # making git fail. Don't fail now: we fix the worktree first. - if [ -s "$fixed_index" ] - then - git apply --whitespace=nowarn -R "$fixed_index" - fi +# Fix index +# For end of file newlines we must go through the worktree +1>&2 echo "Fixing staged changes..." +git apply --cached --whitespace=fix "$index" +git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself +git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix +git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true +git add -u +1>&2 echo #newline - # Fix worktree - 1>&2 echo "Fixing unstaged changes..." - git apply --whitespace=fix "$tree" - git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - 1>&2 echo #newline +# reset work tree +git diff-index -p --cached HEAD > "$fixed_index" +# If all changes were bad whitespace changes the patch is empty +# making git fail. Don't fail now: we fix the worktree first. +if [ -s "$fixed_index" ] +then + git apply --whitespace=nowarn -R "$fixed_index" +fi - if ! [ -s "$fixed_index" ] - then - 1>&2 echo "No changes after fixing whitespace issues!" - exit 1 - fi +# Fix worktree +1>&2 echo "Fixing unstaged changes..." +git apply --whitespace=fix "$tree" +git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix +git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true +1>&2 echo #newline - # Check that we did fix whitespace - if ! git diff-index --check --cached HEAD; - then - 1>&2 echo "Auto-fixing whitespace failed: errors remain." - 1>&2 echo "This may fix itself if you try again." - 1>&2 echo "(Consider whether the number of errors decreases after each run.)" - exit 1 - fi - 1>&2 echo "Whitespace issues fixed!" +if ! [ -s "$fixed_index" ] +then + 1>&2 echo "No changes after fixing whitespace and formatting issues!" + exit 1 +fi - # clean up temporary files - rm "$index" "$tree" "$fixed_index" +# Check that we did fix whitespace +if ! git diff-index --check --cached HEAD; +then + 1>&2 echo "Auto-fixing whitespace failed: errors remain." + 1>&2 echo "This may fix itself if you try again." + 1>&2 echo "(Consider whether the number of errors decreases after each run.)" + exit 1 fi +1>&2 echo "Whitespace and formatting pass complete." + +# clean up temporary files +rm "$index" "$tree" "$fixed_index" diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst new file mode 100644 index 0000000000..224ffdbe9b --- /dev/null +++ b/doc/changelog/03-notations/11859-warn-inexact-float.rst @@ -0,0 +1,6 @@ +- **Added:** + In primitive floats, print a warning when parsing a decimal value + that is not exactly a binary64 floating-point number. + For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't. + (`#11859 <https://github.com/coq/coq/pull/11859>`_, + by Pierre Roux). diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst new file mode 100644 index 0000000000..d510416990 --- /dev/null +++ b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst @@ -0,0 +1,7 @@ +- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`) + may now call the :tacn:`lia` tactic instead of :tacn:`omega` + (when the `Omega` module is loaded); + more goals may be automatically solved, + fewer section variables will be captured spuriously + (`#11018 <https://github.com/coq/coq/pull/11018>`_, + by Vincent Laporte). diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst new file mode 100644 index 0000000000..e409c638bb --- /dev/null +++ b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst @@ -0,0 +1,3 @@ +- **Removed:** Removed SearchAbout command that was deprecated in 8.5. + Use :cmd:`Search` instead. + (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5ca0d8b81f..7401aff48c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -383,6 +383,10 @@ Changes in 8.11+beta1 <https://github.com/coq/coq/issues/3890>`_ and `#4638 <https://github.com/coq/coq/issues/4638>`_ by Maxime Dénès, review by Gaëtan Gilbert). +- **Changed:** + :cmd:`Fail` does not catch critical errors (including "stack overflow") + anymore (`#10173 <https://github.com/coq/coq/pull/10173>`_, + by Gaëtan Gilbert). - **Removed:** Undocumented :n:`Instance : !@type` syntax (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 39f2ccec29..acdd4408ed 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,6 +1062,11 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. +.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing] + + Not all decimal constants are floating-point values. This warning + is generated when parsing such a constant (for instance ``0.1``). + .. example:: .. coqtop:: all diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c33d62532e..b22c5286fe 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -321,18 +321,6 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - .. cmdv:: SearchAbout - :name: SearchAbout - - .. deprecated:: 8.5 - - Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current - :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with - command :cmd:`SearchAbout`. For compatibility, the deprecated name - :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For - compatibility, the list of objects to search when using :cmd:`SearchAbout` - may also be enclosed by optional ``[ ]`` delimiters. - .. cmd:: SearchHead @term @@ -929,16 +917,17 @@ Quitting and debugging .. cmd:: Fail @command - For debugging scripts, sometimes it is desirable to know - whether a command or a tactic fails. If the given :n:`@command` - fails, the ``Fail`` statement succeeds, without changing the proof - state, and in interactive mode, the system - prints a message confirming the failure. - If the given :n:`@command` succeeds, the statement is an error, and - it prints a message indicating that the failure did not occur. + For debugging scripts, sometimes it is desirable to know whether a + command or a tactic fails. If the given :n:`@command` fails, then + :n:`Fail @command` succeeds (excepts in the case of + critical errors, like a "stack overflow"), without changing the + proof state, and in interactive mode, the system prints a message + confirming the failure. .. exn:: The command has not failed! - :undocumented: + + If the given :n:`@command` succeeds, then :n:`Fail @command` + fails with this error message. .. _controlling-display: diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 7ae98f4cd2..4cde3809f0 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -110,6 +110,9 @@ Other command line arguments: * `-no-warn` suppresses printing of some warning messages +* `-no-update` puts updates to `fullGrammar` and `orderedGrammar` into new files named + `*.new`, leaving the originals unmodified. For use in Dune. + * `-short` limits processing to updating/verifying only the `fullGrammar` file * `-verbose` prints more messages about the grammar diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 88a5217652..60b845c4be 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1125,10 +1125,6 @@ query_command: [ | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" searchabout_query searchabout_queries "." | WITH "Search" searchabout_query searchabout_queries -| REPLACE "SearchAbout" searchabout_query searchabout_queries "." -| WITH "SearchAbout" searchabout_query searchabout_queries -| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." -| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules ] vernac_toplevel: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 0450aee2ec..eea1d5081d 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -32,6 +32,7 @@ type args = { fullGrammar : bool; check_tacs : bool; check_cmds : bool; + no_update: bool; show_warn : bool; verbose : bool; verify : bool; @@ -43,6 +44,7 @@ let default_args = { fullGrammar = false; check_tacs = false; check_cmds = false; + no_update = false; show_warn = true; verbose = false; verify = false; @@ -1574,7 +1576,7 @@ let reorder_grammar eg reordered_rules file = g_reorder eg !og.map !og.order -let finish_with_file old_file verify = +let finish_with_file old_file args = let files_eq f1 f2 = let chunksize = 8192 in (try @@ -1605,18 +1607,18 @@ let finish_with_file old_file verify = with Sys_error _ -> false) in - let temp_file = (old_file ^ "_temp") in + let temp_file = (old_file ^ ".new") in if !exit_code <> 0 then Sys.remove temp_file - else if verify then begin + else if args.verify then begin if not (files_eq old_file temp_file) then error "%s is not current\n" old_file; Sys.remove temp_file - end else + end else if not args.no_update then Sys.rename temp_file old_file let open_temp_bin file = - open_out_bin (sprintf "%s_temp" file) + open_out_bin (sprintf "%s.new" file) let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+" @@ -1829,7 +1831,7 @@ let process_rst g file args seen tac_prods cmd_prods = with End_of_file -> (); close_in old_rst; close_out new_rst; - finish_with_file file args.verify + finish_with_file file args let report_omitted_prods entries seen label split = let maybe_warn first last n = @@ -1877,7 +1879,7 @@ let process_grammar args = "DOC_GRAMMAR"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "fullGrammar") args.verify; + finish_with_file (dir "fullGrammar") args; if args.verbose then print_special_tokens g; @@ -1896,7 +1898,7 @@ let process_grammar args = "DOC_GRAMMAR"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "editedGrammar") args.verify; + finish_with_file (dir "editedGrammar") args; report_bad_nts g "editedGrammar" end; @@ -1911,11 +1913,13 @@ let process_grammar args = reorder_grammar g ordered_grammar "orderedGrammar"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "orderedGrammar") args.verify; + finish_with_file (dir "orderedGrammar") args; check_singletons g (* print_dominated g*) end; + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in + let args = { args with no_update = false } in (* always update rsts in place for now *) if !exit_code = 0 then begin let plist nt = let list = (List.map (fun t -> String.trim (prod_to_prodn t)) @@ -1923,17 +1927,20 @@ let process_grammar args = list, StringSet.of_list list in let tac_list, tac_prods = plist "simple_tactic" in let cmd_list, cmd_prods = plist "command" in - let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files; report_omitted_prods !g.order !seen.nts "Nonterminal" ""; let out = open_out (dir "updated_rsts") in close_out out; + end; + (* if args.check_tacs then report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; if args.check_cmds then report_omitted_prods cmd_list !seen.cmds "Command" "\n "; *) + + if !exit_code = 0 then begin (* generate report on cmds or tacs *) let cmdReport outfile cmdStr cmd_nts cmds cmdvs = let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmds)) in @@ -1942,7 +1949,7 @@ let process_grammar args = StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map))) ) StringSet.empty cmd_nts in let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in - let out = open_out_bin (dir outfile) in + let out = open_temp_bin (dir outfile) in StringSet.iter (fun c -> let rsts = StringSet.mem c rstCmds in let gram = StringSet.mem c gramCmds in @@ -1956,6 +1963,7 @@ let process_grammar args = fprintf out "%s%s %s\n" pfx var c) allCmds; close_out out; + finish_with_file (dir outfile) args; Printf.printf "# %s in rsts, gram, total = %d %d %d\n" cmdStr (StringSet.cardinal gramCmds) (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds); in @@ -1973,7 +1981,7 @@ let process_grammar args = let out = open_temp_bin (dir "prodnGrammar") in print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty; close_out out; - finish_with_file (dir "prodnGrammar") args.verify + finish_with_file (dir "prodnGrammar") args end end @@ -1985,6 +1993,7 @@ let parse_args () = | "-check-cmds" -> { args with check_cmds = true } | "-check-tacs" -> { args with check_tacs = true } | "-no-warn" -> show_warn := false; { args with show_warn = true } + | "-no-update" -> { args with no_update = true } | "-short" -> { args with fullGrammar = true } | "-verbose" -> { args with verbose = true } | "-verify" -> { args with verify = true } diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 3afa21f2cf..fba4856241 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -5,26 +5,47 @@ (env (_ (binaries doc_grammar.exe))) (rule - (targets fullGrammar) + (alias check-gram) (deps - ; Main grammar - (glob_files %{project_root}/parsing/*.mlg) - (glob_files %{project_root}/toplevel/*.mlg) - (glob_files %{project_root}/vernac/*.mlg) - ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) - (glob_files %{project_root}/plugins/btauto/*.mlg) - (glob_files %{project_root}/plugins/cc/*.mlg) - (glob_files %{project_root}/plugins/derive/*.mlg) - (glob_files %{project_root}/plugins/extraction/*.mlg) - (glob_files %{project_root}/plugins/firstorder/*.mlg) - (glob_files %{project_root}/plugins/funind/*.mlg) - (glob_files %{project_root}/plugins/ltac/*.mlg) - (glob_files %{project_root}/plugins/micromega/*.mlg) - (glob_files %{project_root}/plugins/nsatz/*.mlg) - (glob_files %{project_root}/plugins/omega/*.mlg) - (glob_files %{project_root}/plugins/rtauto/*.mlg) - (glob_files %{project_root}/plugins/setoid_ring/*.mlg) - (glob_files %{project_root}/plugins/syntax/*.mlg)) + (:input + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect and Ltac2 for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (glob_files %{project_root}/plugins/ltac/*.mlg) + (glob_files %{project_root}/plugins/micromega/*.mlg) + (glob_files %{project_root}/plugins/nsatz/*.mlg) + (glob_files %{project_root}/plugins/omega/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg) + ; Sphinx files + (glob_files %{project_root}/doc/sphinx/language/*.rst) + (glob_files %{project_root}/doc/sphinx/proof-engine/*.rst) + (glob_files %{project_root}/doc/sphinx/user-extensions/*.rst) + (glob_files %{project_root}/doc/sphinx/practical-tools/*.rst) + (glob_files %{project_root}/doc/sphinx/addendum/*.rst) + (glob_files %{project_root}/doc/sphinx/language/core/*.rst) + (glob_files %{project_root}/doc/sphinx/language/extensions/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/writing-proofs/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/automatic-tactics/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/creating-tactics/*.rst) + (glob_files %{project_root}/doc/sphinx/using/libraries/*.rst) + (glob_files %{project_root}/doc/sphinx/using/tools/*.rst)) + common.edit_mlg + orderedGrammar) (action - (chdir %{project_root} (run doc_grammar -short -no-warn %{deps}))) - (mode promote)) + (progn + (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.old; done") + (chdir %{project_root} (run doc_grammar -check-cmds %{input})) + (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.new; done") + (bash "for f in fullGrammar orderedGrammar; do cp ${f}.old ${f}; done") + (diff? fullGrammar fullGrammar.new) + (diff? orderedGrammar orderedGrammar.new)))) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 241cf48cf1..272d17bb35 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1244,8 +1244,6 @@ query_command: [ | "SearchPattern" constr_pattern in_or_out_modules "." | "SearchRewrite" constr_pattern in_or_out_modules "." | "Search" searchabout_query searchabout_queries "." -| "SearchAbout" searchabout_query searchabout_queries "." -| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." ] printable: [ @@ -2454,8 +2452,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 38e7b781df..0c9d7a853b 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -918,8 +918,6 @@ command: [ | "SearchPattern" one_term OPT ne_in_or_out_modules | "SearchRewrite" one_term OPT ne_in_or_out_modules | "Search" searchabout_query OPT searchabout_queries -| "SearchAbout" searchabout_query OPT searchabout_queries -| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules | "Time" command | "Redirect" string command | "Timeout" num command @@ -1441,8 +1439,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" ] as_name: [ diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index c5883cef0d..711986c2b2 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -207,7 +207,6 @@ let state_preserving = [ "Recursive Extraction Library"; "Search"; - "SearchAbout (* deprecated *)"; "SearchHead"; "SearchPattern"; "SearchRewrite"; diff --git a/ide/microPG.ml b/ide/microPG.ml index 46d3316ef6..5a4871b70a 100644 --- a/ide/microPG.ml +++ b/ide/microPG.ml @@ -289,7 +289,6 @@ let pg = insert pg "Proof General" [mC,_c,"c"; mC,_a,"a"] [ mkE _p "p" "Print" (Callback (fun gui -> command gui "Print")); mkE _c "c" "Check" (Callback (fun gui -> command gui "Check")); mkE _b "b" "About" (Callback (fun gui -> command gui "About")); - mkE _a "a" "Search About" (Callback (fun gui -> command gui "SearchAbout")); mkE _o "o" "Search Pattern" (Callback (fun gui->command gui "SearchPattern")); mkE _l "l" "Locate" (Callback (fun gui -> command gui "Locate")); mkE _Return "RET" "match template" (Action("Templates","match")); diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index dcb71d96a1..a7f8c70499 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -8,17 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module StringOrd = -struct - type t = string - let compare s1 s2 = - (* we use first size, then usual comparison *) - let d = String.length s1 - String.length s2 in - if d <> 0 then d - else compare s1 s2 -end - -module Proposals = Set.Make(StringOrd) +module Proposals = CString.Set (** Retrieve completion proposals in the buffer *) let get_syntactic_completion (buffer : GText.buffer) pattern accu = diff --git a/kernel/float64.ml b/kernel/float64.ml index 299f53e8ab..53fc13b04b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -21,12 +21,19 @@ let is_neg_infinity f = f = neg_infinity (* Printing a binary64 float in 17 decimal places and parsing it again will yield the same float. We assume [to_string_raw] is not given a - [nan] as input. *) + [nan] or an infinity as input. *) let to_string_raw f = Printf.sprintf "%.17g" f (* OCaml gives a sign to nan values which should not be displayed as - all NaNs are considered equal here *) -let to_string f = if is_nan f then "nan" else to_string_raw f + all NaNs are considered equal here. + OCaml prints infinities as "inf" (resp. "-inf") + but we want "infinity" (resp. "neg_infinity"). *) +let to_string f = + if is_nan f then "nan" + else if is_infinity f then "infinity" + else if is_neg_infinity f then "neg_infinity" + else to_string_raw f + let of_string = float_of_string (* Compiles a float to OCaml code *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 4c66f1574f..a4465c293b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -169,9 +169,6 @@ let subst_of_rel_context_instance sign l = | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") in aux [] (List.rev sign) l -let adjust_subst_to_rel_context sign l = - List.rev (subst_of_rel_context_instance sign l) - let adjust_rel_to_rel_context sign n = let rec aux sign = let open RelDecl in diff --git a/kernel/vars.mli b/kernel/vars.mli index 52a6159f0a..0aac5ed4ce 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -72,9 +72,6 @@ type substl = constr list [c₁], as if usable for [substl]. *) val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl -(** For compatibility: returns the substitution reversed *) -val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list - (** Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int diff --git a/lib/system.ml b/lib/system.ml index 68410e322a..d7f5fa26ab 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -11,7 +11,6 @@ (* $Id$ *) open Pp -open Util include Minisys @@ -42,15 +41,7 @@ let all_subdirs ~unix_path:root = (* Caching directory contents for efficient syntactic equality of file names even on case-preserving but case-insensitive file systems *) -module StrMod = struct - type t = string - let compare = compare -end - -module StrMap = Map.Make(StrMod) -module StrSet = Set.Make(StrMod) - -let dirmap = ref StrMap.empty +let dirmap = ref CString.Map.empty let make_dir_table dir = let entries = @@ -59,8 +50,8 @@ let make_dir_table dir = with Sys_error _ -> warn_cannot_open_dir dir; [||] in - let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in - Array.fold_left filter_dotfiles StrSet.empty entries + let filter_dotfiles s f = if f.[0] = '.' then s else CString.Set.add f s in + Array.fold_left filter_dotfiles CString.Set.empty entries (** Don't trust in interactive mode (the default) *) let trust_file_cache = ref false @@ -68,20 +59,20 @@ let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = let contents = make_dir_table dir in - dirmap := StrMap.add dir contents !dirmap; + dirmap := CString.Map.add dir contents !dirmap; contents in let contents, fresh = try (* in batch mode, assume the directory content is still fresh *) - StrMap.find dir !dirmap, !trust_file_cache + CString.Map.find dir !dirmap, !trust_file_cache with Not_found -> (* in batch mode, we are not yet sure the directory exists *) - if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true + if !trust_file_cache && not (exists_dir dir) then CString.Set.empty, true else cache_dir dir, true in - StrSet.mem bf contents || + CString.Set.mem bf contents || not fresh && (* rescan, there is a new file we don't know about *) - StrSet.mem bf (cache_dir dir) + CString.Set.mem bf (cache_dir dir) let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase diff --git a/library/libnames.ml b/library/libnames.ml index 6f55a8dc3d..88b2e41855 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -78,9 +78,6 @@ let dirpath_of_string s = in DirPath.make path -module Dirset = Set.Make(DirPath) -module Dirmap = Map.Make(DirPath) - (*s Section paths are absolute names *) type full_path = { diff --git a/library/libnames.mli b/library/libnames.mli index 23792e54c2..a384510879 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names (** {6 Dirpaths } *) @@ -34,9 +33,6 @@ val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool -module Dirset : Set.S with type elt = DirPath.t -module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset - (** {6 Full paths are {e absolute} paths of declarations } *) type full_path diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index df6189f212..4b78e64d98 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -402,7 +402,7 @@ let rec interp_search_about args accu = match args with | [] -> accu | (flag, arg) :: rem -> fun gr env typ -> - let ans = Search.search_about_filter arg gr env typ in + let ans = Search.search_filter arg gr env typ in (if flag then ans else not ans) && interp_search_about rem accu gr env typ let interp_search_arg arg = diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index dadce9a9ea..e0a9906689 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -22,8 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) (*** Parsing for float in digital notation ***) +let warn_inexact_float = + CWarnings.create ~name:"inexact-float" ~category:"parsing" + (fun (sn, f) -> + Pp.strbrk + (Printf.sprintf + "The constant %s is not a binary64 floating-point value. \ + A closest value will be used and unambiguously printed %s." + sn (Float64.to_string f))) + let interp_float ?loc n = - DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n))) + let sn = NumTok.Signed.to_string n in + let f = Float64.of_string sn in + (* return true when f is not exactly equal to n, + this is only used to decide whether or not to display a warning + and does not play any actual role in the parsing *) + let inexact () = match Float64.classify f with + | Float64.(PInf | NInf | NaN) -> true + | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n) + | Float64.(PNormal | NNormal | PSubn | NSubn) -> + let m, e = + let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in + let i = NumTok.UnsignedNat.to_string i in + let f = match f with + | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in + let e = match e with + | None -> "0" | Some e -> NumTok.SignedNat.to_string e in + Bigint.of_string (i ^ f), + (try int_of_string e with Failure _ -> 0) - String.length f in + let m', e' = + let m', e' = Float64.frshiftexp f in + let m' = Float64.normfr_mantissa m' in + let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in + Bigint.of_string (Uint63.to_string m'), + e' in + let c2, c5 = Bigint.(of_int 2, of_int 5) in + (* check m*5^e <> m'*2^e' *) + let check m e m' e' = + not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in + (* check m*5^e*2^e' <> m' *) + let check' m e e' m' = + not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in + (* we now have to check m*10^e <> m'*2^e' *) + if e >= 0 then + if e <= e' then check m e m' (e' - e) + else check' m e (e - e') m' + else (* e < 0 *) + if e' <= e then check m' (-e) m (e - e') + else check' m' (-e) (e' - e) m in + if inexact () then warn_inexact_float ?loc (sn, f); + DAst.make ?loc (GFloat f) (* Pretty printing is already handled in constrextern.ml *) diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index d6458e1409..49401a9937 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -67,8 +67,6 @@ end module ClTypMap = Map.Make(ClTyp) -module IntMap = Map.Make(Int) - let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0 type inheritance_path = coe_info_typ list @@ -97,13 +95,13 @@ struct module Index = struct include Int let print = Pp.int end - type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t } - let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty } + type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t } + let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty } let mem y b = ClTypMap.mem y b.inv - let map x b = IntMap.find x b.v - let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v)) + let map x b = Int.Map.find x b.v + let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v)) let add x y b = - { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv } + { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv } let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv []) end diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 64068724af..d4da93cc5b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -73,7 +73,7 @@ let type_constructor mind mib u (ctx, typ) params = if Int.equal ndecls 0 then ctyp else let _,ctyp = decompose_prod_n_assum ndecls ctyp in - substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + substl (subst_of_rel_context_instance mib.mind_params_ctxt (Array.to_list params)) ctyp diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index fb91ea7b5c..d73d1f2d1a 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -85,8 +85,6 @@ let log_out_ch = ref stdout let cprintf s = cfprintf !log_out_ch s [@@@ocaml.warning "+32"] -module StringMap = Map.Make(String);; - let tokenize_string s = (* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too. But I don't understand how it's used--it looks like things get appended to it but @@ -124,22 +122,22 @@ type hyp_info = { let diff_hyps o_line_idents o_map n_line_idents n_map = let rv : Pp.t list ref = ref [] in - let is_done ident map = (StringMap.find ident map).done_ in + let is_done ident map = (CString.Map.find ident map).done_ in let exists ident map = - try let _ = StringMap.find ident map in true + try let _ = CString.Map.find ident map in true with Not_found -> false in let contains l ident = try [List.find (fun x -> x = ident) l] with Not_found -> [] in let output old_ids_uo new_ids = (* use the order from the old line in case it's changed in the new *) let old_ids = if old_ids_uo = [] then [] else - let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in + let orig = (CString.Map.find (List.hd old_ids_uo) o_map).idents in List.concat (List.map (contains orig) old_ids_uo) in let setup ids map = if ids = [] then ("", Pp.mt ()) else let open Pp in - let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in + let rhs_pp = (CString.Map.find (List.hd ids) map).rhs_pp in let pp_ids = List.map (fun x -> str x) ids in let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in (string_of_ppcmds hyp_pp, hyp_pp) @@ -151,11 +149,11 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = let hyp_diffs = diff_str ~tokenize_string o_line n_line in let (has_added, has_removed) = has_changes hyp_diffs in if show_removed () && has_removed then begin - List.iter (fun x -> (StringMap.find x o_map).done_ <- true) old_ids; + List.iter (fun x -> (CString.Map.find x o_map).done_ <- true) old_ids; rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv; end; if n_line <> "" then begin - List.iter (fun x -> (StringMap.find x n_map).done_ <- true) new_ids; + List.iter (fun x -> (CString.Map.find x n_map).done_ <- true) new_ids; rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv end in @@ -166,14 +164,14 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = match dtype with | `Removed -> if dtype = `Removed then begin - let o_idents = (StringMap.find ident o_map).idents in + let o_idents = (CString.Map.find ident o_map).idents in (* only show lines that have all idents removed here; other removed idents appear later *) if show_removed () && not (is_done ident o_map) && List.for_all (fun x -> not (exists x n_map)) o_idents then output (List.rev o_idents) [] end | _ -> begin (* Added or Common case *) - let n_idents = (StringMap.find ident n_map).idents in + let n_idents = (CString.Map.find ident n_map).idents in (* Process a new hyp line, possibly splitting it. Duplicates some of process_ident iteration, but easier to understand this way *) @@ -184,13 +182,13 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = let fst_omap_idents = ref None in let add ids id map = ids := id :: !ids; - (StringMap.find id map).done_ <- true in + (CString.Map.find id map).done_ <- true in (* get identifiers shared by one old and one new line, plus other Added in new and other Removed in old *) let process_split ident3 = if not (is_done ident3 n_map) then begin - let this_omap_idents = try Some (StringMap.find ident3 o_map).idents + let this_omap_idents = try Some (CString.Map.find ident3 o_map).idents with Not_found -> None in if !fst_omap_idents = None then fst_omap_idents := this_omap_idents; @@ -290,7 +288,7 @@ map will contain: concl_pp is the conclusion as a Pp.t *) let goal_info goal sigma = - let map = ref StringMap.empty in + let map = ref CString.Map.empty in let line_idents = ref [] in let build_hyp_info env sigma hyp = let (names, body, ty) = hyp in @@ -308,7 +306,7 @@ let goal_info goal sigma = let rhs_pp = mid ++ str " : " ++ ts in let make_entry () = { idents; rhs_pp; done_ = false } in - List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents + List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents in try @@ -339,7 +337,7 @@ let unwrap g_s = let goal = Evd.sig_it g_s in let sigma = Refiner.project g_s in goal_info goal sigma - | None -> ([], StringMap.empty, Pp.mt ()) + | None -> ([], CString.Map.empty, Pp.mt ()) let diff_goal_ide og_s ng nsigma = diff_goal_info (unwrap og_s) (goal_info ng nsigma) @@ -405,7 +403,7 @@ the call to db_goal_map and entering the following: (conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof *) let match_goals ot nt = - let nevar_to_oevar = ref StringMap.empty in + let nevar_to_oevar = ref CString.Map.empty in (* ogname is "" when there is no difference on the current path. It's set to the old goal's evar name once a rewritten goal is found, at which point the code only searches for the replacing goals @@ -514,7 +512,7 @@ let match_goals ot nt = | CPatVar _, CPatVar _ -> () | CEvar (n,l), CEvar (n2,l2) -> let oevar = if ogname = "" then Id.to_string n else ogname in - nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar; + nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar; iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) @@ -641,16 +639,16 @@ let make_goal_map_i op np = (* >= 2 removals, >= 1 addition, need to match *) let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in - let oevar_to_og = ref StringMap.empty in + let oevar_to_og = ref CString.Map.empty in let Proof.{sigma=osigma} = Proof.data op in - List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og) + List.iter (fun og -> oevar_to_og := CString.Map.add (goal_to_evar og osigma) og !oevar_to_og) (Goal.Set.elements rem_gs); let Proof.{sigma=nsigma} = Proof.data np in let get_og ng = let nevar = goal_to_evar ng nsigma in - let oevar = StringMap.find nevar nevar_to_oevar in - let og = StringMap.find oevar !oevar_to_og in + let oevar = CString.Map.find nevar nevar_to_oevar in + let og = CString.Map.find oevar !oevar_to_og in og in Goal.Set.iter (fun ng -> diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 83e721d3d5..24b171770a 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -83,11 +83,4 @@ type hyp_info = { mutable done_: bool; } -module StringMap : -sig - type +'a t - val empty: hyp_info t - val add : string -> hyp_info -> hyp_info t -> hyp_info t -end - -val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list +val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list diff --git a/proofs/goal.ml b/proofs/goal.ml index ede68e63b9..b1f8fd3e97 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -131,4 +131,4 @@ module V82 = struct end -module Set = Set.Make(struct type t = goal let compare = Evar.compare end) +module Set = Evar.Set diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v index 42b1244fb5..caa7373f5e 100644 --- a/test-suite/bugs/closed/HoTT_coq_010.v +++ b/test-suite/bugs/closed/HoTT_coq_010.v @@ -1,3 +1,3 @@ -SearchAbout and. +Search and. (* Anomaly: Mismatched instance and context when building universe substitution. Please report. *) diff --git a/test-suite/bugs/closed/bug_3900.v b/test-suite/bugs/closed/bug_3900.v index 6be2161c2f..ddede74acc 100644 --- a/test-suite/bugs/closed/bug_3900.v +++ b/test-suite/bugs/closed/bug_3900.v @@ -9,5 +9,5 @@ Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type. Class Foo (x : Type) := { _ : forall y, y }. Local Instance ishset_pmor {s d m} : Foo (Pmor s d m). Proof. -SearchAbout ((forall _ _, _) -> Foo _). +Search ((forall _ _, _) -> Foo _). Abort. diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out index cfd6633752..dd8189c56f 100644 --- a/test-suite/output/FloatExtraction.out +++ b/test-suite/output/FloatExtraction.out @@ -1,3 +1,17 @@ +File "stdin", line 25, characters 8-12: +Warning: The constant 0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed 0.01. [inexact-float,parsing] +File "stdin", line 25, characters 20-25: +Warning: The constant -0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed -0.01. [inexact-float,parsing] +File "stdin", line 25, characters 27-35: +Warning: The constant 1.7e+308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 1.6999999999999999e+308. +[inexact-float,parsing] +File "stdin", line 25, characters 37-46: +Warning: The constant -1.7e-308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-1.7000000000000002e-308. [inexact-float,parsing] (** val infinity : Float64.t **) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 668a55977d..7941d2e647 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -4,8 +4,16 @@ : float (-2.5)%float : float +File "stdin", line 9, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123%float : float +File "stdin", line 10, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] (-2.5000000000000001e-123)%float : float (2 + 2)%float @@ -18,14 +26,34 @@ : float -2.5 : float +File "stdin", line 19, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123 : float +File "stdin", line 20, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] -2.5000000000000001e-123 : float 2 + 2 : float 2.5 + 2.5 : float +File "stdin", line 24, characters 6-11: +Warning: The constant 1e309 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed infinity. +[inexact-float,parsing] +infinity + : float +File "stdin", line 25, characters 6-12: +Warning: The constant -1e309 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed neg_infinity. +[inexact-float,parsing] +neg_infinity + : float 2 : nat 2%float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 85f611352c..eca712db10 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -21,6 +21,9 @@ Check (-2.5e-123). Check (2 + 2). Check (2.5 + 2.5). +Check 1e309. +Check -1e309. + Open Scope nat_scope. Check 2. diff --git a/test-suite/success/search.v b/test-suite/success/search.v new file mode 100644 index 0000000000..92de43e052 --- /dev/null +++ b/test-suite/success/search.v @@ -0,0 +1,35 @@ + +(** Test of the different syntaxes of Search *) + +Search plus. +Search plus mult. +Search "plus_n". +Search plus "plus_n". +Search "*". +Search "*" "+". + +Search plus inside Peano. +Search plus mult inside Peano. +Search "plus_n" inside Peano. +Search plus "plus_n" inside Peano. +Search "*" inside Peano. +Search "*" "+" inside Peano. + +Search plus outside Peano Logic. +Search plus mult outside Peano Logic. +Search "plus_n" outside Peano Logic. +Search plus "plus_n" outside Peano Logic. +Search "*" outside Peano Logic. +Search "*" "+" outside Peano Logic. + +Search -"*" "+" outside Logic. +Search -"*"%nat "+"%nat outside Logic. + + +(** The example in the Reference Manual *) + +Require Import ZArith. + +Search Z.mul Z.add "distr". +Search "+"%Z "*"%Z "distr" -positive -Prop. +Search (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v deleted file mode 100644 index 9edfd82556..0000000000 --- a/test-suite/success/searchabout.v +++ /dev/null @@ -1,60 +0,0 @@ - -(** Test of the different syntaxes of SearchAbout, in particular - with and without the [ ... ] delimiters *) - -SearchAbout plus. -SearchAbout plus mult. -SearchAbout "plus_n". -SearchAbout plus "plus_n". -SearchAbout "*". -SearchAbout "*" "+". - -SearchAbout plus inside Peano. -SearchAbout plus mult inside Peano. -SearchAbout "plus_n" inside Peano. -SearchAbout plus "plus_n" inside Peano. -SearchAbout "*" inside Peano. -SearchAbout "*" "+" inside Peano. - -SearchAbout plus outside Peano Logic. -SearchAbout plus mult outside Peano Logic. -SearchAbout "plus_n" outside Peano Logic. -SearchAbout plus "plus_n" outside Peano Logic. -SearchAbout "*" outside Peano Logic. -SearchAbout "*" "+" outside Peano Logic. - -SearchAbout -"*" "+" outside Logic. -SearchAbout -"*"%nat "+"%nat outside Logic. - -SearchAbout [plus]. -SearchAbout [plus mult]. -SearchAbout ["plus_n"]. -SearchAbout [plus "plus_n"]. -SearchAbout ["*"]. -SearchAbout ["*" "+"]. - -SearchAbout [plus] inside Peano. -SearchAbout [plus mult] inside Peano. -SearchAbout ["plus_n"] inside Peano. -SearchAbout [plus "plus_n"] inside Peano. -SearchAbout ["*"] inside Peano. -SearchAbout ["*" "+"] inside Peano. - -SearchAbout [plus] outside Peano Logic. -SearchAbout [plus mult] outside Peano Logic. -SearchAbout ["plus_n"] outside Peano Logic. -SearchAbout [plus "plus_n"] outside Peano Logic. -SearchAbout ["*"] outside Peano Logic. -SearchAbout ["*" "+"] outside Peano Logic. - -SearchAbout [-"*" "+"] outside Logic. -SearchAbout [-"*"%nat "+"%nat] outside Logic. - - -(** The example in the Reference Manual *) - -Require Import ZArith. - -SearchAbout Z.mul Z.add "distr". -SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. -SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6126d9c37d..71ba3e645d 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -43,5 +43,5 @@ Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. -(* Default substrings not considered by queries like SearchAbout *) +(* Default substrings not considered by queries like Search *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 1c790a37a0..f6b2544b6e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -2226,7 +2226,7 @@ Section Int31_Specs. < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2. Proof. revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. - intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith. + intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct. 1-3: lia. intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-3: lia. intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt312_step_correct; auto. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index a8c645deb2..c4f738ac39 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1316,9 +1316,8 @@ Lemma iter_sqrt_correct n rec i j: 0 < φ i -> 0 < φ j -> φ (iter_sqrt n rec i j) ^ 2 <= φ i < (φ (iter_sqrt n rec i j) + 1) ^ 2. Proof. revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n. - intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Zpower_0_r; auto with zarith. + intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct. 1-4: lia. + intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith. intros n Hrec rec i j Hi Hj Hij H31 HHrec. apply sqrt_step_correct; auto. intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. @@ -1516,9 +1515,8 @@ Lemma iter2_sqrt_correct n rec ih il j: < (φ (iter2_sqrt n rec ih il j) + 1) ^ 2. Proof. revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n. - intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Zpower_0_r; auto with zarith. + intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct. 1-3: lia. + intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith. intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt2_step_correct; auto. intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. diff --git a/theories/omega/Omega.v b/theories/omega/Omega.v index 9c2e8a9212..10a5aa47b3 100644 --- a/theories/omega/Omega.v +++ b/theories/omega/Omega.v @@ -19,6 +19,7 @@ Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. +Require Import Lia. Declare ML Module "omega_plugin". @@ -28,28 +29,28 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l Require Export Zhints. -Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith. -Hint Extern 10 (_ <= _) => abstract omega: zarith. -Hint Extern 10 (_ < _) => abstract omega: zarith. -Hint Extern 10 (_ >= _) => abstract omega: zarith. -Hint Extern 10 (_ > _) => abstract omega: zarith. - -Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith. -Hint Extern 10 (~ _ <= _) => abstract omega: zarith. -Hint Extern 10 (~ _ < _) => abstract omega: zarith. -Hint Extern 10 (~ _ >= _) => abstract omega: zarith. -Hint Extern 10 (~ _ > _) => abstract omega: zarith. - -Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith. -Hint Extern 10 (_ <= _)%Z => abstract omega: zarith. -Hint Extern 10 (_ < _)%Z => abstract omega: zarith. -Hint Extern 10 (_ >= _)%Z => abstract omega: zarith. -Hint Extern 10 (_ > _)%Z => abstract omega: zarith. - -Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith. -Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith. -Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith. -Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith. -Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith. - -Hint Extern 10 False => abstract omega: zarith. +Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith. +Hint Extern 10 (_ <= _) => abstract lia: zarith. +Hint Extern 10 (_ < _) => abstract lia: zarith. +Hint Extern 10 (_ >= _) => abstract lia: zarith. +Hint Extern 10 (_ > _) => abstract lia: zarith. + +Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith. +Hint Extern 10 (~ _ <= _) => abstract lia: zarith. +Hint Extern 10 (~ _ < _) => abstract lia: zarith. +Hint Extern 10 (~ _ >= _) => abstract lia: zarith. +Hint Extern 10 (~ _ > _) => abstract lia: zarith. + +Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith. +Hint Extern 10 (_ <= _)%Z => abstract lia: zarith. +Hint Extern 10 (_ < _)%Z => abstract lia: zarith. +Hint Extern 10 (_ >= _)%Z => abstract lia: zarith. +Hint Extern 10 (_ > _)%Z => abstract lia: zarith. + +Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith. + +Hint Extern 10 False => abstract lia: zarith. diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d2b0078a7c..862715753d 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -42,7 +42,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite"; + "Search"; "SearchHead"; "SearchPattern"; "SearchRewrite"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dd75693c5b..a8f1a49086 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -983,13 +983,6 @@ GRAMMAR EXTEND Gram { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } - (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> - { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } - (* compatibility: SearchAbout with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules; "." -> - { fun g -> VernacSearch (SearchAbout sl,g, l) } ] ] ; printable: diff --git a/vernac/library.ml b/vernac/library.ml index 85645b92d4..7c629b08e7 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -103,17 +103,13 @@ type library_summary = { libsum_digests : Safe_typing.vodigest; } -module LibraryOrdered = DirPath -module LibraryMap = Map.Make(LibraryOrdered) -module LibraryFilenameMap = Map.Make(LibraryOrdered) - (* This is a map from names to loaded libraries *) -let libraries_table : library_summary LibraryMap.t ref = - Summary.ref LibraryMap.empty ~name:"LIBRARY" +let libraries_table : library_summary DPmap.t ref = + Summary.ref DPmap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) -let libraries_filename_table = ref LibraryFilenameMap.empty +let libraries_filename_table = ref DPmap.empty (* These are the _ordered_ sets of loaded, imported and exported libraries *) let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" @@ -121,7 +117,7 @@ let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" (* various requests to the tables *) let find_library dir = - LibraryMap.find dir !libraries_table + DPmap.find dir !libraries_table let try_find_library dir = try find_library dir @@ -133,16 +129,16 @@ let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) (* from a previous play of the session *) libraries_filename_table := - LibraryFilenameMap.add dir f !libraries_filename_table + DPmap.add dir f !libraries_filename_table let library_full_filename dir = - try LibraryFilenameMap.find dir !libraries_filename_table + try DPmap.find dir !libraries_filename_table with Not_found -> "<unavailable filename>" let overwrite_library_filenames f = let f = if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in - LibraryMap.iter (fun dir _ -> register_library_filename dir f) + DPmap.iter (fun dir _ -> register_library_filename dir f) !libraries_table let library_is_loaded dir = @@ -167,7 +163,7 @@ let register_loaded_library m = | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add libname m !libraries_table + libraries_table := DPmap.add libname m !libraries_table let loaded_libraries () = !libraries_loaded_list @@ -187,13 +183,13 @@ type 'a table_status = | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) + ref (DPmap.empty : (Opaqueproof.opaque_proofterm table_status) DPmap.t) let add_opaque_table dp st = - opaque_tables := LibraryMap.add dp st !opaque_tables + opaque_tables := DPmap.add dp st !opaque_tables let access_table what tables dp i = - let t = match LibraryMap.find dp !tables with + let t = match DPmap.find dp !tables with | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in @@ -206,7 +202,7 @@ let access_table what tables dp i = str ") is inaccessible or corrupted,\ncannot load some " ++ str what ++ str " in it.\n") in - tables := LibraryMap.add dp (Fetched t) !tables; + tables := DPmap.add dp (Fetched t) !tables; t in assert (i < Array.length t); t.(i) @@ -261,14 +257,12 @@ let intern_from_file f = | Some (_,false) -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty -module DPMap = Map.Make(DirPath) - let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) - try (DPMap.find dir contents).library_digests, (needed, contents) + try (DPmap.find dir contents).library_digests, (needed, contents) with Not_found -> Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) @@ -286,7 +280,7 @@ and intern_library_deps ~lib_resolver libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library ~lib_resolver dir from) libs m.library_deps in - (dir :: needed, DPMap.add dir m contents ) + (dir :: needed, DPmap.add dir m contents ) and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in @@ -372,8 +366,8 @@ let warn_require_in_module = strbrk "and optionally Import it inside another one.") let require_library_from_dirpath ~lib_resolver modrefl export = - let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in - let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in + let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPmap.empty) modrefl in + let needed = List.rev_map (fun dir -> DPmap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin @@ -500,14 +494,11 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let save_library_raw f sum lib univs proofs = save_library_base f sum lib (Some univs) None proofs -module StringOrd = struct type t = string let compare = String.compare end -module StringSet = Set.Make(StringOrd) - let get_used_load_paths () = - StringSet.elements - (List.fold_left (fun acc m -> StringSet.add + String.Set.elements + (List.fold_left (fun acc m -> String.Set.add (Filename.dirname (library_full_filename m)) acc) - StringSet.empty !libraries_loaded_list) + String.Set.empty !libraries_loaded_list) let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a3de88d4dc..054b60853f 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -142,7 +142,7 @@ open Pputils | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - let pr_search_about (b,c) = + let pr_search (b,c) = (if b then str "-" else mt()) ++ match c with | SearchSubPattern p -> @@ -158,10 +158,8 @@ open Pputils | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout sl -> - keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b | Search sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b let pr_option_ref_value = function | QualidRefValue id -> pr_qualid id diff --git a/vernac/search.ml b/vernac/search.ml index ceff8acc79..68a30b4231 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration type filter_function = GlobRef.t -> env -> constr -> bool type display_function = GlobRef.t -> env -> constr -> unit -(* This option restricts the output of [SearchPattern ...], -[SearchAbout ...], etc. to the names of the symbols matching the +(* This option restricts the output of [SearchPattern ...], etc. +to the names of the symbols matching the query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) @@ -226,7 +226,7 @@ let module_filter (mods, outside) ref env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_about_filter query gr env typ = match query with +let search_filter query gr env typ = match query with | GlobSearchSubPattern pat -> Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) | GlobSearchString s -> @@ -283,14 +283,14 @@ let search_by_head ?pstate gopt pat mods pr_search = in generic_search ?pstate gopt iter -(** SearchAbout *) +(** Search *) -let search_about ?pstate gopt items mods pr_search = +let search ?pstate gopt items mods pr_search = let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && List.for_all - (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items && + (fun (b,i) -> eqb b (search_filter i ref env typ)) items && blacklist_filter ref env typ in let iter ref env typ = diff --git a/vernac/search.mli b/vernac/search.mli index 11dd0c6794..6dbbff3a8c 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -30,8 +30,7 @@ val blacklist_filter : filter_function val module_filter : DirPath.t list * bool -> filter_function (** Check whether a reference pertains or not to a set of modules *) -val search_about_filter : glob_search_about_item -> filter_function -(** Check whether a reference matches a SearchAbout query. *) +val search_filter : glob_search_about_item -> filter_function (** {6 Specialized search functions} @@ -45,7 +44,7 @@ val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> D -> display_function -> unit val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list +val search : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8641c67d9f..963b5f2084 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1773,10 +1773,6 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let warn_deprecated_search_about = - CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" - (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") - let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1809,12 +1805,8 @@ let vernac_search ~pstate ~atts s gopt r = (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchAbout sl -> - warn_deprecated_search_about (); - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search | Search sl -> - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search); Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b7c6d3c490..d6e7a3947a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -69,7 +69,6 @@ type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | SearchAbout of (bool * search_about_item) list | Search of (bool * search_about_item) list type locatable = |