diff options
175 files changed, 854 insertions, 598 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9e96d3602b..536bd0af76 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -121,7 +121,7 @@ before_script: OPAM_VARIANT: "+flambda" artifacts: name: "$CI_JOB_NAME" - expire_in: 1 month + expire_in: 2 months # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -140,6 +140,7 @@ before_script: name: "$CI_JOB_NAME" paths: - _install_ci/share/doc/coq/ + expire_in: 2 months # set dependencies when using .test-suite-template: @@ -159,6 +160,8 @@ before_script: when: on_failure paths: - test-suite/logs + # Gitlab doesn't support yet "expire_in: never" so we use the instance default + # expire_in: never variables: timeout: "" @@ -177,7 +180,7 @@ before_script: name: "$CI_JOB_NAME.logs" paths: - coqchk.log - expire_in: 1 month + expire_in: 2 months .ci-template: stage: test @@ -341,6 +344,8 @@ pkg:opam: when: on_failure paths: - nix-build-coq.drv-0/*/test-suite/logs + # Gitlab doesn't support yet "expire_in: never" so we use the instance default + # expire_in: never pkg:nix:deploy: extends: .nix-template @@ -465,6 +470,8 @@ test-suite:egde:dune:dev: when: on_failure paths: - _build/default/test-suite/logs + # Gitlab doesn't support yet "expire_in: never" so we use the instance default + # expire_in: never test-suite:edge+trunk+make: stage: test @@ -6,7 +6,7 @@ ## To avoid spam issues, we use by default a pseudo-email <login@gforge> ## for all persons that haven't made commits with real emails ## -## If you're mentionned here and want to update your information, +## If you're mentioned here and want to update your information, ## either amend this file and commit it, or contact the coqdev list Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com> diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 31fa3d2c4a..e811c116b6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -31,7 +31,7 @@ account). You can file a bug for any of the following: It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports. If unsure, you are always very welcome to ask on our [Discourse forum][] -or [Gitter chat][] before, after, or while writting a bug report +or [Gitter chat][] before, after, or while writing a bug report When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not @@ -170,6 +170,7 @@ of the Coq Proof assistant during the indicated time: Nickolai Zeldovich (MIT 2014-2016) Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806, INRIA-PPS then IRIF, 2015-now) + Talia Ringer (UW, 2019) *************************************************************************** INRIA refers to: diff --git a/Makefile.build b/Makefile.build index 034c9ea03c..147668187f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -150,7 +150,7 @@ endif ########################################################################### -# This include below will lauch the build of all .d. +# This include below will launch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d). diff --git a/Makefile.dev b/Makefile.dev index 13b85dfad4..6057696375 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -8,7 +8,7 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## -# Extra targets for developpers : +# Extra targets for developers : # debug printers, revision, partial targets ... ######################### diff --git a/Makefile.doc b/Makefile.doc index 25d146000b..94642e702f 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -167,7 +167,7 @@ doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li $(PDFLATEX) -interaction=batchmode Library;\ ../tools/show_latex_messages -no-overfull Library.log) -### Standard library (full version if you're crazy enouth to try) +### Standard library (full version if you're crazy enough to try) doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex sed -e 's/Library.coqdoc/FullLibrary.coqdoc/g;s/\\begin{document}/\\newcommand{\\textlambda}{\\ensuremath{\\lambda}}\\newcommand{\\textPi}{\\ensuremath{\\Pi}}\\begin{document}/' $< > $@ diff --git a/Makefile.dune b/Makefile.dune index ebf74978a9..88055d62dc 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -5,7 +5,7 @@ .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html stdlib-html apidoc # Documentation targets -.PHONY: test-suite release # Accesory targets +.PHONY: test-suite release # Accessory targets .PHONY: ocheck trunk ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build diff --git a/Makefile.ide b/Makefile.ide index 4cec7aa443..89c1f246db 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -77,7 +77,7 @@ ADWAITASHARE=$(shell ls -d /usr/local/Cellar/adwaita-icon-theme/*)/share .PHONY: coqide coqide-opt coqide-byte coqide-bindings coqide-files coqide-binaries .PHONY: ide-toploop ide-byteloop ide-optloop -# target to build CoqIde (native version) and the stuff needed to lauch it +# target to build CoqIde (native version) and the stuff needed to launch it coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) $(TOPBIN) # target to build CoqIde (in native and byte versions), and no more diff --git a/checker/include b/checker/include index 3ffc301724..411321cb3e 100644 --- a/checker/include +++ b/checker/include @@ -3,7 +3,7 @@ (* Caml script to include for debugging the checker. Usage: from the checker/ directory launch ocaml toplevel and then type #use"include";; - This command loads the relevent modules, defines some pretty + This command loads the relevant modules, defines some pretty printers, and provides functions to interactively check modules (mainly run_l and norec). *) diff --git a/clib/iStream.mli b/clib/iStream.mli index 40d579be60..e56f066c5e 100644 --- a/clib/iStream.mli +++ b/clib/iStream.mli @@ -31,7 +31,7 @@ val cons : 'a -> 'a t -> 'a t (** Append an element in front of a stream. *) val thunk : (unit -> ('a,'a t) u) -> 'a t -(** Internalize the lazyness of a stream. *) +(** Internalize the laziness of a stream. *) val make : ('a -> ('b, 'a) u) -> 'a -> 'b t (** Coiteration constructor. *) diff --git a/configure.ml b/configure.ml index 57f31fec4c..3ced82718e 100644 --- a/configure.ml +++ b/configure.ml @@ -451,7 +451,7 @@ let coq_profile_flag = if !prefs.profile then "-p" else "" let coq_annot_flag = if !prefs.annot then "-annot" else "" let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else "" -(* This variable can be overriden only for debug purposes, use with +(* This variable can be overridden only for debug purposes, use with care. *) let coq_safe_string = "-safe-string" let coq_strict_sequence = "-strict-sequence" diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 26e1e25fb9..42fe13e4eb 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -499,7 +499,7 @@ let print_rules fmt (name, rules) = let pr fmt l = print_list fmt (fun fmt r -> fprintf fmt "(%a)" GramExt.print_extrule r) l in match rules with | [([SymbEntry (e, None)], [Some s], { code = c } )] when String.trim c = s -> - (* This is a horrible hack to work aroud limitations of camlp5 regarding + (* This is a horrible hack to work around limitations of camlp5 regarding factorization of parsing rules. It allows to recognize rules of the form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and reuse the same entry directly. *) diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index c3f3a97ff5..7c8f73c7e4 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -285,9 +285,9 @@ SET RESULT_INSTALLDIR_WFMT=%DESTCOQ% SET TARGET_ARCH=%ARCH%-w64-mingw32
SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
-REM Convert pathes to various formats
+REM Convert paths to various formats
REM WFMT = windows format (C:\..) Used in this batch file.
-REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH variable, which is : separated, so C: doesn't work.
REM MFMT = MinGW format (C:/...) Used for the build, because \\ requires escaping. Mingw can handle \ and /.
SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
@@ -429,13 +429,13 @@ ECHO ========== BATCH FUNCTIONS ========== REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
- ECHO ^<absoloute = install coq in -destcoq absulute path^>
+ ECHO ^<absolute = install coq in -destcoq absolute path^>
ECHO ^<relocatable = install relocatable coq in -destcoq path^>
ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
ECHO -ocaml ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
ECHO -make ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
ECHO -destcyg ^<path to cygwin destination folder^>
- ECHO -destcoq ^<path to coq destination folder (mode=absoloute/relocatable)^>
+ ECHO -destcoq ^<path to coq destination folder (mode=absolute/relocatable)^>
ECHO -setup ^<cygwin setup program name^> (auto adjusted to -arch)
ECHO -proxy ^<internet proxy^>
ECHO -cygrepo ^<cygwin download repository^>
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index a392115ea4..55b46c616c 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -43,7 +43,7 @@ paths like "C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys DLL. The missing piece is a posix shell running on plain Windows (without msys or -Cygwin DLL) and not beeing a binary from obscure sources. I am working on it ... +Cygwin DLL) and not being a binary from obscure sources. I am working on it ... Since compiling gcc and binutils takes a while and it is not of much use without a shell, the building of these components is currently disabled. OCaml is built @@ -274,11 +274,11 @@ Default value: N ===== -cygquiet ===== -Control if the Cygwin setup runs quitely or interactive. +Control if the Cygwin setup runs quietly or interactive. Possible values: -Y: Install Cygwin quitely without user interaction. +Y: Install Cygwin quietly without user interaction. N: Install Cygwin interactively (allows to select additional packages). @@ -344,12 +344,12 @@ selecting more packages) ==================== TODO ==================== - Check for spaces in destination paths -- Check for = signs in all paths (DOS commands don't work with pathes with = in it, possibly even when quoted) +- Check for = signs in all paths (DOS commands don't work with paths with = in it, possibly even when quoted) - Installer doesn't remove OCAMLLIB environment variables (it is in the script, but doesn't seem to work) - CoqIDE doesn't find theme files - Finish / test mingw_in_Cygwin mode (coqide doesn't start, coqc slow cause of scanning complete share folder) -- Possibly create/login as specific user to bash (not sure if it makes sense - nead to create additional bash login link then) -- maybe move share/doc/menhir somehwere else (reduces coqc startup time) +- Possibly create/login as specific user to bash (not sure if it makes sense - need to create additional bash login link then) +- maybe move share/doc/menhir somewhere else (reduces coqc startup time) - Use original installed file list for removing files in uninstaller ==================== Issues with relocation ==================== diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh index 3bba451ec6..543ca972cd 100644 --- a/dev/build/windows/difftar-folder.sh +++ b/dev/build/windows/difftar-folder.sh @@ -40,7 +40,7 @@ fi # Get path prefix if --strip is used if [ "$strip" -gt 0 ] ; then - # Get the path/name of the first file from teh tar and extract the first $strip path components + # Get the path/name of the first file from the tar and extract the first $strip path components # This assumes that the first file in the tar file has at least $strip many path components prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/ else diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d737632638..549f70e8fe 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -765,7 +765,7 @@ function make_ncurses { # gettext make/make install work anyway # # CONFIGURE PARAMETERS - # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW) + # --enable-term-driver --enable-sp-funcs is required for mingw (see README.MinGW) # additional changes # ADD --with-pkg-config # ADD --enable-pc-files @@ -1281,7 +1281,7 @@ function copy_coq_objects { done } -# Copy required GTK config and suport files +# Copy required GTK config and support files function copy_coq_gtk { echo 'gtk-theme-name = "Default"' > "$PREFIX/etc/gtk-3.0/gtkrc" diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c index e4fdcd4d7d..c4c7ec2bff 100755 --- a/dev/build/windows/patches_coq/pkg-config.c +++ b/dev/build/windows/patches_coq/pkg-config.c @@ -1,5 +1,5 @@ // MinGW personality wrapper for pkgconf -// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config +// This is an executable replacement for the shell scripts /bin/ARCH-pkg-config // Compile with e.g. // gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe // gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 98ea594366..408d36df7f 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -31,7 +31,7 @@ PR by running GitLab CI on your private branches. To do so follow these steps: 6. You are encouraged to go to the CI / CD general settings and increase the timeout from 1h to 2h for better reliability. -Now everytime you push (including force-push unless you changed the default +Now every time you push (including force-push unless you changed the default GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and CI will be run. You will receive an e-mail with a report of the failures if there are some. diff --git a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh new file mode 100644 index 0000000000..a89f6aca1b --- /dev/null +++ b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10177" ] || [ "$CI_BRANCH" = "generalize" ]; then + + quickchick_CI_REF=generalize + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + +fi diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh new file mode 100644 index 0000000000..c584438b21 --- /dev/null +++ b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then + + quickchick_CI_REF=instance-no-bang + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index c9eceb1270..66f5a96802 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -92,7 +92,7 @@ When fixes are ready, there are two cases to consider: Once all reviewers approved the PR, the assignee is expected to check that CI completed without relevant failures, and that the PR comes with appropriate documentation and test cases. If not, they should leave a comment on the PR and -put the approriate label. Otherwise, they are expected to merge the PR using the +put the appropriate label. Otherwise, they are expected to merge the PR using the [merge script](../tools/merge-pr.sh). When CI has a few failures which look spurious, restarting the corresponding diff --git a/dev/doc/archive/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex index 0b0811d81b..8b0b14efb8 100644 --- a/dev/doc/archive/naming-conventions.tex +++ b/dev/doc/archive/naming-conventions.tex @@ -570,11 +570,11 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. Zero on domain {\D} & D0 & (notation \verb=0=)\\ One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\ Successor on domain {\D} & Dsucc\\ -Predessor on domain {\D} & Dpred\\ -Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}} +Predecessor on domain {\D} & Dpred\\ +Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existing libraries that already use \texttt{plus} and \texttt{mult}} & (infix notation \verb=+= [50,L])\\ Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\ -Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ +Subtraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\ Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\ Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\ diff --git a/dev/doc/archive/versions-history.tex b/dev/doc/archive/versions-history.tex index 25dabad497..46516dd4e4 100644 --- a/dev/doc/archive/versions-history.tex +++ b/dev/doc/archive/versions-history.tex @@ -372,7 +372,7 @@ Coq V8.4pl5& released 22 October 2014 & \\ Coq V8.4pl6& released 9 April 2015 & \\ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ -&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{asynchronous evaluation} [8-8-2013]\\ && \feature{new proof engine deployed} [2-11-2013]\\ && \feature{universe polymorphism} [6-5-2014]\\ && \feature{primitive projections} [6-5-2014]\\ diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index b0a2b04121..6bbf83aa7e 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -9,13 +9,13 @@ HISTORY: * March 2010 (Pierre Letouzey). Revised build system. In particular, no more stage1,2,3 : - - Stage3 was removed some time ago when coqdep was splitted into + - Stage3 was removed some time ago when coqdep was split into coqdep_boot and full coqdep. - Stage1,2 were replaced by brutal inclusion of all .d at the start of Makefile.build, without trying to guess what could be done at what time. Some initial inclusions hence _fail_, but "make" tries again later and succeed. - - Btw, .ml4 are explicitely turned into .ml files, which stay after build. + - Btw, .ml4 are explicitly turned into .ml files, which stay after build. By default, they are in binary ast format, see READABLE_ML4 option. * February 2014 (Pierre Letouzey). @@ -87,8 +87,8 @@ Cons: clear-text generated .ml. -Makefiles hierachy ------------------- +Makefiles hierarchy +------------------- The Makefile is separated in several files : @@ -101,7 +101,7 @@ The Makefile is separated in several files : FIND_SKIP_DIRS ---------------- +-------------- The recommended style of using FIND_SKIP_DIRS is for example diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 49251d61a1..372e40a0b7 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,14 +108,14 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec dev/dune-dbg +dune exec dev/dune-dbg /path/to/foo.v (ocd) source dune_db ``` or ``` -dune exec dev/dune-dbg checker +dune exec dev/dune-dbg checker Foo (ocd) source dune_db ``` @@ -124,6 +124,8 @@ refined, so you need to build enough of Coq once to use this target [it will then correctly compute the deps and rebuild if you call the script again] This will be fixed in the future. +For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 8cefe699cc..a14781a058 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -18,8 +18,8 @@ See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types * Annotation before commands: +/-/@ a command starting by - is always successful (errors are ignored) -a command starting by + is runned even if option -n is given to make -a command starting by @ is not echoed before being runned +a command starting by + is run even if option -n is given to make +a command starting by @ is not echoed before being run * Custom functions @@ -36,7 +36,7 @@ If the file given to -include doesn't exist, make tries to build it, and even retries again if necessary, but doesn't care if this build finally fails. We used to rely on this "feature", but this should not be the case anymore. We kept "-include" instead of "include" for -avoiding warnings about initially non-existant files. +avoiding warnings about initially non-existent files. Changes (for old-timers) ------------------------ diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7221c3de56..339ac2d9b7 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1278,7 +1278,7 @@ next_global_ident_away true -> next_ident_away_in_goal next_global_ident_away false -> next_global_ident_away ``` -### Cleaning in commmand.ml +### Cleaning in command.ml Functions about starting/ending a lemma are in lemmas.ml Functions about inductive schemes are in indschemes.ml @@ -1593,7 +1593,7 @@ Other kinds of objects: #### Writing subst_thing functions -The subst_thing shoud not copy the thing if it hasn't actually +The subst_thing should not copy the thing if it hasn't actually changed. There are some cool emacs macros in dev/objects.el to help writing subst functions this way quickly and without errors. Also there are *_smartmap functions in Util. diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md index bb17e8fb62..16abf3f519 100644 --- a/dev/doc/econstr.md +++ b/dev/doc/econstr.md @@ -25,7 +25,7 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter Essentially, each time it sees an evar which happens to be defined in the provided evar-map, it replaces it with the corresponding body and carries on. -Due to universe unification occuring at the tactic level, the same goes for +Due to universe unification occurring at the tactic level, the same goes for universe instances and sorts. See the `ESort` and `EInstance` modules in `EConstr`. diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 774552237a..a2c8d2f5ac 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -121,7 +121,7 @@ a limited set of derivation rules), it is recommended to generate proofs as much as possible by refining in ML tactics when it is possible and easy enough. Indeed, this prevents dependence on fragile constructions such as unification. -Obviously, it does not forbid the use of tacticals to mimick what one would do +Obviously, it does not forbid the use of tacticals to mimic what one would do in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple semantics. A list of such tacticals can be found in the `Tacticals` module. Most of them are a porting of the tacticals from the old engine to the new one, so diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 189d6f9fa5..452160ea5a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -113,7 +113,7 @@ - [ ] Upload the new version of the reference manual to the website. *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release - and send annoucement e-mails. + and send announcement e-mails. - [ ] Ping **@Zimmi48** to publish a new version on Zenodo. *TODO: automate this.* - [ ] Close the milestone diff --git a/dev/doc/universes.md b/dev/doc/universes.md index c276603ed2..026c3830a2 100644 --- a/dev/doc/universes.md +++ b/dev/doc/universes.md @@ -163,9 +163,9 @@ only, it's just a matter of using `Evd.fresh_global` / The universe graph ------------------ -To accomodate universe polymorphic definitions, the graph structure in +To accommodate universe polymorphic definitions, the graph structure in kernel/univ.ml was modified. The new API forces every universe to be -declared before it is mentionned in any constraint. This forces to +declared before it is mentioned in any constraint. This forces to declare every universe to be >= Set or > Set. Every universe variable introduced during elaboration is >= Set. Every _global_ universe is now declared explicitly > Set, _after_ typechecking the definition. In diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 48671c03b6..e23d1234f7 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -437,7 +437,7 @@ Searches for objects that satisfy a list of constraints. If `${positiveConstrain * Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. * SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. * In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure. -* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*. +* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is omitted*. ------------------------------- @@ -3,7 +3,7 @@ (public_name coq.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) - (modules :standard) + (modules top_printers) (optional) (libraries coq.toplevel coq.plugins.ltac)) @@ -11,7 +11,7 @@ (targets dune-dbg) (deps dune-dbg.in ../checker/coqchk.bc - ../topbin/coqtop_byte_bin.bc + ../topbin/coqc_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 80ad0500e0..bd0a837938 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,11 +3,14 @@ # Run in a proper install dune env. case $1 in checker) + shift exe=_build/default/checker/coqchk.bc ;; *) - exe=_build/default/topbin/coqtop_byte_bin.bc + exe=_build/default/topbin/coqc_bin.bc ;; esac -ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe +emacs="${INSIDE_EMACS:+-emacs}" + +ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@" diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index d8043558eb..96c92e3162 100755 --- a/dev/lint-commits.sh +++ b/dev/lint-commits.sh @@ -34,6 +34,6 @@ if [ "${#bad[@]}" != 0 ] then >&2 echo "Whitespace errors!" >&2 echo "In commits ${bad[*]}" - >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." + >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." exit 1 fi diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index f48013cf2e..b4c5d3d528 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -6,7 +6,7 @@ ;SetCompress off SetCompressor lzma -; Comment out after debuging. +; Comment out after debugging. ; The VERSION should be passed as an argument at compile time using : ; diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index c6687b9731..b89ae67a82 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -85,6 +85,35 @@ Note that this function is executed before _Coqproject is read if it exists." (setq-local coq-prog-name (concat dir "bin/coqtop"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) +(defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg" + "Command run by `coqdev-ocamldebug'") + +(defun coqdev-ocamldebug () + "Runs a command in an ocamldebug buffer." + (interactive) + (let* ((dir (read-directory-name "Run from directory: " + (coqdev-default-directory))) + (name "ocamldebug-coq") + (buffer-name (concat "*" name "*"))) + (pop-to-buffer buffer-name) + (unless (comint-check-proc buffer-name) + (setq default-directory dir) + (setq coqdev-ocamldebug-command + (read-from-minibuffer "Command to run: " + coqdev-ocamldebug-command)) + (let* ((cmdlist (tuareg--split-args coqdev-ocamldebug-command)) + (cmdlist (mapcar #'substitute-in-file-name cmdlist))) + (apply #'make-comint name + (car cmdlist) + nil + (cdr cmdlist)) + (set-process-filter (get-buffer-process (current-buffer)) + #'ocamldebug-filter) + (set-process-sentinel (get-buffer-process (current-buffer)) + #'ocamldebug-sentinel) + (ocamldebug-mode))) + (ocamldebug-set-buffer))) + ;; This Elisp snippet adds a regexp parser for the format of Anomaly ;; backtraces (coqc -bt ...), to the error parser of the Compilation ;; mode (C-c C-c: "Compile command: ..."). File locations in traces diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex index ae4b569b36..84894b6f7c 100644 --- a/dev/v8-syntax/memo-v8.tex +++ b/dev/v8-syntax/memo-v8.tex @@ -55,7 +55,7 @@ _ are allowed after the first character. Quoted strings are used typically to give a filename (which may not be a regular identifier). As before they are written between double quotes ("). Unlike for V7, there is no escape character: characters -are written normaly but the double quote which is doubled. +are written normally but the double quote which is doubled. \section{Main changes in terms w.r.t. V7} @@ -252,7 +252,7 @@ became \TERM{context}. Syntax is unified with subterm matching. \subsection{Occurrences} -To avoid ambiguity between a numeric literal and the optionnal +To avoid ambiguity between a numeric literal and the optional occurrence numbers of this term, the occurrence numbers are put after the term itself. This applies to tactic \TERM{pattern} and also \TERM{unfold} diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst new file mode 100644 index 0000000000..c69cda9656 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst @@ -0,0 +1,2 @@ +- Remove undocumented :n:`Instance : !@type` syntax + (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/common/styles/html/coqremote/modules/system/system.css b/doc/common/styles/html/coqremote/modules/system/system.css index 9371bb479e..9556c7882a 100644 --- a/doc/common/styles/html/coqremote/modules/system/system.css +++ b/doc/common/styles/html/coqremote/modules/system/system.css @@ -327,7 +327,7 @@ html.js fieldset.collapsed legend a { * html.js fieldset.collapsed table * { display: inline; } -/* For Safari 2 to prevent collapsible fieldsets containing tables from dissapearing due to tableheader.js. */ +/* For Safari 2 to prevent collapsible fieldsets containing tables from disappearing due to tableheader.js. */ html.js fieldset.collapsible { position: relative; } diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg index 82ba45726e..f4d9e7fd5b 100644 --- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -33,7 +33,7 @@ TACTIC EXTEND collapse_hyps END (* More advanced examples, where automatic proof happens but - no tactic is being called explicitely. The first one uses + no tactic is being called explicitly. The first one uses type classes. *) VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY | [ "Tuto3_3" int(n) ] -> { example_classes n } diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 8a895eb515..3dc8707a34 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -168,7 +168,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: .. cmd:: Extraction NoInline {+ @qualid } - Conversely, the constants mentionned by this command will + Conversely, the constants mentioned by this command will never be inlined during extraction. .. cmd:: Print Extraction Inline diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 847abb33fc..68f6d4008a 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -441,7 +441,7 @@ First class setoids and morphisms The implementation is based on a first-class representation of properties of relations and morphisms as typeclasses. That is, the various combinations of properties on relations and morphisms are -represented as records and instances of theses classes are put in a +represented as records and instances of these classes are put in a hint database. For example, the declaration: .. coqdoc:: diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 22ddcae584..45c74ab02a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -299,9 +299,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation num {? of @ident} +.. cmd:: Obligation @num {? of @ident} - Start the proof of obligation num. + Start the proof of obligation :token:`num`. .. cmd:: Next Obligation {? of @ident} diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 65934efaa6..2ba13db042 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -385,7 +385,7 @@ few other commands related to typeclasses. .. note:: As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully - mimicks what happens during typeclass resolution when it is called + mimics what happens during typeclass resolution when it is called during refinement/type inference, except that *only* declared class subgoals are considered at the start of resolution during type inference, while ``all`` can select non-class subgoals as well. It might diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 6b10b7c0b3..1aa2111816 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -449,7 +449,7 @@ underscore or by omitting the annotation to a polymorphic definition. This option, on by default, removes universes which appear only in the body of an opaque polymorphic definition from the definition's universe arguments. As such, no value needs to be provided for - these universes when instanciating the definition. Universe + these universes when instantiating the definition. Universe constraints are automatically adjusted. Consider the following definition: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index cc2c43e7dd..db4ebd5e38 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -186,7 +186,7 @@ Coq is now continuously tested against OCaml trunk, in addition to the oldest supported and latest OCaml releases. Coq's documentation for the development branch is now deployed -continously at https://coq.github.io/doc/master/api (documentation of +continuously at https://coq.github.io/doc/master/api (documentation of the ML API), https://coq.github.io/doc/master/refman (reference manual), and https://coq.github.io/doc/master/stdlib (documentation of the standard library). Similar links exist for the `v8.10` branch. @@ -656,8 +656,8 @@ changes: attribute. - Removed deprecated commands ``Arguments Scope`` and ``Implicit - Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper - Hugunin. + Arguments`` in favor of :cmd:`Arguments (scopes)` and + :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin. - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to avoid repeating uniform parameters in constructor declarations. @@ -665,7 +665,7 @@ changes: - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by Matthieu Sozeau, for controlling the opacity status of variables and constants in hint databases. It is recommended to always use these - commands after creating a hint databse with :cmd:`Create HintDb`. + commands after creating a hint database with :cmd:`Create HintDb`. - Multiple sections with the same name are now allowed, by Jasper Hugunin. @@ -892,7 +892,7 @@ Vernacular Commands `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting globally the opacity flag of variables and constants in hint databases, - overwritting the opacity set of the hint database. + overwriting the opacity set of the hint database. - Added generic syntax for "attributes", as in: `#[local] Lemma foo : bar.` - Added the `Numeral Notation` command for registering decimal numeral @@ -1129,7 +1129,7 @@ Tactics few rare incompatibilities (it was unintendedly recursively rewriting in the side conditions generated by H). - Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure - properties of the executation of a tactic without keeping the effect + properties of the execution of a tactic without keeping the effect of the execution. - `vm_compute` now supports existential variables. - Calls to `shelve` and `give_up` within calls to tactic `refine` now working. @@ -1262,7 +1262,7 @@ Tools Tactic language - The undocumented "nameless" forms `fix N`, `cofix` have been - deprecated; please use `fix ident N /cofix ident` to explicitely + deprecated; please use `fix ident N /cofix ident` to explicitly name the (co)fixpoint hypothesis to be introduced. Documentation @@ -2953,7 +2953,7 @@ Other bugfixes - Fix incorrect behavior of CS resolution - #4591: Uncaught exception in directory browsing. - CoqIDE is more resilient to initialization errors. -- #4614: "Fully check the document" is uninterruptable. +- #4614: "Fully check the document" is uninterruptible. - Try eta-expansion of records only on non-recursive ones - Fix bug when a sort is ascribed to a Record - Primitive projections: protect kernel from erroneous definitions. @@ -3442,7 +3442,7 @@ Libraries * all functions over type Z : Z.add, Z.mul, ... * the minimal proofs of specifications for these functions : Z.add_0_l, ... - * an instantation of all derived properties proved generically in Numbers : + * an instantiation of all derived properties proved generically in Numbers : Z.add_comm, Z.add_assoc, ... A large part of ZArith is now simply compatibility notations, for instance @@ -4623,7 +4623,7 @@ Setoid rewriting + Setoid_Theory is now an alias to Equivalence, scripts building objects of type Setoid_Theory need to unfold (or "red") the definitions of Reflexive, Symmetric and Transitive in order to get the same goals - as before. Scripts which introduced variables explicitely will not break. + as before. Scripts which introduced variables explicitly will not break. + The order of subgoals when doing [setoid_rewrite] with side-conditions is always the same: first the new goal, then the conditions. @@ -5022,7 +5022,7 @@ Syntax Language and commands -- Added sort-polymorphism for definitions in Type (but finally abandonned). +- Added sort-polymorphism for definitions in Type (but finally abandoned). - Support for implicit arguments in the types of parameters in (co-)fixpoints and (co-)inductive declarations. - Improved type inference: use as much of possible general information. @@ -5251,7 +5251,7 @@ Library - New file about the factorial function in Arith -- An additional elimination Acc_iter for Acc, simplier than Acc_rect. +- An additional elimination Acc_iter for Acc, simpler than Acc_rect. This new elimination principle is used for definition well_founded_induction. - New library NArith on binary natural numbers @@ -5336,7 +5336,7 @@ Bugs Miscellaneous - Implicit parameters of inductive types definition now taken into - account for infering other implicit arguments + account for inferring other implicit arguments Incompatibilities @@ -5417,7 +5417,7 @@ Gallina Known problems of the automatic translation - iso-latin-1 characters are no longer supported: move your files to - 7-bits ASCII or unicode before translation (swith to unicode is + 7-bits ASCII or unicode before translation (switch to unicode is automatically done if a file is loaded and saved again by coqide) - Renaming in ZArith: incompatibilities in Coq user contribs due to merging names INZ, from Reals, and inject_nat. @@ -5442,7 +5442,7 @@ Vernacular commands - "Functional Scheme" and "Functional Induction" extended to polymorphic types and dependent types - Notation now allows recursive patterns, hence recovering parts of the - fonctionalities of pre-V8 Grammar/Syntax commands + functionalities of pre-V8 Grammar/Syntax commands - Command "Print." discontinued. - Redundant syntax "Implicit Arguments On/Off" discontinued diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index 0f5b991ba4..c4a48d6985 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -110,7 +110,7 @@ advantage of special hardware, debuggers, and the like. We hope that |Coq| can be of use to researchers interested in experimenting with this new methodology. -.. [#years] At the time of writting, i.e. 1995. +.. [#years] At the time of writing, i.e. 1995. Versions 1 to 5 --------------- @@ -305,7 +305,7 @@ Michel Mauny, Ascander Suarez and Pierre Weis. V3.1 was started in the summer of 1986, V3.2 was frozen at the end of November 1986. V3.4 was developed in the first half of 1987. -Thierry Coquand held a post-doctoral position in Cambrige University +Thierry Coquand held a post-doctoral position in Cambridge University in 1986-87, where he developed a variant implementation in SML, with which he wrote some developments on fixpoints in Scott's domains. @@ -345,7 +345,7 @@ lemmas when local hypotheses of proofs were discharged. This gave a notion of global mathematical environment with local sections. Another significant practical change was that the system, originally -developped on the VAX central computer of our lab, was transferred on +developed on the VAX central computer of our lab, was transferred on SUN personal workstations, allowing a level of distributed development. The extraction algorithm was modified, with three annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop`` @@ -503,7 +503,7 @@ of CNRS-ENS Lyon. Chetan Murthy joined the team in 1991 and became the main software architect of Version 5. He completely rehauled the implementation for efficiency. Versions 5.6 and 5.8 were major distributed versions, -with complete documentation and a library of users' developements. The +with complete documentation and a library of users' developments. The use of the RCS revision control system, and systematic ChangeLog files, allow a more precise tracking of the software developments. @@ -1330,7 +1330,7 @@ Language - Inductive definitions now accept ">" in constructor types to declare the corresponding constructor as a coercion. -- Idem for assumptions declarations and constants when the type is mentionned. +- Idem for assumptions declarations and constants when the type is mentioned. - The "Coercion" and "Canonical Structure" keywords now accept the same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t". - Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u". @@ -1383,7 +1383,7 @@ Tactics it can also recognize 'False' in the hypothesis and use it to solve the goal. - Coercions now handled in "with" bindings -- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses +- "Subst x" replaces all occurrences of x by t in the goal and hypotheses when an hypothesis x=t or x:=t or t=x exists - Fresh names for Assert and Pose now based on collision-avoiding Intro naming strategy (exceptional source of incompatibilities) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 5e214f6f7f..2b673ff62b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1662,6 +1662,7 @@ Declaring Implicit Arguments of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits + :name: Arguments (clear implicits) This command clears implicit arguments. @@ -1738,6 +1739,7 @@ Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Arguments @qualid : default implicits + :name: Arguments (default implicits) This command tells |Coq| to automatically detect what are the implicit arguments of a defined object. @@ -1908,6 +1910,7 @@ Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Arguments @qualid {* @name} : @rename + :name: Arguments (rename) This command is used to redefine the names of implicit arguments. @@ -2131,24 +2134,71 @@ Implicit generalization .. index:: `{ } .. index:: `( ) +.. index:: `{! } +.. index:: `(! ) Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are -quantified explicitly. Implicit generalization is done inside binders -starting with a \` and terms delimited by \`{ } and \`( ), always -introducing maximally inserted implicit arguments for the generalized -variables. Inside implicit generalization delimiters, free variables -in the current context are automatically quantified using a product or -a lambda abstraction to generate a closed term. In the following -statement for example, the variables n and m are automatically -generalized and become explicit arguments of the lemma as we are using -\`( ): +quantified explicitly. -.. coqtop:: all +It is activated for a binder by prefixing a \`, and for terms by +surrounding it with \`{ } or \`( ). + +Terms surrounded by \`{ } introduce their free variables as maximally +inserted implicit arguments, and terms surrounded by \`( ) introduce +them as explicit arguments. + +Generalizing binders always introduce their free variables as +maximally inserted implicit arguments. The binder itself introduces +its argument as usual. + +In the following statement, ``A`` and ``y`` are automatically +generalized, ``A`` is implicit and ``x``, ``y`` and the anonymous +equality argument are explicit. + +.. coqtop:: all reset Generalizable All Variables. - Lemma nat_comm : `(n = n + 0). + Definition sym `(x:A) : `(x = y -> y = x) := fun _ p => eq_sym p. + + Print sym. + +Dually to normal binders, the name is optional but the type is required: + +.. coqtop:: all + + Check (forall `{x = y :> A}, y = x). + +When generalizing a binder whose type is a typeclass, its own class +arguments are omitted from the syntax and are generalized using +automatic names, without instance search. Other arguments are also +generalized unless provided. This produces a fully general statement. +this behaviour may be disabled by prefixing the type with a ``!`` or +by forcing the typeclass name to be an explicit application using +``@`` (however the later ignores implicit argument information). + +.. coqtop:: all + + Class Op (A:Type) := op : A -> A -> A. + + Class Commutative (A:Type) `(Op A) := commutative : forall x y, op x y = op y x. + Instance nat_op : Op nat := plus. + + Set Printing Implicit. + Check (forall `{Commutative }, True). + Check (forall `{Commutative nat}, True). + Fail Check (forall `{Commutative nat _}, True). + Fail Check (forall `{!Commutative nat}, True). + Arguments Commutative _ {_}. + Check (forall `{!Commutative nat}, True). + Check (forall `{@Commutative nat plus}, True). + +Multiple binders can be merged using ``,`` as a separator: + +.. coqtop:: all + + Check (forall `{Commutative A, Hnat : !Commutative nat}, True). One can control the set of generalizable identifiers with the ``Generalizable`` vernacular command to avoid unexpected @@ -2176,22 +2226,6 @@ that specify which variables should be generalizable. Allows exporting the choice of generalizable variables. -One can also use implicit generalization for binders, in which case -the generalized variables are added as binders and set maximally -implicit. - -.. coqtop:: all - - Definition id `(x : A) : A := x. - - Print id. - -The generalizing binders \`{ } and \`( ) work similarly to their -explicit counterparts, only binding the generalized variables -implicitly, as maximally-inserted arguments. In these binders, the -binding name for the bound object is optional, whereas the type is -mandatory, dually to regular binders. - .. _Coercions: Coercions diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index bbd7e0ba3d..0a95a6edd6 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -121,6 +121,7 @@ mode but it can also be used in toplevel definitions as shown below. : solve [ `expr` | ... | `expr` ] : idtac [ `message_token` ... `message_token`] : fail [`natural`] [`message_token` ... `message_token`] + : gfail [`natural`] [`message_token` ... `message_token`] : fresh [ `component` … `component` ] : context `ident` [`term`] : eval `redexpr` in `term` @@ -582,11 +583,11 @@ Failing the call to :n:`fail @num` is not enclosed in a :n:`+` command, respecting the algebraic identity. - .. tacv:: fail {* message_token} + .. tacv:: fail {* @message_token} The given tokens are used for printing the failure message. - .. tacv:: fail @num {* message_token} + .. tacv:: fail @num {* @message_token} This is a combination of the previous variants. @@ -597,8 +598,8 @@ Failing Similarly, ``gfail`` fails even when used after ``all:`` and there are no goals left. See the example for clarification. - .. tacv:: gfail {* message_token} - gfail @num {* message_token} + .. tacv:: gfail {* @message_token} + gfail @num {* @message_token} These variants fail with an error message or an error level even if there are no goals left. Be careful however if Coq terms have to be @@ -708,7 +709,7 @@ tactic for printing. By copying the definition of :tacn:`time_constr` from the standard library, - users can achive support for a fixed pattern of nesting by passing + users can achieve support for a fixed pattern of nesting by passing different :token:`string` parameters to :tacn:`restart_timer` and :tacn:`finish_timing` at each level of nesting. @@ -964,7 +965,7 @@ system decide a name with the intro tactic is not so good since it is very awkward to retrieve the name the system gave. The following expression returns an identifier: -.. tacn:: fresh {* component} +.. tacn:: fresh {* @component} It evaluates to an identifier unbound in the goal. This fresh identifier is obtained by concatenating the value of the :n:`@component`\ s (each of them @@ -1676,7 +1677,7 @@ It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in |Ltac| and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The -reasons for the performence degradation can be intricate, like a slowly +reasons for the performance degradation can be intricate, like a slowly performing |Ltac| match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending on its calling context. Thus diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 75e019592f..45c40ee787 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -853,7 +853,7 @@ An *occurrence switch* can be: algorithm in a local definition, instead of copying large terms by hand. -It is important to remember that matching *preceeds* occurrence +It is important to remember that matching *precedes* occurrence selection. .. example:: @@ -1499,7 +1499,7 @@ side of an equation. The abstract tactic ``````````````````` -.. tacn:: abstract: {+ d_item} +.. tacn:: abstract: {+ @d_item} :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the @@ -2455,7 +2455,7 @@ the holes are abstracted in term. Lemma test : True. have: _ * 0 = 0. - The invokation of ``have`` is equivalent to: + The invocation of ``have`` is equivalent to: .. coqtop:: reset none @@ -4927,7 +4927,7 @@ bookkeeping steps. apply/PQequiv. thus in this case, the tactic ``apply/PQequiv`` is equivalent to - ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is tha analogue of + ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is the analogue of ``iffRL`` for the converse implication. Any |SSR| term whose type coerces to a double implication can be diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4e47621938..cdd23f4d06 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2703,33 +2703,33 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left - .. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in @goal_occurrences Analogous to :n:`rewrite @term` but rewriting is done following clause (similarly to :ref:`performing computations <performingcomputations>`). For instance: - + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis - `H`:sub:`1` instead of the current goal. - + :n:`rewrite H in H`:sub:`1` :g:`at 1, H`:sub:`2` :g:`at - 2 |- *` means - :n:`rewrite H; rewrite H in H`:sub:`1` :g:`at 1; rewrite H in H`:sub:`2` :g:`at - 2.` + + :n:`rewrite H in H'` will rewrite `H` in the hypothesis + ``H'`` instead of the current goal. + + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means + :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` In particular a failure will happen if any of these three simpler tactics fails. - + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses - :g:`H`:sub:`i` different from :g:`H`. + + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses + :g:`H'` different from :g:`H`. A success will happen as soon as at least one of these simpler tactics succeeds. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. - .. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at @occurrences Rewrite only the given occurrences of :token:`term`. Occurrences are specified from left to right as for pattern (:tacn:`pattern`). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to ``Import Setoid`` to use this variant. - .. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by @tactic Use tactic to completely solve the side-conditions arising from the :tacn:`rewrite`. @@ -2799,13 +2799,14 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has the form :n:`@term’ = @term` - .. tacv:: replace @term {? with @term} in clause {? by @tactic} - replace -> @term in clause - replace <- @term in clause + .. tacv:: replace @term {? with @term} in @goal_occurences {? by @tactic} + replace -> @term in @goal_occurences + replace <- @term in @goal_occurences - Acts as before but the replacements take place in the specified clause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any ``type of`` nor ``value of``. + Acts as before but the replacements take place in the specified clauses + (:token:`goal_occurences`) (see :ref:`performingcomputations`) and not + only in the conclusion of the goal. The clause argument must not contain + any ``type of`` nor ``value of``. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite @@ -2893,7 +2894,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - .. tacv:: stepr @term stepr @term by tactic + .. tacv:: stepr @term by @tactic :name: stepr This behaves as :tacn:`stepl` but on the right-hand-side of the binary @@ -3159,7 +3160,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command. .. example:: @@ -3299,12 +3300,13 @@ the conversion in hypotheses :n:`{+ @ident}`. an expression defining a notation (e.g. `"_ + _"`), and this notation refers to an unfoldable constant, then the tactic unfolds it. -.. tacv:: unfold @string%key +.. tacv:: unfold @string%@ident This is variant of :n:`unfold @string` where :n:`@string` gets its - interpretation from the scope bound to the delimiting key :n:`key` + interpretation from the scope bound to the delimiting key :token:`ident` instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`). -.. tacv:: unfold {+, qualid_or_string at {+, @num}} + +.. tacv:: unfold {+, @qualid_or_string at {+, @num}} This is the most general form, where :n:`qualid_or_string` is either a :n:`@qualid` or a :n:`@string` referring to a notation. @@ -3382,14 +3384,13 @@ the conversion in hypotheses :n:`{+ @ident}`. Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: conv_tactic in {+, @ident} +.. tacn:: @tactic in {+, @ident} - Applies the conversion tactic :n:`conv_tactic` to the hypotheses - :n:`{+ @ident}`. The tactic :n:`conv_tactic` is any of the conversion tactics - listed in this section. + Applies :token:`tactic` (any of the conversion tactics listed in this + section) to the hypotheses :n:`{+ @ident}`. - If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by - (type of :n:`@ident`) to address not the body but the type of the local + If :token:`ident` is a local definition, then :token:`ident` can be replaced by + :n:`type of @ident` to address not the body but the type of the local definition. Example: :n:`unfold not in (type of H1) (type of H3)`. @@ -3550,9 +3551,9 @@ Automation This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in clause +.. tacv:: autounfold with {+ @ident} in @goal_occurences - Performs the unfolding in the given clause. + Performs the unfolding in the given clause (:token:`goal_occurences`). .. tacv:: autounfold with * @@ -3714,7 +3715,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint Resolve -> @term : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentionned + the hint will be used as :n:`apply <- @term`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). @@ -3783,7 +3784,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is This sets the transparency flag used during unification of hints in the database for all constants or all variables, - overwritting the existing settings of opacity. It is advised + overwriting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident @@ -3981,7 +3982,7 @@ use one or several databases specific to your development. Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in the bases :n:`{+ @ident}`. -.. cmd:: Hint Rewrite {+ @term} using tactic : {+ @ident} +.. cmd:: Hint Rewrite {+ @term} using @tactic : {+ @ident} When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the tactic ``tactic`` will be applied to the generated subgoals, the main subgoal @@ -4202,7 +4203,7 @@ some incompatibilities. Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search environment. -.. tacv:: firstorder tactic using {+ @qualid} with {+ @ident} +.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident} This combines the effects of the different variants of :tacn:`firstorder`. @@ -4243,10 +4244,10 @@ some incompatibilities. congruence. Qed. -.. tacv:: congruence n +.. tacv:: congruence @num - Tries to add at most `n` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of `n` does not make + Tries to add at most :token:`num` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`num` does not make success slower, only failure. You might consider adding some lemmas as hypotheses using assert in order for :tacn:`congruence` to use them. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 26dc4e02cf..ffa727ff6c 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -264,11 +264,11 @@ Requests to the environment main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`. - .. cmdv:: Search @string%@key + .. cmdv:: Search @string%@ident The string string must be a notation or the main symbol of a notation which is then interpreted in the scope bound to - the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`). + the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`). .. cmdv:: Search @term_pattern @@ -1208,7 +1208,7 @@ Controlling the locality of commands effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and the Global modifier is not applicable to them. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index cda228a7da..3710c0af9d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1032,11 +1032,11 @@ Local opening of an interpretation scope +++++++++++++++++++++++++++++++++++++++++ It is possible to locally extend the interpretation scope stack using the syntax -:g:`(term)%key` (or simply :g:`term%key` for atomic terms), where key is a +:n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a special identifier called *delimiting key* and bound to a given scope. In such a situation, the term term, and all its subterms, are -interpreted in the scope stack extended with the scope bound tokey. +interpreted in the scope stack extended with the scope bound to :token:`ident`. .. cmd:: Delimit Scope @scope with @ident @@ -1051,15 +1051,15 @@ interpreted in the scope stack extended with the scope bound tokey. Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ -.. cmd:: Arguments @qualid {+ @name%@scope} +.. cmd:: Arguments @qualid {+ @name%@ident} :name: Arguments (scopes) It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is - :n:`Arguments @qualid {+ @name%@scope}` where the list is a prefix of the - arguments of ``qualid`` eventually annotated with their ``scope``. Grouping + :n:`Arguments @qualid {+ @name%@ident}` where the list is a prefix of the + arguments of ``qualid`` optionally annotated with their scope :token:`ident`. Grouping round parentheses can be used to decorate multiple arguments with the same - scope. ``scope`` can be either a scope name or its delimiting key. For + scope. :token:`ident` can be either a scope name or its delimiting key. For example the following command puts the first two arguments of :g:`plus_fct` in the scope delimited by the key ``F`` (``Rfun_scope``) and the last argument in the scope delimited by the key ``R`` (``R_scope``). @@ -1070,13 +1070,13 @@ Binding arguments of a constant to an interpretation scope The ``Arguments`` command accepts scopes decoration to all grouping parentheses. In the following example arguments A and B are marked as - maximally inserted implicit arguments and are put into the type_scope scope. + maximally inserted implicit arguments and are put into the ``type_scope`` scope. .. coqdoc:: Arguments respectful {A B}%type (R R')%signature _ _. - When interpreting a term, if some of the arguments of qualid are built + When interpreting a term, if some of the arguments of :token:`qualid` are built from a notation, then this notation is interpreted in the scope stack extended by the scope bound (if any) to this argument. The effect of the scope is limited to the argument itself. It does not propagate to @@ -1088,21 +1088,21 @@ Binding arguments of a constant to an interpretation scope This command can be used to clear argument scopes of :token:`qualid`. - .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes + .. cmdv:: Arguments @qualid {+ @name%@ident} : extra scopes Defines extra argument scopes, to be used in case of coercion to ``Funclass`` (see the :ref:`implicitcoercions` chapter) or with a computed type. - .. cmdv:: Global Arguments @qualid {+ @name%@scope} + .. cmdv:: Global Arguments @qualid {+ @name%@ident} - This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a + This behaves like :n:`Arguments qualid {+ @name%@ident}` but survives when a section is closed instead of stopping working at section closing. Without the ``Global`` modifier, the effect of the command stops when the section it belongs to ends. - .. cmdv:: Local Arguments @qualid {+ @name%@scope} + .. cmdv:: Local Arguments @qualid {+ @name%@ident} - This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not + This behaves like :n:`Arguments @qualid {+ @name%@ident}` but does not survive modules and files. Without the ``Local`` modifier, the effect of the command is visible from within other modules or files. @@ -1143,8 +1143,8 @@ Binding types of arguments to an interpretation scope scope of operations on the natural numbers), it may be convenient to bind it to this type. When a scope ``scope`` is bound to a type ``type``, any new function defined later on gets its arguments of type ``type`` interpreted by default in - scope scope (this default behavior can however be overwritten by explicitly - using the command :cmd:`Arguments`). + scope ``scope`` (this default behavior can however be overwritten by explicitly + using the command :cmd:`Arguments <Arguments (scopes)>`). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type @@ -1198,7 +1198,7 @@ The ``function_scope`` interpretation scope The scope ``function_scope`` also has a special status. It is temporarily activated each time the argument of a global reference is -recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or +recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or :g:`A -> B`. diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index d8ac640f2a..dde8a7b838 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -412,7 +412,7 @@ but its behaviour is not to fold the abbreviation at all.}. {\tt LetTac} could be followed by a specification (called a clause) of the places where the abbreviation had to be folded (hypothese and/or conclusion). Clauses are the syntactic notion to denote in which parts -of a goal a given transformation shold occur. Its basic notation is +of a goal a given transformation should occur. Its basic notation is either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |- \textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all the hypotheses), or a comma-separated list of either hypothesis name, @@ -620,7 +620,7 @@ These constraints are met by the makefiles produced by {\tt coq\_makefile} Otherwise, modify your build program so as to pass option {\tt -translate} to program {\tt coqc}. The effect of this option is to -ouptut the translated source of any {\tt .v} file in a file with +output the translated source of any {\tt .v} file in a file with extension {\tt .v8} located in the same directory than the original file. @@ -675,7 +675,7 @@ solve all occurrences of the problem. The definition of identifiers changed. Most of those changes are handled by the translator. They include: \begin{itemize} -\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt +\item {\tt \_} is not an identifier anymore: it is translated to {\tt x\_} \item avoid clash with new keywords by adding a trailing {\tt \_} \end{itemize} diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 1de9890992..ba58ff0084 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -52,7 +52,7 @@ def is_whitespace_string(elem): return isinstance(elem, NavigableString) and elem.strip() == "" def strip_soup(soup, pred): - """Strip elements maching pred from front and tail of soup.""" + """Strip elements matching pred from front and tail of soup.""" while soup.contents and pred(soup.contents[-1]): soup.contents.pop() diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 26f6255069..2b124ee5c1 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -47,7 +47,7 @@ class CoqTop: :param coqtop_bin: The path to coqtop; uses $COQBIN by default, falling back to "coqtop" :param color: When True, tell coqtop to produce ANSI color codes (see the ansicolors module) - :param args: Additional arugments to coqtop. + :param args: Additional arguments to coqtop. """ self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): @@ -68,7 +68,7 @@ class CoqTop: self.coqtop.kill(9) def next_prompt(self): - """Wait for the next coqtop prompt, and return the output preceeding it.""" + """Wait for the next coqtop prompt, and return the output preceding it.""" self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10) return self.coqtop.before diff --git a/doc/whodidwhat/whodidwhat-8.2update.tex b/doc/whodidwhat/whodidwhat-8.2update.tex index 4f4f0e952e..f45e6564f2 100644 --- a/doc/whodidwhat/whodidwhat-8.2update.tex +++ b/doc/whodidwhat/whodidwhat-8.2update.tex @@ -181,7 +181,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin, Yves Bertot -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/doc/whodidwhat/whodidwhat-8.3update.tex b/doc/whodidwhat/whodidwhat-8.3update.tex index 0a07378169..7cce0083d5 100644 --- a/doc/whodidwhat/whodidwhat-8.3update.tex +++ b/doc/whodidwhat/whodidwhat-8.3update.tex @@ -188,7 +188,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex index bb4c5ce469..2d74a653ed 100644 --- a/doc/whodidwhat/whodidwhat-8.4update.tex +++ b/doc/whodidwhat/whodidwhat-8.4update.tex @@ -191,7 +191,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex index ce099dc363..600ecf93db 100644 --- a/doc/whodidwhat/whodidwhat-8.5update.tex +++ b/doc/whodidwhat/whodidwhat-8.5update.tex @@ -197,7 +197,7 @@ \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech -\item Whelp suppport: Hugo Herbelin +\item Whelp support: Hugo Herbelin \end{itemize} \section{Parsing and printing} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 0a5bba39b9..7c2ecca89e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -860,7 +860,7 @@ let compare_constructor_instances evd u u' = [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8eaff8bd13..907be8eba2 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -208,7 +208,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns diff --git a/engine/ftactic.ml b/engine/ftactic.ml index dab2e7d5ef..b59d04e813 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -18,8 +18,8 @@ type 'a focus = (** Type of tactics potentially goal-dependent. If it contains a [Depends], then the length of the inner list is guaranteed to be the number of - currently focussed goals. Otherwise it means the tactic does not depend - on the current set of focussed goals. *) + currently focused goals. Otherwise it means the tactic does not depend + on the current set of focused goals. *) type 'a t = 'a focus Proofview.tactic let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index ed95d62bc6..5922781d4d 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -18,7 +18,7 @@ type +'a t = 'a focus Proofview.tactic (** The type of focussing tactics. A focussing tactic is like a normal tactic, except that it is able to remember it have entered a goal. Whenever this is the case, each subsequent effect of the tactic is dispatched on the - focussed goals. This is a monad. *) + focused goals. This is a monad. *) (** {5 Monadic interface} *) @@ -32,20 +32,20 @@ val bind : 'a t -> ('a -> 'b t) -> 'b t val lift : 'a Proofview.tactic -> 'a t (** Transform a tactic into a focussing tactic. The resulting tactic is not - focussed. *) + focused. *) val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** Given a continuation producing a tactic, evaluates the focussing tactic. If - the tactic has not focussed, then the continuation is evaluated once. - Otherwise it is called in each of the currently focussed goals. *) + the tactic has not focused, then the continuation is evaluated once. + Otherwise it is called in each of the currently focused goals. *) (** {5 Focussing} *) -(** Enter a goal. The resulting tactic is focussed. *) +(** Enter a goal. The resulting tactic is focused. *) val enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is - focussed. *) + focused. *) val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index e0c24f049f..a504ee28e2 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -151,7 +151,7 @@ struct (** Double-continuation backtracking monads are reasonable folklore for "search" implementations (including the Tac interactive prover's tactics). Yet it's quite hard to wrap your head around - these. I recommand reading a few times the "Backtracking, + these. I recommend reading a few times the "Backtracking, Interleaving, and Terminating Monad Transformers" paper by O. Kiselyov, C. Shan, D. Friedman, and A. Sabry. The peculiar shape of the monadic type is reminiscent of that of the diff --git a/engine/proofview.ml b/engine/proofview.ml index 5c5a02d3fa..c00c90e5e9 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -31,7 +31,7 @@ type entry = (EConstr.constr * EConstr.types) list ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) let proofview p = @@ -114,7 +114,7 @@ type focus_context = goal_with_state list * goal_with_state list instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) let focus_context (left,right) = @@ -123,7 +123,7 @@ let focus_context (left,right) = (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the - original list. The focused list has lenght [j-i-1] and contains + original list. The focused list has length [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises [IndexOutOfRange] if [i > length l], or [j > length l] or [j < @@ -245,7 +245,7 @@ let tclUNIT = Proof.return (** Bind operation of the tactic monad. *) let tclBIND = Proof.(>>=) -(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation, +(** Interprets the ";" (semicolon) of Ltac. As a monadic operation, it's a specialized "bind". *) let tclTHEN = Proof.(>>) diff --git a/engine/proofview.mli b/engine/proofview.mli index b7ff3ac432..60697c1611 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -24,7 +24,7 @@ type proofview ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) val proofview : proofview -> Evar.t list * Evd.evar_map @@ -95,7 +95,7 @@ type focus_context instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) val focus_context : focus_context -> Evar.t list * Evar.t list diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 80eb9d0124..8ed75a8d00 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -252,7 +252,7 @@ module Giveup : Writer with type t = goal list = struct let put gs = Logical.put (true, gs) end -(** Lens and utilies pertaining to the info trace *) +(** Lens and utilities pertaining to the info trace *) module InfoL = struct let recording = Logical.(map (fun {P.trace} -> trace) current) let if_recording t = diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 3437b6ce77..f0c9fdb589 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -145,7 +145,7 @@ module Shelf : State with type t = goal list of the tactic. *) module Giveup : Writer with type t = goal list -(** Lens and utilies pertaining to the info trace *) +(** Lens and utilities pertaining to the info trace *) module InfoL : sig (** [record_trace t] behaves like [t] and compute its [info] trace. *) val record_trace : 'a Logical.t -> 'a Logical.t diff --git a/engine/univMinim.ml b/engine/univMinim.ml index fcbf305f9d..4f9f9ce6a5 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -353,7 +353,7 @@ let normalize_context_set g ctx us algs weak = noneqs Constraint.empty in (* Compute the left and right set of flexible variables, constraints - mentionning other variables remain in noneqs. *) + mentioning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> let lus = LMap.mem l us and rus = LMap.mem r us in diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index c452c7b307..f9d18e7190 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -222,7 +222,7 @@ let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) t | Stoken _, _ -> true | _ -> false -(** Ancilliary datatypes *) +(** Ancillary datatypes *) type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml index 251e3dded3..4c66a6944e 100644 --- a/ide/configwin_types.ml +++ b/ide/configwin_types.ml @@ -87,7 +87,7 @@ type modifiers_param = { (** The value, as a list of modifiers and a key code *) md_editable : bool ; (** indicates if the value can be changed *) md_f_apply : Gdk.Tags.modifier list -> unit ; - (** the function to call to apply the new value of the paramter *) + (** the function to call to apply the new value of the parameter *) md_help : string option ; (** optional help string *) md_expand : bool ; (** expand or not *) md_allow : Gdk.Tags.modifier list diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index ccb6bedaf6..9d8fdf6335 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -34,7 +34,7 @@ type status = { status_path : string list; (** Module path of the current proof *) status_proofname : string option; - (** Current proof name. [None] if no focussed proof is in progress *) + (** Current proof name. [None] if no focused proof is in progress *) status_allproofs : string list; (** List of all pending proofs. Order is not significant *) status_proofnum : int; @@ -43,7 +43,7 @@ type status = { type 'a pre_goals = { fg_goals : 'a list; - (** List of the focussed goals *) + (** List of the focused goals *) bg_goals : ('a list * 'a list) list; (** Zipper representing the unfocused background goals *) shelved_goals : 'a list; @@ -70,7 +70,7 @@ type option_state = { opt_sync : bool; (** Whether an option is synchronous *) opt_depr : bool; - (** Wheter an option is deprecated *) + (** Whether an option is deprecated *) opt_name : string; (** A short string that is displayed when using [Test] *) opt_value : option_value; diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli index 31fc7b56f1..18d4b1eeee 100644 --- a/ide/protocol/richpp.mli +++ b/ide/protocol/richpp.mli @@ -25,7 +25,7 @@ type 'annotation located = { of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired - annotation. [width] sets the printing witdh of the formatter. *) + annotation. [width] sets the printing width of the formatter. *) val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli index 178f7c808f..4b47aa9f7c 100644 --- a/ide/protocol/xml_printer.mli +++ b/ide/protocol/xml_printer.mli @@ -16,11 +16,11 @@ type target = TChannel of out_channel | TBuffer of Buffer.t val make : target -> t (** Print the xml data structure to a source into a compact xml string (without - any user-readable formating ). *) + any user-readable formatting ). *) val print : t -> xml -> unit (** Print the xml data structure into a compact xml string (without - any user-readable formating ). *) + any user-readable formatting ). *) val to_string : xml -> string (** Print the xml data structure into an user-readable string with diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index e18219210f..5b37ca35ed 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -405,7 +405,7 @@ end = struct | (lg, rg) :: l -> Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in - Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals + Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 9f778d99e9..3ebbbdfb88 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -40,8 +40,8 @@ type explicitation = type binder_kind = | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool - (** Inner binding, outer bindings, typeclass-specific flag + | Generalized of binding_kind * bool + (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses *) type abstraction_kind = AbsLambda | AbsPi diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 443473d5b6..bcb2f34377 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with let binder_kind_eq b1 b2 = match b1, b2 with | Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 -| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> - binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 && +| Generalized (ck1, b1), Generalized (ck2, b2) -> + binding_kind_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb66658a37..fe50bd4b08 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -107,7 +107,7 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f06493b374..31f3736bae 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -389,7 +389,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} let intern_generalized_binder ?(global_level=false) intern_type ntnvars - env {loc;v=na} b b' t ty = + env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = if t then ty, ids else @@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) + (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -433,8 +433,8 @@ let intern_assumption intern ntnvars env nal bk ty = (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in + | Generalized (b',t) -> + let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in env, b let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function @@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); - (* Two possibilities: either the args are given with explict + (* Two possibilities: either the args are given with explicit variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be added later on; or the args are not enough to have all arguments, @@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with @returns a raw_case_pattern_expr : - no notations and syntactic definition - - global reference and identifeir instead of reference + - global reference and identifier instead of reference *) @@ -1642,7 +1642,7 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supportted only in local binders and only at top + are supported only in local binders and only at top level. In fact, they are currently eliminated by the parser. The only reason why they are in the [cases_pattern_expr] type is that the parser needs to factor diff --git a/interp/declare.mli b/interp/declare.mli index 2ffde31fc0..795d9a767d 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -40,7 +40,7 @@ type internal_flag = | InternalTacticRequest | UserIndividualRequest -(* Defaut definition entries, transparent with no secctx or proj information *) +(* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 806fe93297..f3cdd64633 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -96,11 +96,11 @@ let set_maximality imps b = this kind if there is enough arguments to infer them) - [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) - [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) diff --git a/interp/impargs.mli b/interp/impargs.mli index ccdd448460..1099074c63 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) + of a reference can be automatically inferred *) type argument_position = @@ -50,11 +50,11 @@ type implicit_explanation = this kind if there is enough arguments to infer them) *) | DepFlex of argument_position (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 6277d874dd..bac46c2d2f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -196,10 +196,9 @@ let combine_params avoid fn applied needed = user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") in aux [] avoid applied needed -let combine_params_freevar = - fun avoid (_, decl) -> - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) +let combine_params_freevar avoid (_, decl) = + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in @@ -222,34 +221,34 @@ let implicit_application env ?(allow_partial=true) f ty = let is_class = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in - let gr = Nametab.locate qid in - if Typeclasses.is_class gr then Some (clapp, gr) else None + if Libnames.idset_mem_qualid qid env then None + else + let gr = Nametab.locate qid in + if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in - match is_class with - | None -> ty, env - | Some ({CAst.loc;v=(id, par, inst)}, gr) -> - let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in - let c, avoid = - let env = Global.env () in - let sigma = Evd.from_env env in - let c = class_info env sigma gr in - let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in - CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid - in c, avoid + match is_class with + | None -> ty, env + | Some ({CAst.loc;v=(id, par, inst)}, gr) -> + let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let env = Global.env () in + let sigma = Evd.from_env env in + let c = class_info env sigma gr in + let (ci, rd) = c.cl_context in + if not allow_partial then + begin + let opt_succ x n = match x with + | None -> succ n + | Some _ -> n + in + let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in + let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in + if not (Int.equal needlen applen) then + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd + end; + let pars = List.rev (List.combine ci rd) in + let args, avoid = combine_params avoid f par pars in + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 49273c4146..a7e1de736c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = match onlyparse with | None -> (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) + notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat | _ -> () end diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 542a05fd25..a1c49bee95 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */ init_coq_interpreter(); /* Some predefined pointer code. - * It is typically contained in accumlator blocks whose tag is 0 and thus + * It is typically contained in accumulator blocks whose tag is 0 and thus * scanned by the GC, so make it look like an OCaml block. */ value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95f88c0306..fc7d1a54f2 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -226,7 +226,7 @@ let unfold_red kn = * this constant or abstraction. * * i_tab is the cache table of the results * - * ref_value_cache searchs in the tab, otherwise uses i_repr to + * ref_value_cache searches in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't * be unfolded, returns None, but does not store this failure. * This * doesn't take the RESET into account. You mustn't keep such a table @@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with and comp_subs el s = Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s -(* This function defines the correspondance between constr and +(* This function defines the correspondence between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1a790eaed6..60185464c5 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 69f004307d..90fbcb8ae3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -386,7 +386,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation *) +(* Extension of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function diff --git a/kernel/constr.mli b/kernel/constr.mli index 7fc57cdb8a..aa5878c9d7 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci]. - [p] stucture is [fun args x -> "return clause"] + [p] structure is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 36ee952099..860d19fe26 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -22,11 +22,11 @@ type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives - and constants hiding inductives are implicitely polymorphic when + and constants hiding inductives are implicitly polymorphic when applied to parameters, on the universes appearing in the whnf of their parameters and their conclusion, in a template style. - In truely universe polymorphic mode, we always use RegularArity. + In truly universe polymorphic mode, we always use RegularArity. *) type template_arity = { diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d9335d39b5..ca7086a3e4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -166,7 +166,7 @@ let make_subst env = (* template, it is identity substitution otherwise (ie. when u is *) (* already in the domain of the substitution) [remember_subst] will *) (* update its image [x] by [sup x u] in order not to forget the *) - (* dependency in [u] that remains to be fullfilled. *) + (* dependency in [u] that remains to be fulfilled. *) make (remember_subst u subst) (sign, exp, []) | _sign, [], _ -> (* Uniform parameters are exhausted *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 2de5faa6df..72393d0081 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = in let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature - with the identity substitution accompagned by the new resolver*) + with the identity substitution accompanied by the new resolver*) let id_subst = map_mp mp' mp' new_mb.mod_delta in let new_after = subst_structure id_subst after in before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst diff --git a/kernel/modops.ml b/kernel/modops.ml index 4fdd7ab334..472fddb829 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = "Module M:=P." or "Module M. Include P. End M." We need to perform two operations to compute the body of M. - The first one is applying the substitution {P <- M} on the type of P - - The second one is strenghtening. *) + - The second one is strengthening. *) let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with |NoFunctor struc -> diff --git a/kernel/uint63.mli b/kernel/uint63.mli index f25f24512d..93632da110 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -13,7 +13,7 @@ val of_uint : int -> t val hash : t -> int - (* convertion to a string *) + (* conversion to a string *) val to_string : t -> string val of_string : string -> t diff --git a/kernel/univ.ml b/kernel/univ.ml index b1bbc25fe6..2b88d6884d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -726,7 +726,7 @@ let univ_level_rem u v min = | Some u' -> if Level.equal u u' then min else v | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v -(* Is u mentionned in v (or equals to v) ? *) +(* Is u mentioned in v (or equals to v) ? *) (**********************************************************************) diff --git a/kernel/univ.mli b/kernel/univ.mli index db178c4bb0..ddb204dd52 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t val universe_level : Universe.t -> Level.t option -(** [univ_level_mem l u] Is l is mentionned in u ? *) +(** [univ_level_mem l u] Is l is mentioned in u ? *) val univ_level_mem : Level.t -> Universe.t -> bool diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 777a207013..5e3a3c3347 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -12,7 +12,7 @@ open Univ open Constr (*******************************************) -(* Initalization of the abstract machine ***) +(* Initialization of the abstract machine ***) (* Necessary for [relaccu_tbl] *) (*******************************************) diff --git a/lib/cProfile.mli b/lib/cProfile.mli index 764faf8d1a..00babe1a47 100644 --- a/lib/cProfile.mli +++ b/lib/cProfile.mli @@ -18,7 +18,7 @@ To trace a function "f" you first need to get a key for it by using : let fkey = declare_profile "f";; -(the string is used to print the profile infomation). Warning: this +(the string is used to print the profile information). Warning: this function does a side effect. Choose the ident you want instead "fkey". Then if the function has ONE argument add the following just after diff --git a/lib/envars.mli b/lib/envars.mli index ebf86d0650..558fe74042 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -38,7 +38,7 @@ val datadir : unit -> string (** [configdir] is the path to the installed config directory. *) val configdir : unit -> string -(** [set_coqlib] must be runned once before any access to [coqlib] *) +(** [set_coqlib] must be run once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) diff --git a/lib/feedback.mli b/lib/feedback.mli index f407e2fd5b..c9e6ca1266 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -56,7 +56,7 @@ type feedback = { (** {6 Feedback sent, even asynchronously, to the user interface} *) -(* The interpreter assignes an state_id to the ast, and feedbacks happening +(* The interpreter assigns a state_id to the ast, and feedbacks happening * during interpretation are attached to it. *) diff --git a/lib/flags.mli b/lib/flags.mli index a70a23b902..535b46950e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,7 +64,7 @@ val beautify : bool ref val beautify_file : bool ref (* Coq quiet mode. Note that normal mode is called "verbose" here, - whereas [quiet] supresses normal output such as goals in coqtop *) + whereas [quiet] suppresses normal output such as goals in coqtop *) val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b diff --git a/lib/pp.mli b/lib/pp.mli index 4ce6a535c8..8b3a07d4b2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -18,7 +18,7 @@ (* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned againt its use, *) +(* uses, however regular users are _strongly_ warned against its use, *) (* they should instead rely on the available functions below. *) (* *) (* Box order and number is indeed an important factor. Try to create *) diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 03468271d2..0eec18bd5a 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -88,7 +88,7 @@ Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight. -Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*". diff --git a/lib/spawn.mli b/lib/spawn.mli index 944aa27a7f..24bbded4f1 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -9,7 +9,7 @@ (************************************************************************) (* This module implements spawning/killing managed processes with a - * synchronous or asynchronous comunication channel that works with + * synchronous or asynchronous communication channel that works with * threads or with a glib like main loop model. * * This module requires no threads and no main loop model. It takes care diff --git a/library/declaremods.ml b/library/declaremods.ml index 5fd11e187a..d74bdd484c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -51,7 +51,7 @@ let inl2intopt = function - Then comes either the object segment itself (for interactive modules), or a compact way to store derived objects (path to - a earlier module + subtitution). + a earlier module + substitution). *) type algebraic_objects = diff --git a/library/libnames.ml b/library/libnames.ml index 87c4de42e8..41b38e0378 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,6 +162,9 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath +let idset_mem_qualid qid s = + qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s + (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index bbb4d2a058..7d77d95991 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t +val idset_mem_qualid : qualid -> Id.Set.t -> bool +(** false when the qualid is not an ident *) + (** {6 ... } *) (** some preset paths *) diff --git a/library/library.ml b/library/library.ml index f99bcc7ecf..9f4eb531ed 100644 --- a/library/library.ml +++ b/library/library.ml @@ -208,7 +208,7 @@ let register_open_library export m = let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentionned by the user are always reopen *) + (* Libraries explicitly mentioned by the user are always reopen *) List.exists (fun m' -> DirPath.equal m m') explicit_libs || not (library_is_opened m) then begin @@ -268,7 +268,7 @@ let in_import_library : DirPath.t list * bool -> obj = (** {6 Tables of opaque proof terms} *) (** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, we can quickly load a first half of a .vo file without these opaque terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) diff --git a/library/nametab.mli b/library/nametab.mli index a4f177aad0..33cb4faf99 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -38,7 +38,7 @@ open Globnames } {- [exists : full_user_name -> bool] - Is the [full_user_name] already atributed as an absolute user name + Is the [full_user_name] already attributed as an absolute user name of some object? } {- [locate : qualid -> object_reference] diff --git a/library/summary.mli b/library/summary.mli index 0d77d725ac..3875bcfe9e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,7 +28,7 @@ type 'a summary_declaration = { Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence - the responsability of plugins to initialize themselves properly. + the responsibility of plugins to initialize themselves properly. *) val declare_summary : string -> 'a summary_declaration -> unit diff --git a/man/coqdep.1 b/man/coqdep.1 index c417402c25..4639a75677 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -106,7 +106,7 @@ Skips subdirectory Output the given file name ordered by dependencies. .TP .B \-boot -For coq developpers, prints dependencies over coq library files +For coq developers, prints dependencies over coq library files (omitted by default). diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 4a9190c10a..6df97609f5 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -500,9 +500,9 @@ GRAMMAR EXTEND Gram | "{"; id=name; idl=LIST1 name; "}" -> { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> { let (p, ty) = match p.CAst.v with diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8f38e437b4..a78ad4f842 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -585,7 +585,7 @@ let unfreeze (grams, lex) = (** No need to provide an init function : the grammar state is statically available, and already empty initially, while - the lexer state should not be resetted, since it contains + the lexer state should not be reset, since it contains keywords declared in g_*.ml4 *) let parser_summary_tag = diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index 4bc3dba36e..bc7e1448f7 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -200,7 +200,7 @@ For the moment there are: Wf.well_founded_induction Wf.well_founded_induction_type Those constants does not match the auto-inlining criterion based on strictness. -Of course, you can still overide this behaviour via some Extraction NoInline. +Of course, you can still override this behaviour via some Extraction NoInline. * There is now a web page showing the extraction of all standard theories: http://www.lri.fr/~letouzey/extraction diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 36bb1148b6..02da168fd0 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -(** Restore lazyness of andb, orb. +(** Restore laziness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined - by extraction in order to have lazyness, producing inelegant + by extraction in order to have laziness, producing inelegant (if ... then ... else false) and (if ... then true else ...). *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 59c57cc544..f46d09e335 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -573,7 +573,7 @@ let pp_ocaml_gen k mp rls olab = if is_mp_bound base then pp_ocaml_bound base rls else pp_ocaml_extern k base rls -(* For Haskell, things are simplier: we have removed (almost) all structures *) +(* For Haskell, things are simpler: we have removed (almost) all structures *) let pp_haskell_gen k mp rls = match rls with | [] -> assert false @@ -590,7 +590,7 @@ let pp_global k r = let s = List.hd ls in let mp,l = repr_of_r r in if ModPath.equal mp (top_visible_mp ()) then - (* simpliest situation: definition of r (or use in the same context) *) + (* simplest situation: definition of r (or use in the same context) *) (* we update the visible environment *) (add_visible (k,s) l; unquote s) else @@ -607,7 +607,7 @@ let pp_module mp = let ls = mp_renaming mp in match mp with | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) -> - (* simpliest situation: definition of mp (or use in the same context) *) + (* simplest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in add_visible (Mod,s) l; s diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d7bb27f121..db1a389fe7 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY -(* Same, with content splitted in several files *) +(* Same, with content split in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] -> { separate_extraction l } END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4e229a94b6..c2c48f9565 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -101,7 +101,7 @@ let labels_of_ref r = (*S The main tables: constants, inductives, records, ... *) -(* Theses tables are not registered within coq save/undo mechanism +(* These tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum @@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj = ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + declare_object @@ superglobal_object_nodischarge "ML extractions custom matches" ~cache:(fun (_,(r,s)) -> add_custom_match r s) ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 287a374ab1..cffe8a3e78 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -658,7 +658,7 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = *) (fun g -> -(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *) +(* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) thin [hid] g ) ) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e9a2c285d0..f51c6dc6be 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -429,11 +429,11 @@ let get_funs_constant mp = let l_const = get_funs_constant const f in (* We need to check that all the functions found are in the same block - to prevent Reset stange thing + to prevent Reset strange thing *) let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in - (* all the paremeter must be equal*) + (* all the parameters must be equal*) let _check_params = let first_params = List.hd l_params in List.iter @@ -514,7 +514,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ ) fas in - (* We create the first priciple by tactic *) + (* We create the first principle by tactic *) let first_type,other_princ_types = match l_schemes with s::l_schemes -> s,l_schemes diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e15e167ff3..4c67d65816 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1369,7 +1369,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in @@ -1438,7 +1438,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 481a8be3ba..24b3690138 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -55,7 +55,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr Glob_term.cases_pattern * Id.Map.key list * Id.t Id.Map.t -(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt +(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result respects barendregt conventions and does not share bound variables with avoid *) val alpha_rt : Id.t list -> glob_constr -> glob_constr diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 40f66ce5eb..48cf040919 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -115,7 +115,7 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (*****************************************************************) -(* Copy of the standart save mechanism but without the much too *) +(* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) open Entries @@ -357,7 +357,7 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) -(* Debuging *) +(* Debugging *) let functional_induction_rewrite_dependent_proofs = ref true let function_debug = ref false open Goptions diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index edb698280f..2a0140f02c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -591,7 +591,7 @@ let rec reflexivity_with_destruct_cases g = (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] - is the tactic used to prove completness lemma. + is the tactic used to prove completeness lemma. [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. @@ -748,7 +748,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let env = Global.env () in @@ -928,7 +928,7 @@ let revert_graph kn post_tac hid g = [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct] is the correctness lemma for [fconst]. - The sketch is the follwing~: + The sketch is the following~: \begin{enumerate} \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ (fails if it is not possible) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1fca132655..216be3797b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1584,7 +1584,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let pstate = com_terminate tcc_lemma_name diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 963b7189f9..164bd7e118 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -30,7 +30,6 @@ open Evd open Tactypes open Locus open Locusops -open Decl_kinds open Elimschemes open Environ open Termops @@ -207,7 +206,7 @@ end) = struct let mk_relation env evd a = app_poly env evd relation [| a |] - (** Build an infered signature from constraints on the arguments and expected output + (** Build an inferred signature from constraints on the arguments and expected output relation *) let build_signature evars env m (cstrs : (types * types option) option list) @@ -1791,15 +1790,15 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = - (((CAst.make @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders instance fields = +let anew_instance ~pstate atts binders (name,t) fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic - binders instance (Some (true, CAst.make @@ CRecord (fields))) + name binders t (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = @@ -2014,16 +2013,18 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = let add_morphism ~pstate atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in - let instance = - (((CAst.make @@ Name instance_id),None), Explicit, - CAst.make @@ CAppExpl ( - (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + let instance_name = (CAst.make @@ Name instance_id),None in + let instance_t = + CAst.make @@ CAppExpl + ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), + [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in + let _, pstate = new_instance ~pstate + ~program_mode:atts.program ~global:atts.global atts.polymorphic + instance_name binders instance_t None + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + in pstate (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 0eb7726a18..8bd69dd4fd 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index fd303f5d94..f839c3e886 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 800be2565d..4a0b01bcdc 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) - (* a name intented to be used as a (non-variable) identifier *) + (* a name intended to be used as a (non-variable) identifier *) try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id @@ -2075,7 +2075,7 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* EJGA: We sould also pass the proof name if desired, for now + (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) let name, poly = Id.of_string "ltac_gen", poly in diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 2b5e496168..7783661787 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v index 47fcac6481..4e8fe5a8ff 100644 --- a/plugins/micromega/DeclConstant.v +++ b/plugins/micromega/DeclConstant.v @@ -62,6 +62,7 @@ Instance DZO: DeclaredConstant Z0 := {}. Instance DZpos: DeclaredConstant Zpos := {}. Instance DZneg: DeclaredConstant Zneg := {}. Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}. +Instance DZpow : DeclaredConstant Z.pow := {}. Require Import QArith. diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 6112eda200..830cbdf7f6 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -55,7 +55,7 @@ Extract Constant Rinv => "fun x -> 1 / x". extraction is only performed as a test in the test suite. *) (*Extraction "micromega.ml" Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula - ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ + ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index e0e2232be5..7759bda7c7 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -129,7 +129,7 @@ Proof. intros n m H1 H2; rewrite H2 in H1; now apply H1. Qed. -(* Propeties of plus, minus and opp *) +(* Properties of plus, minus and opp *) Theorem Rplus_0_l : forall n : R, 0 + n == n. Proof. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 60931df517..c5e179fbb8 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -990,7 +990,7 @@ Proof. rewrite IHs. reflexivity. Qed. -(** equality migth be (too) strong *) +(** equality might be (too) strong *) Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). Proof. destruct f. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index ab218a1778..953690c510 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -75,6 +75,21 @@ Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x => x) (pow_N 1 Z.mul). +Fixpoint Zeval_const (e: PExpr Z) : option Z := + match e with + | PEc c => Some c + | PEX _ x => None + | PEadd e1 e2 => map_option2 (fun x y => Some (x + y)) + (Zeval_const e1) (Zeval_const e2) + | PEmul e1 e2 => map_option2 (fun x y => Some (x * y)) + (Zeval_const e1) (Zeval_const e2) + | PEpow e1 n => map_option (fun x => Some (Z.pow x (Z.of_N n))) + (Zeval_const e1) + | PEsub e1 e2 => map_option2 (fun x y => Some (x - y)) + (Zeval_const e1) (Zeval_const e2) + | PEopp e => map_option (fun x => Some (Z.opp x)) (Zeval_const e) + end. + Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n. Proof. destruct n. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index de9dec0f74..48027442b2 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -346,7 +346,9 @@ struct let coq_PsatzC = lazy (constant "PsatzC") let coq_PsatzZ = lazy (constant "PsatzZ") - let coq_GT = lazy (m_constant "GT") + (* let coq_GT = lazy (m_constant "GT")*) + + let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant") let coq_TT = lazy (gen_constant_in_modules "ZMicromega" @@ -462,13 +464,24 @@ struct what to consider as a constant (see [parse_constant]) *) - let is_ground_term env sigma term = - let typ = Retyping.get_type_of env sigma term in - try - ignore (Typeclasses.resolve_one_typeclass env sigma (EConstr.mkApp(Lazy.force coq_GT,[| typ;term|]))) ; - true - with - | Not_found -> false + let is_declared_term env evd t = + match EConstr.kind evd t with + | Const _ | Construct _ -> (* Restrict typeclass resolution to trivial cases *) + begin + let typ = Retyping.get_type_of env evd t in + try + ignore (Typeclasses.resolve_one_typeclass env evd (EConstr.mkApp(Lazy.force coq_DeclaredConstant,[| typ;t|]))) ; true + with Not_found -> false + end + | _ -> false + + let rec is_ground_term env evd term = + match EConstr.kind evd term with + | App(c,args) -> + is_declared_term env evd c && + Array.for_all (is_ground_term env evd) args + | Const _ | Construct _ -> is_declared_term env evd term + | _ -> false let parse_z sigma term = @@ -674,26 +687,28 @@ struct let parse_zop gl (op,args) = let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" + match args with + | [| a1 ; a2|] -> assoc_const sigma op zop_table, a1, a2 + | [| ty ; a1 ; a2|] -> + if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl ty (Lazy.force coq_Z) + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError + | _ -> raise ParseError let parse_rop gl (op,args) = let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" + match args with + | [| a1 ; a2|] -> assoc_const sigma op rop_table, a1 , a2 + | [| ty ; a1 ; a2|] -> + if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl ty (Lazy.force coq_R) + then (Mc.OpEq, a1, a2) + else raise ParseError + | _ -> raise ParseError let parse_qop gl (op,args) = - (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) + if Array.length args = 2 + then (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) + else raise ParseError type 'a op = | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) @@ -804,7 +819,7 @@ struct (op expr1 expr2,env) in try (Mc.PEc (parse_constant gl term) , env) - with ParseError -> + with ParseError -> match EConstr.kind gl.sigma term with | App(t,args) -> ( @@ -820,7 +835,7 @@ struct let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) - with e when CErrors.noncritical e -> + with ParseError -> (* if the exponent is a variable *) let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) end @@ -858,19 +873,48 @@ struct coq_Ropp , Opp ; coq_Rpower , Power] - (** [parse_constant parse gl t] returns the reification of term [t]. + let parse_constant parse gl t = parse gl.sigma t + + (** [parse_more_constant parse gl t] returns the reification of term [t]. If [t] is a ground term, then it is first reduced to normal form before using a 'syntactic' parser *) - let parse_constant parse gl t = - if is_ground_term gl.env gl.sigma t - then - parse gl.sigma (Redexpr.cbv_vm gl.env gl.sigma t) - else raise ParseError + let parse_more_constant parse gl t = + try + parse gl t + with ParseError -> + begin + if debug then Feedback.msg_debug Pp.(str "try harder"); + if is_ground_term gl.env gl.sigma t + then parse gl (Redexpr.cbv_vm gl.env gl.sigma t) + else raise ParseError + end let zconstant = parse_constant parse_z let qconstant = parse_constant parse_q let nconstant = parse_constant parse_nat + (** [parse_more_zexpr parse_constant gl] improves the parsing of exponent + which can be arithmetic expressions (without variables). + [parse_constant_expr] returns a constant if the argument is an expression without variables. *) + + let rec parse_zexpr gl = + parse_expr gl + zconstant + (fun expr (x:EConstr.t) -> + let z = parse_zconstant gl x in + match z with + | Mc.Zneg _ -> Mc.PEc Mc.Z0 + | _ -> Mc.PEpow(expr, Mc.Z.to_N z) + ) + zop_spec + and parse_zconstant gl e = + let (e,_) = parse_zexpr gl (Env.empty gl) e in + match Mc.zeval_const e with + | None -> raise ParseError + | Some z -> z + + + (* NB: R is a different story. Because it is axiomatised, reducing would not be effective. Therefore, there is a specific parser for constant over R @@ -905,7 +949,7 @@ struct let b = rconstant args.(1) in f a b with - ParseError -> + ParseError -> match op with | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> let arg = rconstant args.(0) in @@ -913,12 +957,12 @@ struct then raise ParseError (* This is a division by zero -- no semantics *) else Mc.CInv(arg) | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> - Mc.CPow(rconstant args.(0) , Mc.Inr (nconstant gl args.(1))) + Mc.CPow(rconstant args.(0) , Mc.Inr (parse_more_constant nconstant gl args.(1))) | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> Mc.CQ (qconstant gl args.(0)) | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> - Mc.CZ (zconstant gl args.(0)) - | _ -> raise ParseError + Mc.CZ (parse_more_constant zconstant gl args.(0)) + | _ -> raise ParseError end | _ -> raise ParseError in @@ -934,14 +978,6 @@ struct res - let parse_zexpr gl = parse_expr gl - zconstant - (fun expr x -> - let exp = (zconstant gl x) in - match exp with - | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) - zop_spec let parse_qexpr gl = parse_expr gl qconstant @@ -952,7 +988,7 @@ struct begin match expr with | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) - | _ -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError + | _ -> raise ParseError end | _ -> let exp = Mc.Z.to_N exp in Mc.PEpow(expr,exp)) @@ -1031,14 +1067,16 @@ struct let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg | _ -> parse_atom env tg term) - | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b -> + | Prod(typ,a,b) when typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg - | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (Mc.TT,env,tg) - | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> Mc.(FF,env,tg) - | _ when is_prop term -> Mc.X(term),env,tg - | _ -> raise ParseError + | _ -> if EConstr.eq_constr sigma term (Lazy.force coq_True) + then (Mc.TT,env,tg) + else if EConstr.eq_constr sigma term (Lazy.force coq_False) + then Mc.(FF,env,tg) + else if is_prop term then Mc.X(term),env,tg + else raise ParseError in xparse_formula env tg ((*Reductionops.whd_zeta*) term) @@ -1170,8 +1208,8 @@ let dump_rexpr = lazy (** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occuring in form - - props is an environment for the propositions occuring in form + - vars is an environment for the arithmetic variables occurring in form + - props is an environment for the propositions occurring in form @return a goal where all the variables and propositions of the formula are quantified *) @@ -1358,19 +1396,11 @@ let rec parse_hyps gl parse_arith env tg hyps = let (c,env,tg) = parse_formula gl parse_arith env tg t in ((i,c)::lhyps, env,tg) with e when CErrors.noncritical e -> (lhyps,env,tg) - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - - -(*exception ParseError*) - - let parse_goal gl parse_arith (env:Env.t) hyps term = - (* try*) let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in (lhyps,f,env) - (* with Failure x -> raise ParseError*) (** * The datastructures that aggregate theory-dependent proof values. @@ -1439,7 +1469,7 @@ let pre_processZ mt f = x <= y or (x and y are incomparable) *) (** - * Instanciate the current Coq goal with a Micromega formula, a varmap, and a + * Instantiate the current Coq goal with a Micromega formula, a varmap, and a * witness. *) @@ -1886,7 +1916,7 @@ let micromega_genr prover tac = ] with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") | CsdpNotFound -> flush stdout ; Tacticals.New.tclFAIL 0 (Pp.str diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index b34c3b2b7d..a64a5a84b3 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -230,6 +230,13 @@ module Coq_Pos = | XO p -> XO (mul p y) | XH -> y + (** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) + + let rec iter f x = function + | XI n' -> f (iter f (iter f x n') n') + | XO n' -> iter f (iter f x n') n' + | XH -> f x + (** val size_nat : positive -> nat **) let rec size_nat = function @@ -398,6 +405,18 @@ module Z = | Zpos y' -> Zneg (Coq_Pos.mul x' y') | Zneg y' -> Zpos (Coq_Pos.mul x' y')) + (** val pow_pos : z -> positive -> z **) + + let pow_pos z0 = + Coq_Pos.iter (mul z0) (Zpos XH) + + (** val pow : z -> z -> z **) + + let pow x = function + | Z0 -> Zpos XH + | Zpos p -> pow_pos x p + | Zneg _ -> Z0 + (** val compare : z -> z -> comparison **) let compare x y = @@ -460,6 +479,12 @@ module Z = | O -> Z0 | S n1 -> Zpos (Coq_Pos.of_succ_nat n1) + (** val of_N : n -> z **) + + let of_N = function + | N0 -> Z0 + | Npos p -> Zpos p + (** val pos_div_eucl : positive -> z -> z * z **) let rec pos_div_eucl a b = @@ -1642,6 +1667,21 @@ let rec vm_add default x v = function | XO p -> Branch ((vm_add default p v l), o, r) | XH -> Branch (l, v, r)) +(** val zeval_const : z pExpr -> z option **) + +let rec zeval_const = function +| PEc c -> Some c +| PEX _ -> None +| PEadd (e1, e2) -> + map_option2 (fun x y -> Some (Z.add x y)) (zeval_const e1) (zeval_const e2) +| PEsub (e1, e2) -> + map_option2 (fun x y -> Some (Z.sub x y)) (zeval_const e1) (zeval_const e2) +| PEmul (e1, e2) -> + map_option2 (fun x y -> Some (Z.mul x y)) (zeval_const e1) (zeval_const e2) +| PEopp e0 -> map_option (fun x -> Some (Z.opp x)) (zeval_const e0) +| PEpow (e1, n0) -> + map_option (fun x -> Some (Z.pow x (Z.of_N n0))) (zeval_const e1) + type zWitness = z psatz (** val zWeakChecker : z nFormula list -> z psatz -> bool **) diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 5de6caac0b..64cb3a8355 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -86,6 +86,8 @@ module Coq_Pos : val mul : positive -> positive -> positive + val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 + val size_nat : positive -> nat val compare_cont : comparison -> positive -> positive -> comparison @@ -124,6 +126,10 @@ module Z : val mul : z -> z -> z + val pow_pos : z -> positive -> z + + val pow : z -> z -> z + val compare : z -> z -> comparison val leb : z -> z -> bool @@ -140,6 +146,8 @@ module Z : val of_nat : nat -> z + val of_N : n -> z + val pos_div_eucl : positive -> z -> z * z val div_eucl : z -> z -> z * z @@ -179,20 +187,20 @@ val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol val paddI : - ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 - pol -> 'a1 pol + ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol + -> 'a1 pol val psubI : ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> - positive -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> + 'a1 pol -> 'a1 pol val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> - 'a1 pol -> positive -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 + pol -> positive -> 'a1 pol -> 'a1 pol val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol @@ -205,20 +213,19 @@ val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol val pmulC : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 - pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> - 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 + pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 pol -> 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + pol -> 'a1 pol -> 'a1 pol val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + pol -> 'a1 pol type 'c pExpr = | PEc of 'c @@ -232,16 +239,16 @@ type 'c pExpr = val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol val ppow_pos : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol type ('tA, 'tX, 'aA, 'aF) gFormula = | TT @@ -253,8 +260,7 @@ type ('tA, 'tX, 'aA, 'aF) gFormula = | N of ('tA, 'tX, 'aA, 'aF) gFormula | I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula -val mapX : - ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula +val mapX : ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 @@ -278,37 +284,36 @@ val cnf_tt : ('a1, 'a2) cnf val cnf_ff : ('a1, 'a2) cnf val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> - ('a1, 'a2) clause option + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, + 'a2) clause option val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) - clause -> ('a1, 'a2) clause option + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> + ('a1, 'a2) clause option val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf - -> ('a1, 'a2) cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> + ('a1, 'a2) cnf val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> - ('a1, 'a2) cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> - ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, - 'a3) cnf + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> + 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 list) sum val ror_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause - -> (('a1, 'a2) clause, 'a2 list) sum + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> + (('a1, 'a2) clause, 'a2 list) sum val ror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause @@ -319,17 +324,16 @@ val ror_cnf : clause list -> ('a1, 'a2) cnf * 'a2 list val rxcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> - ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, - 'a3) cnf * 'a3 list + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> + 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 + list -val cnf_checker : - (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool +val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> - ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, - 'a3, unit0) gFormula -> 'a4 list -> bool + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> + 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0) + gFormula -> 'a4 list -> bool val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool @@ -363,27 +367,27 @@ val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option val pexpr_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + polC -> 'a1 nFormula -> 'a1 nFormula option val nformula_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + nFormula -> 'a1 nFormula -> 'a1 nFormula option val nformula_plus_nformula : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula - -> 'a1 nFormula option + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> + 'a1 nFormula option val eval_Psatz : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool val check_normalised_formulas : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool type op2 = | OpEq @@ -396,8 +400,8 @@ type op2 = type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } val norm : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> @@ -407,20 +411,20 @@ val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf val xdenorm : positive -> 'a1 pol -> 'a1 pExpr @@ -475,6 +479,8 @@ val singleton : 'a1 -> positive -> 'a1 -> 'a1 t val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t +val zeval_const : z pExpr -> z option + type zWitness = z psatz val zWeakChecker : z nFormula list -> z psatz -> bool @@ -563,12 +569,12 @@ val bound_var : positive -> z formula val mk_eq_pos : positive -> positive -> positive -> z formula val bound_vars : - (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, - 'a1, 'a2, 'a3) gFormula + (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, 'a1, + 'a2, 'a3) gFormula val bound_problem_fr : - (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, - 'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula + (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, 'a3) + gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula val zChecker : z nFormula list -> zArithProof -> bool diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 0209030b64..f038f8a71a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -21,7 +21,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli index 4e7a388aaf..d2f3e756a9 100644 --- a/plugins/micromega/persistent_cache.mli +++ b/plugins/micromega/persistent_cache.mli @@ -17,7 +17,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 6aebc4ca9a..e3a9f6f60f 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -200,7 +200,7 @@ let is_undefined f = | _ -> false;; (* ------------------------------------------------------------------------- *) -(* Operation analagous to "map" for lists. *) +(* Operation analogous to "map" for lists. *) (* ------------------------------------------------------------------------- *) let mapf = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 1777418ef6..bece316c7d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -267,7 +267,7 @@ module PIdeal = Ideal.Make(Poly) open PIdeal (* term to sparse polynomial - varaibles <=np are in the coefficients + variables <=np are in the coefficients *) let term_pol_sparse nvars np t= diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 5db587b9cc..f6ca232c2e 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -357,7 +357,7 @@ let remP v p = moinsP p (multP (coefDom v p) (puisP (x v) (deg v p))) -(* first interger coefficient of p *) +(* first integer coefficient of p *) let rec coef_int_tete p = let v = max_var_pol p in if v>0 @@ -526,7 +526,7 @@ let div_pol_rat p q= (* pseudo division : q = c*x^m+q1 - retruns (r,c,d,s) s.t. c^d*p = s*q + r. + returns (r,c,d,s) s.t. c^d*p = s*q + r. *) let pseudo_div p q x = diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 695f000cb1..23d7b141a4 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -359,7 +359,10 @@ Ltac zify_positive_rel := Ltac zify_positive_op := match goal with - (* Zneg -> -Zpos (except for numbers) *) + (* Z.pow_pos -> Z.pow *) + | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H + | |- context [ Z.pow_pos ?a ?b ] => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) + (* Zneg -> -Zpos (except for numbers) *) | H : context [ Zneg ?a ] |- _ => let isp := isPcst a in match isp with @@ -377,6 +380,10 @@ Ltac zify_positive_op := | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + (* Z.power_pos *) + | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H + | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + (* Pos.add -> Z.add *) | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b) diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 49d729bd6c..c5f387b248 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -49,7 +49,7 @@ Require Import ssreflect ssrfun. altP (idP my_formula) but circumventing the dependent index capture issue; destructing boolP my_formula generates two subgoals with - assumtions my_formula and ~~ myformula. As + assumptions my_formula and ~~ myformula. As with altP, my_formula must be an application. \unless C, P <-> we can assume property P when a something that holds under condition C (such as C itself). @@ -64,7 +64,7 @@ Require Import ssreflect ssrfun. := forall b : bool, (P -> b) -> b. This is equivalent to ~ (~ P) when P : Prop. implies P Q == wrapper variant type that coerces to P -> Q and - can be used as a P -> Q view unambigously. + can be used as a P -> Q view unambiguously. Useful to avoid spurious insertion of <-> views when Q is a conjunction of foralls, as in Lemma all_and2 below; conversely, avoids confusion in @@ -1003,7 +1003,7 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(** Pseudo-cancellation -- i.e, absorbtion **) +(** Pseudo-cancellation -- i.e, absorption **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. @@ -1245,7 +1245,7 @@ Notation "[ 'pred' x : T | E1 & E2 ]" := (** Coercions for simpl_pred. As simpl_pred T values are used both applicatively and collectively we need simpl_pred to coerce to both pred T _and_ {pred T}. However it is - undesireable to have two distinct constants for what are essentially identical + undesirable to have two distinct constants for what are essentially identical coercion functions, as this confuses the SSReflect keyed matching algorithm. While the Coq Coercion declarations appear to disallow such Coercion aliasing, it is possible to work around this limitation with a combination of modules @@ -1331,9 +1331,9 @@ Variant mem_pred T := Mem of pred T. Similarly to pred_of_simpl, it will usually not be inserted by type inference, as all mem_pred mp =~= pred_sort ?pT unification problems will be solve by the memPredType instance below; pred_of_mem will however - be used if a mem_pred T is used as a {pred T}, which is desireable as it + be used if a mem_pred T is used as a {pred T}, which is desirable as it will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma - expection a generic collective predicate p : {pred T} and premise x \in P + exception a generic collective predicate p : {pred T} and premise x \in P will display a subgoal x \in A rathere than x \in mem A. Conversely, pred_of_mem will _not_ if it is used id (mem A) is used applicatively or as a pred T; there the simpl_of_mem coercion defined below @@ -1396,7 +1396,7 @@ Notation "[ 'rel' x y 'in' A & B ]" := Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope. Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope. -(** Aliases of pred T that let us tag intances of simpl_pred as applicative +(** Aliases of pred T that let us tag instances of simpl_pred as applicative or collective, via bespoke coercions. This tagging will give control over the simplification behaviour of inE and othe rewriting lemmas below. For this control to work it is crucial that collective_of_simpl _not_ @@ -1428,7 +1428,7 @@ Implicit Types (mp : mem_pred T). - registered_applicative_pred: this user-facing structure is used to declare values of type pred T meant to be used applicatively. The structure parameter merely displays this same value, and is used to avoid - undesireable, visible occurrence of the structure in the right hand side + undesirable, visible occurrence of the structure in the right hand side of rewrite rules such as app_predE. There is a canonical instance of registered_applicative_pred for values of the applicative_of_simpl coercion, which handles the @@ -1454,7 +1454,7 @@ Implicit Types (mp : mem_pred T). has been fixed earlier by the manifest_mem_pred match. In particular the definition of a predicate using the applicative_pred_of_simpl idiom above will not be expanded - this very case is the reason in_applicative uses - a mem_pred telescope in its left hand side. The more straighforward + a mem_pred telescope in its left hand side. The more straightforward ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap)) with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...] rather than ?p := Apred in the example above. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 5e3e8ce5fb..572d72ccd8 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -132,7 +132,7 @@ Delimit Scope ssripat_scope with ssripat. Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer - avoids a spurrious trailing %%GEN_IF. **) + avoids a spurious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. @@ -347,10 +347,10 @@ Register protect_term as plugins.ssreflect.protect_term. (** The ssreflect idiom for a non-keyed pattern: - - unkeyed t wiil match any subterm that unifies with t, regardless of + - unkeyed t will match any subterm that unifies with t, regardless of whether it displays the same head symbol as t. - unkeyed t a b will match any application of a term f unifying with t, - to two arguments unifying with with a and b, repectively, regardless of + to two arguments unifying with with a and b, respectively, regardless of apparent head symbols. - unkeyed x where x is a variable will match any subterm with the same type as x (when x would raise the 'indeterminate pattern' error). **) @@ -380,7 +380,7 @@ Notation "=^~ r" := (ssr_converse r) : form_scope. locked_with k t is equal but not convertible to t, much like locked t, but supports explicit tagging with a value k : unit. This is used to mitigate a flaw in the term comparison heuristic of the Coq kernel, - which treats all terms of the form locked t as equal and conpares their + which treats all terms of the form locked t as equal and compares their arguments recursively, leading to an exponential blowup of comparison. For this reason locked_with should be used rather than locked when defining ADT operations. The unlock tactic does not support locked_with @@ -523,7 +523,7 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. elim/abstract_context: (pattern) => G defG. vm_compute; rewrite {}defG {G}. Note that vm_cast are not stored in the proof term - for reductions occuring in the context, hence + for reductions occurring in the context, hence set here := pattern; vm_compute in (value of here) blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : @@ -637,7 +637,7 @@ Ltac over := later complain that it cannot erase _top_assumption_ after having abstracted the viewed assumption. Making x and y maximal implicits would avoid this and force the intended @Some_inj nat x y _top_assumption_ - interpretation, but is undesireable as it makes it harder to use Some_inj + interpretation, but is undesirable as it makes it harder to use Some_inj with the many SSReflect and MathComp lemmas that have an injectivity premise. Specifying {T : nonPropType} solves this more elegantly, as then (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop. @@ -655,13 +655,13 @@ Module NonPropType. maybeProp T to tt and use the test_negative instance and set ?r to false. - call_of c r sets up a call to test_of on condition c with expected result r. It has a default instance for its 'callee' projection to Type, which - sets c := maybeProj T and r := false whe unifying with a type T. + sets c := maybeProj T and r := false when unifying with a type T. - type is a telescope on call_of c r, which checks that unifying test_of ?r1 with c indeed sets ?r1 := r; the type structure bundles the 'test' instance and its 'result' value along with its call_of c r projection. The default instance essentially provides eta-expansion for 'type'. This is only essential for the first 'result' projection to bool; using the instance - for other projection merely avoids spurrious delta expansions that would + for other projection merely avoids spurious delta expansions that would spoil the notProp T notation. In detail, unifying T =~= ?S with ?S : nonPropType, i.e., (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 675e4d2457..dbc9bb24c5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -96,7 +96,7 @@ let subgoals_tys sigma (relctx, concl) = * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None - * 4. build the tactic handle intructions and clears as required in ipats and + * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) let get_eq_type gl = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 93c0d5c236..59fc69f100 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -128,7 +128,7 @@ let newssrcongrtac arg ist gl = x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in - (* here thw two cases: simple equality or arrow *) + (* here the two cases: simple equality or arrow *) let equality, _, eq_args, gl' = let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in @@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) -(* such a generic Leibnitz equation -- short of inspecting the type *) +(* such a generic Leibniz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match Constr.kind c with diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 25975c84e8..6d1d858648 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -143,7 +143,7 @@ val mk_tpattern : type find_P = env -> constr -> int -> k:subst -> constr -(** [conclude ()] asserts that all mentioned ocurrences have been visited. +(** [conclude ()] asserts that all mentioned occurrences have been visited. @return the instance of the pattern, the evarmap after the pattern instantiation, the proof term and the ssrdit stored in the tpattern @raise UserEerror if too many occurrences were specified *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 78733784a7..9d3ed40f6c 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -339,8 +339,7 @@ let tag_var = tag Tag.variable let pr_binder many pr (nal,k,t) = match k with - | Generalized (b, b', t') -> - assert (match b with Implicit -> true | _ -> false); + | Generalized (b', t') -> begin match nal with |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' diff --git a/stm/stm.ml b/stm/stm.ml index 2a7fb084fc..d469994f3f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -100,6 +100,15 @@ let forward_feedback, forward_feedback_hook = let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun ~doc:_ _ _ -> ()) () +let document_add, document_add_hook = Hook.make + ~default:(fun _ _ -> ()) () + +let document_edit, document_edit_hook = Hook.make + ~default:(fun _ -> ()) () + +let sentence_exec, sentence_exec_hook = Hook.make + ~default:(fun _ -> ()) () + include Hook (* enables: Hooks.(call foo args) *) @@ -571,7 +580,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i - | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i + | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -2767,6 +2776,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = doc, VCS.cur_tip () let observe ~doc id = + Hooks.(call sentence_exec id); let vcs = VCS.backup () in try Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; @@ -3122,6 +3132,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> ) (0, 0) loc let add ~doc ~ontop ?newtip verb ast = + Hooks.(call document_add ast ontop); let loc = ast.CAst.loc in let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then @@ -3167,6 +3178,7 @@ let query ~doc ~at ~route s = s let edit_at ~doc id = + Hooks.(call document_edit id); if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = @@ -3322,6 +3334,9 @@ let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let forward_feedback_hook = Hooks.forward_feedback_hook let unreachable_state_hook = Hooks.unreachable_state_hook +let document_add_hook = Hooks.document_add_hook +let document_edit_hook = Hooks.document_edit_hook +let sentence_exec_hook = Hooks.sentence_exec_hook let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) type document = VCS.vcs diff --git a/stm/stm.mli b/stm/stm.mli index 73f3ffab7e..24c672c973 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -282,6 +282,19 @@ val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t +(* + * Hooks into the UI for plugins (not for general use) + *) + +(** User adds a sentence to the document (after parsing) *) +val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t + +(** User edits a sentence in the document *) +val document_edit_hook : (Stateid.t -> unit) Hook.t + +(** User requests evaluation of a sentence *) +val sentence_exec_hook : (Stateid.t -> unit) Hook.t + val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 7cecd801e4..aa16f9535d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -188,11 +188,11 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater - | VernacInstance (_,((name,_),_,_),_,_) -> + | VernacInstance ((name,_),_,_,_,_) -> VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll diff --git a/test-suite/bugs/closed/bug_10176.v b/test-suite/bugs/closed/bug_10176.v new file mode 100644 index 0000000000..fdb0eb87a4 --- /dev/null +++ b/test-suite/bugs/closed/bug_10176.v @@ -0,0 +1,7 @@ +Class Foo (xxx:nat) := foo : nat. + +Lemma aa `{Foo} : nat. Abort. + +Fail Lemma xy (Foo:bool->Type) `{Foo} : nat. + +Fail Lemma yx (Fooo:bool->Type) `{Fooo} : nat. diff --git a/test-suite/micromega/bug_10158.v b/test-suite/micromega/bug_10158.v new file mode 100644 index 0000000000..2c8f798f12 --- /dev/null +++ b/test-suite/micromega/bug_10158.v @@ -0,0 +1,48 @@ +Require Import ZArith_base. +Require Import Coq.micromega.Lia. + +Open Scope Z_scope. + +Fixpoint fib (n: nat) : Z := + match n with + | O => 1 + | S O => 1 + | S (S n as p) => fib p + fib n + end. + +Axiom fib_47_computed: fib 47 = 2971215073. + +Lemma fib_bound: + fib 47 < 2 ^ 32. +Proof. + pose proof fib_47_computed. + lia. +Qed. + +Require Import Reals. +Require Import Coq.micromega.Lra. + +Open Scope R_scope. + +Fixpoint fibr (n: nat) : R := + match n with + | O => 1 + | S O => 1 + | S (S n as p) => fibr p + fibr n + end. + +Axiom fibr_47_computed: fibr 47 = 2971215073. + +Lemma fibr_bound: + fibr 47 < 2 ^ 32. +Proof. + pose proof fibr_47_computed. + lra. +Qed. + +Lemma fibr_bound': + fibr 47 < IZR (Z.pow_pos 2 32). +Proof. + pose proof fibr_47_computed. + lra. +Qed. diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v index 02b98b562f..f02d93f911 100644 --- a/test-suite/micromega/rsyntax.v +++ b/test-suite/micromega/rsyntax.v @@ -57,15 +57,7 @@ Require Import Lia. Goal ( 1 ^ (2 + 2) = 1)%Z. Proof. - Fail lia. - reflexivity. -Qed. - -Instance DZplus : DeclaredConstant Z.add := {}. - -Goal ( 1 ^ (2 + 2) = 1)%Z. -Proof. - lia. + lia. (* exponent is a constant expr *) Qed. diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh index 8b4a49e577..ed473e5874 100755 --- a/test-suite/misc/changelog.sh +++ b/test-suite/misc/changelog.sh @@ -1,11 +1,9 @@ #!/bin/sh -while read line; do - if [ "$line" = "is_a_released_version = False" ]; then +if grep -q -F "is_a_released_version = False" ../config/coq_config.py; then echo "This is not a released version: nothing to test." exit 0 - fi -done < ../config/coq_config.py +fi for d in ../doc/changelog/*; do if [ -d "$d" ]; then diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 7429a521b3..c0ef9b392d 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -7,8 +7,8 @@ Require Import QMicromega. Require Import RMicromega. Recursive Extraction - Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula - ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ +Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula + ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index c014ecc7ab..2dd254496b 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -337,7 +337,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) - Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. apply H. firstorder. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index e9a9d6aff2..7f26181108 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -94,7 +94,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Obligation Tactic := unfold complement, equiv ; program_simpl. Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) : - ! EqDec (prod A B) eq := + EqDec (prod A B) eq := { equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -115,7 +115,7 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : (** Objects of function spaces with countable domains like bool have decidable equality. Proving the reflection requires functional extensionality though. *) -Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := +Program Instance bool_function_eqdec `(EqDec A eq) : EqDec (bool -> A) eq := { equiv_dec f g := if f true == g true then if f false == g false then in_left @@ -130,7 +130,7 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := Require Import List. -Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := +Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := { equiv_dec := fix aux (x y : list A) := match x, y with diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 440b317573..3c0982cde7 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -464,7 +464,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) - Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric A eqA R. Proof with auto. reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. @@ -481,7 +481,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and relation equivalence. *) Program Instance subrelation_partial_order : - ! PartialOrder (relation A) relation_equivalence subrelation. + PartialOrder (@relation_equivalence A) subrelation. Next Obligation. Proof. diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 1701bf4365..40946a8d56 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -48,7 +48,7 @@ Ltac2 @ external make : kind -> constr := "ltac2" "constr_make". Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check". (** Checks that a constr generated by unsafe means is indeed safe in the current environment, and returns it, or the error otherwise. Panics if - not focussed. *) + not focused. *) Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl". (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with @@ -68,6 +68,6 @@ Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "const End Unsafe. Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context". -(** On a focussed goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a - focussed goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is +(** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a + focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is the proof built by the tactic. *) diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v index 8d1fb0cd8a..5e8eef526e 100644 --- a/user-contrib/Ltac2/Pattern.v +++ b/user-contrib/Ltac2/Pattern.v @@ -25,7 +25,7 @@ Ltac2 @ external empty_context : unit -> context := Ltac2 @ external matches : t -> constr -> (ident * constr) list := "ltac2" "pattern_matches". (** If the term matches the pattern, returns the bound variables. If it doesn't, - fail with [Match_failure]. Panics if not focussed. *) + fail with [Match_failure]. Panics if not focused. *) Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) := "ltac2" "pattern_matches_subterm". diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index 1069d0bfa3..2e7dfc42db 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -173,7 +173,7 @@ type strexpr = (** {5 Dynamic semantics} *) -(** Values are represented in a way similar to OCaml, i.e. they constrast +(** Values are represented in a way similar to OCaml, i.e. they contrast immediate integers (integers, constructors without arguments) and structured blocks (tuples, arrays, constructors with arguments), as well as a few other base cases, namely closures, strings, named constructors, and dynamic type diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli index d646b5cda5..829570a354 100644 --- a/user-contrib/Ltac2/tac2intern.mli +++ b/user-contrib/Ltac2/tac2intern.mli @@ -20,7 +20,7 @@ val is_value : glb_tacexpr -> bool val check_unit : ?loc:Loc.t -> type_scheme -> unit val check_subtype : type_scheme -> type_scheme -> bool -(** [check_subtype t1 t2] returns [true] iff all values of intances of type [t1] +(** [check_subtype t1 t2] returns [true] iff all values of instances of type [t1] also have type [t2]. *) val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml index 058d02adde..354a578cb3 100644 --- a/user-contrib/Ltac2/tac2match.ml +++ b/user-contrib/Ltac2/tac2match.ml @@ -88,7 +88,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) diff --git a/vernac/classes.ml b/vernac/classes.ml index 5a7f60584a..ea66234993 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -494,21 +494,8 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate -let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = +let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in - let tclass, ids = - match bk with - | Decl_kinds.Implicit -> - Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false - (fun avoid (clname, _) -> - match clname with - | Some cl -> - let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in - t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - cl - | Explicit -> cl, Id.Set.empty - in let tclass = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass @@ -535,14 +522,13 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl - let new_instance ~pstate ?(global=false) ~program_mode - poly ctx (instid, bk, cl) props + poly instid ctx cl props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ~generalize ctx pl bk cl + interp_instance_context ~program_mode env ~generalize ctx pl cl in let id = match instid with @@ -555,10 +541,10 @@ let new_instance ~pstate ?(global=false) ~program_mode do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props -let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = +let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ctx pl bk cl + interp_instance_context ~program_mode env ctx pl cl in do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid diff --git a/vernac/classes.mli b/vernac/classes.mli index 57bb9ce312..8d5f3e3a06 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -46,28 +46,29 @@ val declare_instance_constant : unit val new_instance : - pstate:Proof_global.t option -> - ?global:bool (** Not global by default. *) -> - program_mode:bool -> - Decl_kinds.polymorphic -> - local_binder_expr list -> - Vernacexpr.typeclass_constraint -> - (bool * constr_expr) option -> - ?generalize:bool -> - ?tac:unit Proofview.tactic -> - ?hook:(GlobRef.t -> unit) -> - Hints.hint_info_expr -> - (* May open a proof *) - Id.t * Proof_global.t option - -val declare_new_instance : - ?global:bool (** Not global by default. *) -> - program_mode:bool -> - Decl_kinds.polymorphic -> - local_binder_expr list -> - ident_decl * Decl_kinds.binding_kind * constr_expr -> - Hints.hint_info_expr -> - unit + pstate:Proof_global.t option + -> ?global:bool (** Not global by default. *) + -> program_mode:bool + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> (bool * constr_expr) option + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t * Proof_global.t option (* May open a proof *) + +val declare_new_instance + : ?global:bool (** Not global by default. *) + -> program_mode:bool + -> Decl_kinds.polymorphic + -> ident_decl + -> local_binder_expr list + -> constr_expr + -> Hints.hint_info_expr + -> unit (** {6 Low level interface used by Add Morphism, do not use } *) val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 6438b48e32..b2db64f74c 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -723,11 +723,11 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> - { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) } + { VernacInstance (fst namesup,snd namesup,t,props,info) } | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> @@ -888,9 +888,9 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info -> - { VernacDeclareInstance (bl, (id, expl, t), info) } + { VernacDeclareInstance (id, bl, t, info) } (* Should be in syntax, but camlp5 would not factorize *) | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f2332bab8b..2e97a169cc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -911,7 +911,7 @@ open Pputils spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (sup, (instid, bk, cl), props, info) -> + | VernacInstance (instid, sup, cl, props, info) -> return ( hov 1 ( keyword "Instance" ++ @@ -920,7 +920,6 @@ open Pputils | { v = Anonymous }, _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++ (match props with | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" @@ -929,13 +928,12 @@ open Pputils | None -> mt())) ) - | VernacDeclareInstance (sup, (instid, bk, cl), info) -> + | VernacDeclareInstance (instid, sup, cl, info) -> return ( hov 1 ( keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info) ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 29b78a5195..b9d1326ba5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1058,18 +1058,18 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance ~atts sup inst props pri = +let vernac_instance ~atts name bl t props pri = let open DefAttributes in let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; + Dumpglob.dump_constraint (fst name) false "inst"; let program_mode = atts.program in - Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri + Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri -let vernac_declare_instance ~atts sup inst pri = +let vernac_declare_instance ~atts id bl inst pri = let open DefAttributes in let global = not (make_section_locality atts.locality) in - Dumpglob.dump_definition (fst (pi1 inst)) false "inst"; - Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri + Dumpglob.dump_definition (fst id) false "inst"; + Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri let vernac_context ~poly l = if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom @@ -2199,7 +2199,7 @@ let with_fail ~st f = try let _ = f () in raise HasNotFailed with | HasNotFailed as e -> raise e - | e -> + | e when CErrors.noncritical e || e = Timeout -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) @@ -2372,10 +2372,10 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = pstate (* Type classes *) - | VernacInstance (sup, inst, props, info) -> - snd @@ with_def_attributes ~atts (vernac_instance ~pstate sup inst props info) - | VernacDeclareInstance (sup, inst, info) -> - with_def_attributes ~atts vernac_declare_instance sup inst info; + | VernacInstance (name, bl, t, props, info) -> + snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info) + | VernacDeclareInstance (id, bl, inst, info) -> + with_def_attributes ~atts vernac_declare_instance id bl inst info; pstate | VernacContext sup -> let () = vernac_context ~poly:(only_polymorphism atts) sup in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 23633e39ab..f946e0596e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -303,15 +303,17 @@ type nonrec vernac_expr = (* Type classes *) | VernacInstance of - local_binder_expr list * (* super *) - typeclass_constraint * (* instance name, class name, params *) - (bool * constr_expr) option * (* props *) - Hints.hint_info_expr + name_decl * (* name *) + local_binder_expr list * (* binders *) + constr_expr * (* type *) + (bool * constr_expr) option * (* body (bool=true when using {}) *) + Hints.hint_info_expr | VernacDeclareInstance of - local_binder_expr list * (* super *) - (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *) - Hints.hint_info_expr + ident_decl * (* name *) + local_binder_expr list * (* binders *) + constr_expr * (* type *) + Hints.hint_info_expr | VernacContext of local_binder_expr list |