diff options
| -rw-r--r-- | .github/CODEOWNERS | 15 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.build | 17 | ||||
| -rw-r--r-- | Makefile.common | 6 | ||||
| -rw-r--r-- | Makefile.doc | 8 | ||||
| -rw-r--r-- | Makefile.make | 2 | ||||
| -rw-r--r-- | Makefile.vofiles | 14 | ||||
| -rw-r--r-- | dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh | 6 | ||||
| -rw-r--r-- | doc/README.md | 2 | ||||
| -rw-r--r-- | doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst | 8 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/11350-list.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 | ||||
| -rw-r--r-- | doc/stdlib/dune | 4 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 180 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 10 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/notations/sphinx.py | 2 | ||||
| -rw-r--r-- | dune | 4 | ||||
| -rw-r--r-- | interp/constrextern.ml | 8 | ||||
| -rw-r--r-- | interp/notation.ml | 28 | ||||
| -rw-r--r-- | interp/notation.mli | 3 | ||||
| -rw-r--r-- | man/coqdep.1 | 30 | ||||
| -rw-r--r-- | man/coqwc.1 | 2 | ||||
| -rw-r--r-- | parsing/extend.ml | 5 | ||||
| -rw-r--r-- | parsing/notgram_ops.ml | 6 | ||||
| -rw-r--r-- | plugins/fourier/plugin_base.dune | 5 | ||||
| -rw-r--r-- | pretyping/cases.ml | 5 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 611 | ||||
| -rw-r--r-- | pretyping/program.ml | 7 | ||||
| -rw-r--r-- | pretyping/program.mli | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9517.v | 19 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9521.v | 23 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9640.v | 23 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 11 | ||||
| -rw-r--r-- | theories/Lists/List.v | 25 | ||||
| -rw-r--r-- | theories/btauto/Algebra.v (renamed from plugins/btauto/Algebra.v) | 0 | ||||
| -rw-r--r-- | theories/btauto/Btauto.v (renamed from plugins/btauto/Btauto.v) | 0 | ||||
| -rw-r--r-- | theories/btauto/Reflect.v (renamed from plugins/btauto/Reflect.v) | 0 | ||||
| -rw-r--r-- | theories/derive/Derive.v (renamed from plugins/derive/Derive.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellBasic.v (renamed from plugins/extraction/ExtrHaskellBasic.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellNatInt.v (renamed from plugins/extraction/ExtrHaskellNatInt.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellNatInteger.v (renamed from plugins/extraction/ExtrHaskellNatInteger.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellNatNum.v (renamed from plugins/extraction/ExtrHaskellNatNum.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellString.v (renamed from plugins/extraction/ExtrHaskellString.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellZInt.v (renamed from plugins/extraction/ExtrHaskellZInt.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellZInteger.v (renamed from plugins/extraction/ExtrHaskellZInteger.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrHaskellZNum.v (renamed from plugins/extraction/ExtrHaskellZNum.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOCamlFloats.v (renamed from plugins/extraction/ExtrOCamlFloats.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOCamlInt63.v (renamed from plugins/extraction/ExtrOCamlInt63.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlBasic.v (renamed from plugins/extraction/ExtrOcamlBasic.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlBigIntConv.v (renamed from plugins/extraction/ExtrOcamlBigIntConv.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlChar.v (renamed from plugins/extraction/ExtrOcamlChar.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlIntConv.v (renamed from plugins/extraction/ExtrOcamlIntConv.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlNatBigInt.v (renamed from plugins/extraction/ExtrOcamlNatBigInt.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlNatInt.v (renamed from plugins/extraction/ExtrOcamlNatInt.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlNativeString.v (renamed from plugins/extraction/ExtrOcamlNativeString.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlString.v (renamed from plugins/extraction/ExtrOcamlString.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlZBigInt.v (renamed from plugins/extraction/ExtrOcamlZBigInt.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlZInt.v (renamed from plugins/extraction/ExtrOcamlZInt.v) | 0 | ||||
| -rw-r--r-- | theories/extraction/Extraction.v (renamed from plugins/extraction/Extraction.v) | 0 | ||||
| -rw-r--r-- | theories/funind/FunInd.v (renamed from plugins/funind/FunInd.v) | 0 | ||||
| -rw-r--r-- | theories/funind/Recdef.v (renamed from plugins/funind/Recdef.v) | 0 | ||||
| -rw-r--r-- | theories/ltac/Ltac.v (renamed from plugins/ltac/Ltac.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/DeclConstant.v (renamed from plugins/micromega/DeclConstant.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Env.v (renamed from plugins/micromega/Env.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/EnvRing.v (renamed from plugins/micromega/EnvRing.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Fourier.v (renamed from plugins/micromega/Fourier.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Fourier_util.v (renamed from plugins/micromega/Fourier_util.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Lia.v (renamed from plugins/micromega/Lia.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Lqa.v (renamed from plugins/micromega/Lqa.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Lra.v (renamed from plugins/micromega/Lra.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/MExtraction.v (renamed from plugins/micromega/MExtraction.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/OrderedRing.v (renamed from plugins/micromega/OrderedRing.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Psatz.v (renamed from plugins/micromega/Psatz.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/QMicromega.v (renamed from plugins/micromega/QMicromega.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/RMicromega.v (renamed from plugins/micromega/RMicromega.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Refl.v (renamed from plugins/micromega/Refl.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/RingMicromega.v (renamed from plugins/micromega/RingMicromega.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Tauto.v (renamed from plugins/micromega/Tauto.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/VarMap.v (renamed from plugins/micromega/VarMap.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/ZCoeff.v (renamed from plugins/micromega/ZCoeff.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/ZMicromega.v (renamed from plugins/micromega/ZMicromega.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Zify.v (renamed from plugins/micromega/Zify.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/ZifyBool.v (renamed from plugins/micromega/ZifyBool.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/ZifyClasses.v (renamed from plugins/micromega/ZifyClasses.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/ZifyComparison.v (renamed from plugins/micromega/ZifyComparison.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/ZifyInst.v (renamed from plugins/micromega/ZifyInst.v) | 0 | ||||
| -rw-r--r-- | theories/micromega/Ztac.v (renamed from plugins/micromega/Ztac.v) | 0 | ||||
| -rw-r--r-- | theories/nsatz/Nsatz.v (renamed from plugins/nsatz/Nsatz.v) | 0 | ||||
| -rw-r--r-- | theories/omega/Omega.v (renamed from plugins/omega/Omega.v) | 0 | ||||
| -rw-r--r-- | theories/omega/OmegaLemmas.v (renamed from plugins/omega/OmegaLemmas.v) | 0 | ||||
| -rw-r--r-- | theories/omega/OmegaPlugin.v (renamed from plugins/omega/OmegaPlugin.v) | 0 | ||||
| -rw-r--r-- | theories/omega/OmegaTactic.v (renamed from plugins/omega/OmegaTactic.v) | 0 | ||||
| -rw-r--r-- | theories/omega/PreOmega.v (renamed from plugins/omega/PreOmega.v) | 0 | ||||
| -rw-r--r-- | theories/rtauto/Bintree.v (renamed from plugins/rtauto/Bintree.v) | 0 | ||||
| -rw-r--r-- | theories/rtauto/Rtauto.v (renamed from plugins/rtauto/Rtauto.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Algebra_syntax.v (renamed from plugins/setoid_ring/Algebra_syntax.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/ArithRing.v (renamed from plugins/setoid_ring/ArithRing.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/BinList.v (renamed from plugins/setoid_ring/BinList.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Cring.v (renamed from plugins/setoid_ring/Cring.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Field.v (renamed from plugins/setoid_ring/Field.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Field_tac.v (renamed from plugins/setoid_ring/Field_tac.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Field_theory.v (renamed from plugins/setoid_ring/Field_theory.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/InitialRing.v (renamed from plugins/setoid_ring/InitialRing.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Integral_domain.v (renamed from plugins/setoid_ring/Integral_domain.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/NArithRing.v (renamed from plugins/setoid_ring/NArithRing.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ncring.v (renamed from plugins/setoid_ring/Ncring.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ncring_initial.v (renamed from plugins/setoid_ring/Ncring_initial.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ncring_polynom.v (renamed from plugins/setoid_ring/Ncring_polynom.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ncring_tac.v (renamed from plugins/setoid_ring/Ncring_tac.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/RealField.v (renamed from plugins/setoid_ring/RealField.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ring.v (renamed from plugins/setoid_ring/Ring.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ring_base.v (renamed from plugins/setoid_ring/Ring_base.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ring_polynom.v (renamed from plugins/setoid_ring/Ring_polynom.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ring_tac.v (renamed from plugins/setoid_ring/Ring_tac.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Ring_theory.v (renamed from plugins/setoid_ring/Ring_theory.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Rings_Q.v (renamed from plugins/setoid_ring/Rings_Q.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Rings_R.v (renamed from plugins/setoid_ring/Rings_R.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/Rings_Z.v (renamed from plugins/setoid_ring/Rings_Z.v) | 0 | ||||
| -rw-r--r-- | theories/setoid_ring/ZArithRing.v (renamed from plugins/setoid_ring/ZArithRing.v) | 0 | ||||
| -rw-r--r-- | theories/ssr/ssrbool.v (renamed from plugins/ssr/ssrbool.v) | 0 | ||||
| -rw-r--r-- | theories/ssr/ssrclasses.v (renamed from plugins/ssr/ssrclasses.v) | 0 | ||||
| -rw-r--r-- | theories/ssr/ssreflect.v (renamed from plugins/ssr/ssreflect.v) | 0 | ||||
| -rw-r--r-- | theories/ssr/ssrfun.v (renamed from plugins/ssr/ssrfun.v) | 0 | ||||
| -rw-r--r-- | theories/ssr/ssrsetoid.v (renamed from plugins/ssr/ssrsetoid.v) | 0 | ||||
| -rw-r--r-- | theories/ssr/ssrunder.v (renamed from plugins/ssr/ssrunder.v) | 0 | ||||
| -rw-r--r-- | theories/ssrmatching/ssrmatching.v (renamed from plugins/ssrmatching/ssrmatching.v) | 0 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 13 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 9 | ||||
| -rw-r--r-- | tools/coqdep.ml | 11 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 152 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 11 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mli | 7 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 83 | ||||
| -rw-r--r-- | tools/dune | 10 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 11 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 19 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 91 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 21 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 81 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 19 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
145 files changed, 821 insertions, 843 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 63d6ccc240..4a126c4e5a 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -121,33 +121,48 @@ ########## Plugins ########## /plugins/btauto/ @coq/btauto-maintainers +/theories/btauto/ @coq/btauto-maintainers /plugins/cc/ @coq/cc-maintainers +/theories/cc/ @coq/cc-maintainers /plugins/derive/ @coq/derive-maintainers +/theories/derive/ @coq/derive-maintainers /plugins/extraction/ @coq/extraction-maintainers +/theories/extraction/ @coq/extraction-maintainers /plugins/firstorder/ @coq/firstorder-maintainers +/theories/firstorder/ @coq/firstorder-maintainers /plugins/funind/ @coq/funind-maintainers +/theories/funind/ @coq/funind-maintainers /plugins/ltac/ @coq/ltac-maintainers +/theories/ltac/ @coq/ltac-maintainers /plugins/micromega/ @coq/micromega-maintainers +/theories/micromega/ @coq/micromega-maintainers /test-suite/micromega/ @coq/micromega-maintainers /plugins/nsatz/ @coq/nsatz-maintainers +/theories/nsatz/ @coq/nsatz-maintainers /plugins/setoid_ring/ @coq/ring-maintainers +/theories/setoid_ring/ @coq/ring-maintainers /plugins/ssrmatching/ @coq/ssreflect-maintainers +/theories/ssrmatching/ @coq/ssreflect-maintainers + /plugins/ssr/ @coq/ssreflect-maintainers +/theories/ssr/ @coq/ssreflect-maintainers + /test-suite/ssr/ @coq/ssreflect-maintainers /plugins/syntax/ @coq/parsing-maintainers /plugins/rtauto/ @coq/rtauto-maintainers +/theories/rtauto/ @coq/rtauto-maintainers /user-contrib/Ltac2 @coq/ltac2-maintainers diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8fd5eb3972..4fdbe6e818 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -258,7 +258,7 @@ build:base: variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" # coqdoc for stdlib, until we know how to build it from installed Coq - EXTRA_TARGET: "stdlib" + EXTRA_TARGET: "doc-stdlib" EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable" # no coqide for 32bit: libgtk installation problems diff --git a/Makefile.build b/Makefile.build index 3c32e5bcc2..8a11d913a9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -809,21 +809,20 @@ $(USERCONTRIBMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter user-contrib/%, $(ML # NB: for make world, no need to mention explicitly the .cmxs of the plugins, # since they are all mentioned in at least one Declare ML Module in some .v -coqlib: theories plugins +coqlib: stdlib-vo contrib-vo ifdef QUICK - $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio' - $(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(PLUGINSVO) + $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio' + $(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(CONTRIBVO) endif -coqlib.timing.diff: theories.timing.diff plugins.timing.diff +coqlib.timing.diff: stdlib.timing.diff -theories: $(THEORIESVO) -plugins: $(PLUGINSVO) +stdlib-vo: $(THEORIESVO) +contrib-vo: $(CONTRIBVO) -theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff) -plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff) +stdlib.timing.diff: $(ALLVO:.$(VO)=.v.timing.diff) -.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff +.PHONY: coqlib stdlib-vo contrib-vo coqlib.timing.diff stdlib.timing.diff # The .vo files in Init are built with the -noinit option diff --git a/Makefile.common b/Makefile.common index 32bf19e99c..780ba717ee 100644 --- a/Makefile.common +++ b/Makefile.common @@ -42,17 +42,17 @@ COQTIME_FILE_MAKER:=tools/TimeFileMaker.py COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py VOTOUR:=bin/votour +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) +OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) # these get installed! TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) $(COQPP) $(VOTOUR) + $(COQWORKMGR) $(COQPP) $(VOTOUR) $(OCAMLLIBDEP) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) COQDEPBOOT:=bin/coqdep_boot$(EXE) COQDEPBOOTBYTE:=bin/coqdep_boot.byte$(EXE) -OCAMLLIBDEP:=bin/ocamllibdep$(EXE) -OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) FAKEIDE:=bin/fake_ide$(EXE) FAKEIDEBYTE:=bin/fake_ide.byte$(EXE) diff --git a/Makefile.doc b/Makefile.doc index 50c4acb416..eb58162cc0 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -56,9 +56,9 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps -.PHONY: stdlib full-stdlib sphinx +.PHONY: doc-stdlib full-stdlib sphinx -doc: refman stdlib +doc: refman doc-stdlib SPHINX_DEPS ?= ifndef QUICK @@ -93,7 +93,7 @@ doc-pdf:\ doc-ps:\ doc/stdlib/Library.ps -stdlib: \ +doc-stdlib: \ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf full-stdlib: \ @@ -129,7 +129,7 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst) # Standard library ###################################################################### -DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 +DOCLIBS=-R theories Coq -Q user-contrib/Ltac2 Ltac2 ### Standard library (browsable html format) diff --git a/Makefile.make b/Makefile.make index e63a578e37..e020ffc5be 100644 --- a/Makefile.make +++ b/Makefile.make @@ -275,7 +275,7 @@ depclean: find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + cacheclean: - find theories plugins test-suite -name '.*.aux' -exec rm -f {} + + find theories test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist diff --git a/Makefile.vofiles b/Makefile.vofiles index fe7ca7c36f..04bc2cf105 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -13,8 +13,8 @@ endif ########################################################################### THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v")) -PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name "*.v")) -ALLVO := $(THEORIESVO) $(PLUGINSVO) +CONTRIBVO := $(patsubst %.v,%.$(VO),$(shell find $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name "*.v")) +ALLVO := $(THEORIESVO) $(CONTRIBVO) VFILES := $(ALLVO:.$(VO)=.v) ## More specific targets @@ -23,17 +23,15 @@ THEORIESLIGHTVO:= \ $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO)) # convert a (stdlib) filename into a module name: -# remove .vo, replace theories and plugins by Coq, and replace slashes by dots -vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))) +# remove .vo, replace stdlib by Coq, and replace slashes by dots +vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(1:.vo=)))) ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo)) - # Converting a stdlib filename into native compiler filenames # Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))) - -vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))) +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(vo:.$(VO)=.cm*))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(vo:.$(VO)=.o))))) ifdef QUICK GLOBFILES:= diff --git a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh new file mode 100644 index 0000000000..87dad61dbc --- /dev/null +++ b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10204" ] || [ "$CI_BRANCH" = "rm-unsafe-type-of-coercion" ]; then + + paramcoq_CI_REF=fix-papp + paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq + +fi diff --git a/doc/README.md b/doc/README.md index ef3ccc2105..7fa6f5cf3d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -96,7 +96,7 @@ Alternatively, you can use some specific targets: - `make refman-{html,pdf}` to produce only one format of the reference manual -- `make stdlib` +- `make doc-stdlib` to produce all formats of the Coq standard library diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst new file mode 100644 index 0000000000..b105928b22 --- /dev/null +++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Bugs in dealing with precedences of notations in custom entries + (`#11530 <https://github.com/coq/coq/pull/11530>`_, + by Hugo Herbelin, fixing in particular + `#9517 <https://github.com/coq/coq/pull/9517>`_, + `#9519 <https://github.com/coq/coq/pull/9519>`_, + `#9521 <https://github.com/coq/coq/pull/9521>`_, + `#11331 <https://github.com/coq/coq/pull/11331>`_). diff --git a/doc/changelog/10-standard-library/11350-list.rst b/doc/changelog/10-standard-library/11350-list.rst new file mode 100644 index 0000000000..52c2517161 --- /dev/null +++ b/doc/changelog/10-standard-library/11350-list.rst @@ -0,0 +1,5 @@ +- **Added:** + ``remove'`` and ``count_occ'`` over lists, + alternatives to ``remove`` and ``count_occ`` based on ``filter`` + (`#11350 <https://github.com/coq/coq/pull/11350>`_, + by Yishuai Li). diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..3d1fc6d4b9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -545,7 +545,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +554,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 36a5916868..2fa4f1fa42 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality: :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), while :n:`and` has a single constructor (:n:`conj`) with multiple parameters (:n:`A` and :n:`B`). - These are defined in theories/Init/Logic.v. The "where" clauses define the + These are defined in ``theories/Init/Logic.v``. The "where" clauses define the infix notation for "or" and "and". .. coqdoc:: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..a8d5ac610f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 828caecabc..093c7a62b2 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,6 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} @@ -17,7 +16,6 @@ (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) @@ -26,7 +24,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index dbc3a42ee9..60d6039b0f 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,90 +1,90 @@ -plugins/btauto/Algebra.v -plugins/btauto/Btauto.v -plugins/btauto/Reflect.v -plugins/derive/Derive.v -plugins/extraction/ExtrHaskellBasic.v -plugins/extraction/ExtrHaskellNatInt.v -plugins/extraction/ExtrHaskellNatInteger.v -plugins/extraction/ExtrHaskellNatNum.v -plugins/extraction/ExtrHaskellString.v -plugins/extraction/ExtrHaskellZInt.v -plugins/extraction/ExtrHaskellZInteger.v -plugins/extraction/ExtrHaskellZNum.v -plugins/extraction/ExtrOcamlBasic.v -plugins/extraction/ExtrOcamlBigIntConv.v -plugins/extraction/ExtrOcamlChar.v -plugins/extraction/ExtrOCamlInt63.v -plugins/extraction/ExtrOCamlFloats.v -plugins/extraction/ExtrOcamlIntConv.v -plugins/extraction/ExtrOcamlNatBigInt.v -plugins/extraction/ExtrOcamlNatInt.v -plugins/extraction/ExtrOcamlString.v -plugins/extraction/ExtrOcamlNativeString.v -plugins/extraction/ExtrOcamlZBigInt.v -plugins/extraction/ExtrOcamlZInt.v -plugins/extraction/Extraction.v -plugins/funind/FunInd.v -plugins/funind/Recdef.v -plugins/ltac/Ltac.v -plugins/micromega/Ztac.v -plugins/micromega/DeclConstant.v -plugins/micromega/Env.v -plugins/micromega/EnvRing.v -plugins/micromega/Fourier.v -plugins/micromega/Fourier_util.v -plugins/micromega/Lia.v -plugins/micromega/Lqa.v -plugins/micromega/Lra.v -plugins/micromega/MExtraction.v -plugins/micromega/OrderedRing.v -plugins/micromega/Psatz.v -plugins/micromega/QMicromega.v -plugins/micromega/RMicromega.v -plugins/micromega/Refl.v -plugins/micromega/RingMicromega.v -plugins/micromega/Tauto.v -plugins/micromega/VarMap.v -plugins/micromega/ZCoeff.v -plugins/micromega/ZMicromega.v -plugins/micromega/ZifyInst.v -plugins/micromega/ZifyBool.v -plugins/micromega/ZifyComparison.v -plugins/micromega/ZifyClasses.v -plugins/micromega/Zify.v -plugins/nsatz/Nsatz.v -plugins/omega/Omega.v -plugins/omega/OmegaLemmas.v -plugins/omega/OmegaPlugin.v -plugins/omega/OmegaTactic.v -plugins/omega/PreOmega.v -plugins/quote/Quote.v -plugins/romega/ROmega.v -plugins/romega/ReflOmegaCore.v -plugins/rtauto/Bintree.v -plugins/rtauto/Rtauto.v -plugins/setoid_ring/Algebra_syntax.v -plugins/setoid_ring/ArithRing.v -plugins/setoid_ring/BinList.v -plugins/setoid_ring/Cring.v -plugins/setoid_ring/Field.v -plugins/setoid_ring/Field_tac.v -plugins/setoid_ring/Field_theory.v -plugins/setoid_ring/InitialRing.v -plugins/setoid_ring/Integral_domain.v -plugins/setoid_ring/NArithRing.v -plugins/setoid_ring/Ncring.v -plugins/setoid_ring/Ncring_initial.v -plugins/setoid_ring/Ncring_polynom.v -plugins/setoid_ring/Ncring_tac.v -plugins/setoid_ring/RealField.v -plugins/setoid_ring/Ring.v -plugins/setoid_ring/Ring_base.v -plugins/setoid_ring/Ring_polynom.v -plugins/setoid_ring/Ring_tac.v -plugins/setoid_ring/Ring_theory.v -plugins/setoid_ring/Rings_Q.v -plugins/setoid_ring/Rings_R.v -plugins/setoid_ring/Rings_Z.v -plugins/setoid_ring/ZArithRing.v -plugins/ssr/ssrunder.v -plugins/ssr/ssrsetoid.v +theories/btauto/Algebra.v +theories/btauto/Btauto.v +theories/btauto/Reflect.v +theories/derive/Derive.v +theories/extraction/ExtrHaskellBasic.v +theories/extraction/ExtrHaskellNatInt.v +theories/extraction/ExtrHaskellNatInteger.v +theories/extraction/ExtrHaskellNatNum.v +theories/extraction/ExtrHaskellString.v +theories/extraction/ExtrHaskellZInt.v +theories/extraction/ExtrHaskellZInteger.v +theories/extraction/ExtrHaskellZNum.v +theories/extraction/ExtrOcamlBasic.v +theories/extraction/ExtrOcamlBigIntConv.v +theories/extraction/ExtrOcamlChar.v +theories/extraction/ExtrOCamlInt63.v +theories/extraction/ExtrOCamlFloats.v +theories/extraction/ExtrOcamlIntConv.v +theories/extraction/ExtrOcamlNatBigInt.v +theories/extraction/ExtrOcamlNatInt.v +theories/extraction/ExtrOcamlString.v +theories/extraction/ExtrOcamlNativeString.v +theories/extraction/ExtrOcamlZBigInt.v +theories/extraction/ExtrOcamlZInt.v +theories/extraction/Extraction.v +theories/funind/FunInd.v +theories/funind/Recdef.v +theories/ltac/Ltac.v +theories/micromega/Ztac.v +theories/micromega/DeclConstant.v +theories/micromega/Env.v +theories/micromega/EnvRing.v +theories/micromega/Fourier.v +theories/micromega/Fourier_util.v +theories/micromega/Lia.v +theories/micromega/Lqa.v +theories/micromega/Lra.v +theories/micromega/MExtraction.v +theories/micromega/OrderedRing.v +theories/micromega/Psatz.v +theories/micromega/QMicromega.v +theories/micromega/RMicromega.v +theories/micromega/Refl.v +theories/micromega/RingMicromega.v +theories/micromega/Tauto.v +theories/micromega/VarMap.v +theories/micromega/ZCoeff.v +theories/micromega/ZMicromega.v +theories/micromega/ZifyInst.v +theories/micromega/ZifyBool.v +theories/micromega/ZifyComparison.v +theories/micromega/ZifyClasses.v +theories/micromega/Zify.v +theories/nsatz/Nsatz.v +theories/omega/Omega.v +theories/omega/OmegaLemmas.v +theories/omega/OmegaPlugin.v +theories/omega/OmegaTactic.v +theories/omega/PreOmega.v +theories/quote/Quote.v +theories/romega/ROmega.v +theories/romega/ReflOmegaCore.v +theories/rtauto/Bintree.v +theories/rtauto/Rtauto.v +theories/setoid_ring/Algebra_syntax.v +theories/setoid_ring/ArithRing.v +theories/setoid_ring/BinList.v +theories/setoid_ring/Cring.v +theories/setoid_ring/Field.v +theories/setoid_ring/Field_tac.v +theories/setoid_ring/Field_theory.v +theories/setoid_ring/InitialRing.v +theories/setoid_ring/Integral_domain.v +theories/setoid_ring/NArithRing.v +theories/setoid_ring/Ncring.v +theories/setoid_ring/Ncring_initial.v +theories/setoid_ring/Ncring_polynom.v +theories/setoid_ring/Ncring_tac.v +theories/setoid_ring/RealField.v +theories/setoid_ring/Ring.v +theories/setoid_ring/Ring_base.v +theories/setoid_ring/Ring_polynom.v +theories/setoid_ring/Ring_tac.v +theories/setoid_ring/Ring_theory.v +theories/setoid_ring/Rings_Q.v +theories/setoid_ring/Rings_R.v +theories/setoid_ring/Rings_Z.v +theories/setoid_ring/ZArithRing.v +theories/ssr/ssrunder.v +theories/ssr/ssrsetoid.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b2ddf36b65..51688e2d9e 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -619,11 +619,11 @@ through the <tt>Require Import</tt> command.</p> small scale reflection formalization technique </dt> <dd> - plugins/ssrmatching/ssrmatching.v - plugins/ssr/ssrclasses.v - plugins/ssr/ssreflect.v - plugins/ssr/ssrbool.v - plugins/ssr/ssrfun.v + theories/ssrmatching/ssrmatching.v + theories/ssr/ssrclasses.v + theories/ssr/ssreflect.v + theories/ssr/ssrbool.v + theories/ssr/ssrfun.v </dd> <dt> <b>Ltac2</b>: diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 732f15b78a..a51308f153 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,7 +8,7 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do if [[ $k =~ "user-contrib" ]]; then diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index ab18d136b8..5659a64b84 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): while atom != "": if atom[0] == "'": node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex") + node += nodes.raw("'", "'", format="html") atom = atom[1:] elif atom[0] == "`": node += nodes.raw("\\`{}", "\\`{}", format="latex") + node += nodes.raw("`", "`", format="html") atom = atom[1:] else: index_ap = atom.find("'") @@ -27,9 +27,9 @@ (source_tree user-contrib)) (action (with-stdout-to .vfiles.d - (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ + (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \ - `find theories plugins user-contrib -type f -name *.v`")))) + `find theories user-contrib -type f -name *.v`")))) (alias (name vodeps) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c198c4eb9b..06232b8e1a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -792,9 +792,11 @@ let rec flatten_application c = match DAst.get c with let extern_possible_prim_token (custom,scopes) r = let (sc,n) = uninterp_prim_token r in - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> + let coercion = + if entry_has_prim_token n custom then [] else + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> coercion in match availability_of_prim_token n sc scopes with | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) diff --git a/interp/notation.ml b/interp/notation.ml index 93969f3718..9d6cab550d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1349,6 +1349,34 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false +let entry_has_numeral_map = ref String.Map.empty +let entry_has_string_map = ref String.Map.empty + +let declare_custom_entry_has_numeral s n = + try + let p = String.Map.find s !entry_has_numeral_map in + user_err (str "Custom entry " ++ str s ++ + str " has already a rule for numerals at level " ++ int p ++ str ".") + with Not_found -> + entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map + +let declare_custom_entry_has_string s n = + try + let p = String.Map.find s !entry_has_string_map in + user_err (str "Custom entry " ++ str s ++ + str " has already a rule for strings at level " ++ int p ++ str ".") + with Not_found -> + entry_has_string_map := String.Map.add s n !entry_has_string_map + +let entry_has_prim_token prim = function + | InConstrEntrySomeLevel -> true + | InCustomEntryLevel (s,n) -> + match prim with + | Numeral _ -> + (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false) + | String _ -> + (try String.Map.find s !entry_has_string_map <= n with Not_found -> false) + let uninterp_prim_token c = match glob_prim_constr_key c with | None -> raise Notation_ops.No_match diff --git a/interp/notation.mli b/interp/notation.mli index ea5125f7ec..707be6cb87 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -305,9 +305,12 @@ val availability_of_entry_coercion : notation_entry_level -> notation_entry_leve val declare_custom_entry_has_global : string -> int -> unit val declare_custom_entry_has_ident : string -> int -> unit +val declare_custom_entry_has_numeral : string -> int -> unit +val declare_custom_entry_has_string : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool +val entry_has_prim_token : prim_token -> notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) diff --git a/man/coqdep.1 b/man/coqdep.1 index 4223482c99..0770ce88c8 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -12,9 +12,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .BI \-coqlib \ directory ] [ -.BI \-c -] -[ .BI \-i ] [ @@ -52,10 +49,6 @@ directives and the dot notation .SH OPTIONS .TP -.BI \-c -Prints the dependencies of Caml modules. -(On Caml modules, the behaviour is exactly the same as ocamldep). -.TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. .TP @@ -152,29 +145,8 @@ example% coqdep \-I . *.v .fi .RE .br -.ne 7 -.LP -To get only the Caml dependencies: -.IP -.B -example% coqdep \-c \-I . *.ml -.RS -.sp .5 -.nf -.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo -.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx -.B C.cmo: C.ml -.B C.cmx: C.ml -.B B.cmo: B.ml -.B B.cmx: B.ml -.B A.cmo: A.ml -.B A.cmx: A.ml -.fi -.RE -.br -.ne 7 .SH BUGS Please report any bug to -.B coq\-bugs@pauillac.inria.fr +.B https://github.com/coq/coq/issues diff --git a/man/coqwc.1 b/man/coqwc.1 index 4594aeecb7..eee37f3d1f 100644 --- a/man/coqwc.1 +++ b/man/coqwc.1 @@ -44,4 +44,4 @@ Do not skip headers .SH BUGS Please report any bug to -.B coq\-bugs@pauillac.inria.fr +.B https://github.com/coq/coq/issues diff --git a/parsing/extend.ml b/parsing/extend.ml index dcdaa25c33..178f7354f2 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -21,6 +21,7 @@ type production_position = type production_level = | NextLevel | NumLevel of int + | DefaultLevel (** Interpreted differently at the border or inside a rule *) (** User-level types used to tell how to parse or interpret of the non-terminal *) @@ -28,6 +29,7 @@ type 'a constr_entry_key_gen = | ETIdent | ETGlobal | ETBigint + | ETString | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) @@ -40,7 +42,7 @@ type constr_entry_key = (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = - production_level option constr_entry_key_gen + production_level constr_entry_key_gen (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) @@ -52,6 +54,7 @@ type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdString (* Parsed as a string *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *) diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 009dafdb13..5c220abeda 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -48,17 +48,19 @@ let production_position_eq pp1 pp2 = match (pp1,pp2) with let production_level_eq l1 l2 = match (l1,l2) with | NextLevel, NextLevel -> true | NumLevel n1, NumLevel n2 -> Int.equal n1 n2 -| (NextLevel | NumLevel _), _ -> false +| DefaultLevel, DefaultLevel -> true +| (NextLevel | NumLevel _ | DefaultLevel), _ -> false let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETIdent, ETIdent -> true | ETGlobal, ETGlobal -> true | ETBigint, ETBigint -> true +| ETString, ETString -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) -> notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false +| (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in diff --git a/plugins/fourier/plugin_base.dune b/plugins/fourier/plugin_base.dune deleted file mode 100644 index 8cc76f6f9e..0000000000 --- a/plugins/fourier/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name fourier_plugin) - (public_name coq.plugins.fourier) - (synopsis "Coq's fourier plugin") - (libraries coq.plugins.ltac)) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 29d6726262..abc16f621e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2126,11 +2126,6 @@ let eq_id avoid id = let hid' = next_ident_away hid avoid in hid' -let papp sigma gr args = - let evdref = ref sigma in - let ans = papp evdref gr args in - !evdref, ans - let mk_eq sigma typ x y = papp sigma coq_eq_ind [| typ; x ; y |] let mk_eq_refl sigma typ x = papp sigma coq_eq_refl [| typ; x |] let mk_JMeq sigma typ x typ' y = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c4aa3479bf..62bc27cd3c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -92,19 +92,23 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 = open Program -let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env sigma c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define opaque; Evar_kinds.qm_name=na; }) in - let evd, v = Evarutil.new_evar env !evdref ~src c in - let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in - evdref := evd; - v - -let app_opt env evdref f t = - whd_betaiota !evdref (app_opt f t) + let sigma, v = Evarutil.new_evar env sigma ~src c in + let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma v)) in + sigma, v + +let app_opt env sigma f t = + let sigma, t = + match f with + | None -> sigma, t + | Some f -> f sigma t + in + sigma, whd_betaiota sigma t let pair_of_array a = (a.(0), a.(1)) @@ -125,8 +129,8 @@ let disc_subset sigma x = exception NoSubtacCoercion -let hnf env evd c = whd_all env evd c -let hnf_nodelta env evd c = whd_betaiota evd c +let hnf env sigma c = whd_all env sigma c +let hnf_nodelta env sigma c = whd_betaiota sigma c let lift_args n sign = let rec liftrec k = function @@ -135,222 +139,219 @@ let lift_args n sign = in liftrec (List.length sign) sign -let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) - : (EConstr.constr -> EConstr.constr) option - = +let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr) + : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.constr) option + = let open Context.Rel.Declaration in - let rec coerce_unify env x y = - let x = hnf env !evdref x and y = hnf env !evdref y in - try - evdref := Evarconv.unify_leq_delay env !evdref x y; - None - with UnableToUnify _ -> coerce' env x y - and coerce' env x y : (EConstr.constr -> EConstr.constr) option = - let subco () = subset_coerce env evdref x y in + let rec coerce_unify env sigma x y = + let x = hnf env sigma x and y = hnf env sigma y in + try + (Evarconv.unify_leq_delay env sigma x y, None) + with UnableToUnify _ -> coerce' env sigma x y + and coerce' env sigma x y : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.constr) option = + let subco sigma = subset_coerce env sigma x y in let dest_prod c = - match Reductionops.splay_prod_n env (!evdref) 1 c with + match Reductionops.splay_prod_n env sigma 1 c with | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, t), c | _ -> raise NoSubtacCoercion in - let coerce_application typ typ' c c' l l' = + let coerce_application sigma typ typ' c c' l l' = let len = Array.length l in - let rec aux tele typ typ' i co = + let rec aux sigma tele typ typ' i co = if i < len then let hdx = l.(i) and hdy = l'.(i) in - try evdref := unify_leq_delay env !evdref hdx hdy; - let (n, eqT), restT = dest_prod typ in - let (n', eqT'), restT' = dest_prod typ' in - aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co - with UnableToUnify _ -> - let (n, eqT), restT = dest_prod typ in - let (n', eqT'), restT' = dest_prod typ' in - let () = - try evdref := unify_leq_delay env !evdref eqT eqT' - with UnableToUnify _ -> raise NoSubtacCoercion - in - (* Disallow equalities on arities *) - if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion; - let restargs = lift_args 1 - (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) - in - let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in - let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in - let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential ?loc n.binder_name env evdref eq in - let eq_app x = papp evdref coq_eq_rect - [| eqT; hdx; pred; x; hdy; evar|] - in - aux (hdy :: tele) (subst1 hdx restT) - (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) - else Some (fun x -> - let term = co x in - let sigma, term = Typing.solve_evars env !evdref term in - evdref := sigma; term) + try + let sigma = unify_leq_delay env sigma hdx hdy in + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in + aux sigma (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co + with UnableToUnify _ -> + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in + let sigma = + try + unify_leq_delay env sigma eqT eqT' + with UnableToUnify _ -> raise NoSubtacCoercion + in + (* Disallow equalities on arities *) + if Reductionops.is_arity env sigma eqT then raise NoSubtacCoercion; + let restargs = lift_args 1 + (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) + in + let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in + let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in + let sigma, eq = papp sigma coq_eq_ind [| eqT; hdx; hdy |] in + let sigma, evar = make_existential ?loc n.binder_name env sigma eq in + let eq_app sigma x = papp sigma coq_eq_rect + [| eqT; hdx; pred; x; hdy; evar|] + in + aux sigma (hdy :: tele) (subst1 hdx restT) + (subst1 hdy restT') (succ i) (fun sigma x -> let sigma, x = co sigma x in eq_app sigma x) + else + sigma, Some (fun sigma x -> + let sigma, term = co sigma x in + let sigma, term = Typing.solve_evars env sigma term in + sigma, term) in - if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then - (* Second-order unification needed. *) - raise NoSubtacCoercion; - aux [] typ typ' 0 (fun x -> x) + if isEvar sigma c || isEvar sigma c' || not (Program.is_program_generalized_coercion ()) then + (* Second-order unification needed. *) + raise NoSubtacCoercion; + aux sigma [] typ typ' 0 (fun sigma x -> sigma, x) in - match (EConstr.kind !evdref x, EConstr.kind !evdref y) with - | Sort s, Sort s' -> - (match ESorts.kind !evdref s, ESorts.kind !evdref s' with - | Prop, Prop | Set, Set -> None - | (Prop | Set), Type _ -> None - | Type x, Type y when Univ.Universe.equal x y -> None (* false *) - | _ -> subco ()) - | Prod (name, a, b), Prod (name', a', b') -> - let name' = - {name' with - binder_name = - Name (Namegen.next_ident_away - Namegen.default_dependent_ident (Termops.vars_of_env env))} - in - let env' = push_rel (LocalAssum (name', a')) env in - let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in - (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) - let coec1 = app_opt env' evdref c1 (mkRel 1) in - (* env, x : a' |- c1[x] : lift 1 a *) - let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in - (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) - (match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun f -> - mkLambda (name', a', - app_opt env' evdref c2 - (mkApp (lift 1 f, [| coec1 |]))))) - - | App (c, l), App (c', l') -> - (match EConstr.kind !evdref c, EConstr.kind !evdref c' with - Ind (i, u), Ind (i', u') -> (* Inductive types *) - let len = Array.length l in - let sigT = delayed_force sigT_typ in - let prod = delayed_force prod_typ in - (* Sigma types *) - if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i' - && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod)) - then - if eq_ind i (destIndRef sigT) - then - begin - let (a, pb), (a', pb') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let remove_head a c = - match EConstr.kind !evdref c with - | Lambda (n, t, t') -> c, t' - | Evar (k, args) -> - let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in - evdref := evs; - let (n, dom, rng) = destLambda !evdref t in - if isEvar !evdref dom then - let (domk, args) = destEvar !evdref dom in - evdref := define domk a !evdref; - else (); - t, rng - | _ -> raise NoSubtacCoercion - in - let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let ra = Retyping.relevance_of_type env !evdref a in - let env' = push_rel - (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a)) - env - in - let c2 = coerce_unify env' b b' in - match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt env' evdref c1 (papp evdref sigT_proj1 - [| a; pb; x |]), - app_opt env' evdref c2 (papp evdref sigT_proj2 - [| a; pb; x |]) - in - papp evdref sigT_intro [| a'; pb'; x ; y |]) - end - else - begin - let (a, b), (a', b') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let c2 = coerce_unify env b b' in - match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt env evdref c1 (papp evdref prod_proj1 - [| a; b; x |]), - app_opt env evdref c2 (papp evdref prod_proj2 - [| a; b; x |]) - in - papp evdref prod_intro [| a'; b'; x ; y |]) - end - else - if eq_ind i i' && Int.equal len (Array.length l') then - let evm = !evdref in - (try subco () - with NoSubtacCoercion -> - let typ = Typing.unsafe_type_of env evm c in - let typ' = Typing.unsafe_type_of env evm c' in - coerce_application typ typ' c c' l l') - else - subco () - | x, y when EConstr.eq_constr !evdref c c' -> - if Int.equal (Array.length l) (Array.length l') then - let evm = !evdref in - let lam_type = Typing.unsafe_type_of env evm c in - let lam_type' = Typing.unsafe_type_of env evm c' in - coerce_application lam_type lam_type' c c' l l' - else subco () - | _ -> subco ()) - | _, _ -> subco () - - and subset_coerce env evdref x y = - match disc_subset !evdref x with - Some (u, p) -> - let c = coerce_unify env u y in - let f x = - app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |]) - in Some f + match (EConstr.kind sigma x, EConstr.kind sigma y) with + | Sort s, Sort s' -> + (match ESorts.kind sigma s, ESorts.kind sigma s' with + | Prop, Prop | Set, Set -> sigma, None + | (Prop | Set), Type _ -> sigma, None + | Type x, Type y when Univ.Universe.equal x y -> sigma, None (* false *) + | _ -> subco sigma) + | Prod (name, a, b), Prod (name', a', b') -> + let name' = + {name' with + binder_name = + Name (Namegen.next_ident_away + Namegen.default_dependent_ident (Termops.vars_of_env env))} + in + let env' = push_rel (LocalAssum (name', a')) env in + let sigma, c1 = coerce_unify env' sigma (lift 1 a') (lift 1 a) in + (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) + let sigma, coec1 = app_opt env' sigma c1 (mkRel 1) in + (* env, x : a' |- c1[x] : lift 1 a *) + let sigma, c2 = coerce_unify env' sigma (subst1 coec1 (liftn 1 2 b)) b' in + (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) + (match c1, c2 with + | None, None -> sigma, None + | _, _ -> + sigma, + Some (fun sigma f -> + let sigma, t = app_opt env' sigma c2 + (mkApp (lift 1 f, [| coec1 |])) in + sigma, mkLambda (name', a', t))) + + | App (c, l), App (c', l') -> + (match EConstr.kind sigma c, EConstr.kind sigma c' with + Ind (i, u), Ind (i', u') -> (* Inductive types *) + let len = Array.length l in + let sigT = delayed_force sigT_typ in + let prod = delayed_force prod_typ in + (* Sigma types *) + if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i' + && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod)) + then + if eq_ind i (destIndRef sigT) + then + begin + let (a, pb), (a', pb') = + pair_of_array l, pair_of_array l' + in + let sigma, c1 = coerce_unify env sigma a a' in + let remove_head sigma a c = + match EConstr.kind sigma c with + | Lambda (n, t, t') -> sigma, (c, t') + | Evar (k, args) -> + let (sigma, t) = Evardefine.define_evar_as_lambda env sigma (k,args) in + let (n, dom, rng) = destLambda sigma t in + let sigma = + if isEvar sigma dom then + let (domk, args) = destEvar sigma dom in + define domk a sigma + else sigma + in + sigma, (t, rng) + | _ -> raise NoSubtacCoercion + in + let sigma, (pb, b) = remove_head sigma a pb in + let sigma, (pb', b') = remove_head sigma a' pb' in + let ra = Retyping.relevance_of_type env sigma a in + let env' = push_rel + (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a)) + env + in + let sigma, c2 = coerce_unify env' sigma b b' in + match c1, c2 with + | None, None -> sigma, None + | _, _ -> + sigma, + Some (fun sigma x -> + let sigma, t1 = papp sigma sigT_proj1 [| a; pb; x |] in + let sigma, t2 = papp sigma sigT_proj2 [| a; pb; x |] in + let sigma, x = app_opt env' sigma c1 t1 in + let sigma, y = app_opt env' sigma c2 t2 in + papp sigma sigT_intro [| a'; pb'; x ; y |]) + end + else + begin + let (a, b), (a', b') = + pair_of_array l, pair_of_array l' + in + let sigma, c1 = coerce_unify env sigma a a' in + let sigma, c2 = coerce_unify env sigma b b' in + match c1, c2 with + | None, None -> sigma, None + | _, _ -> + sigma, + Some (fun sigma x -> + let sigma, t1 = papp sigma prod_proj1 [| a; b; x |] in + let sigma, t2 = papp sigma prod_proj2 [| a; b; x |] in + let sigma, x = app_opt env sigma c1 t1 in + let sigma, y = app_opt env sigma c2 t2 in + papp sigma prod_intro [| a'; b'; x ; y |]) + end + else + if eq_ind i i' && Int.equal len (Array.length l') then + (try subco sigma + with NoSubtacCoercion -> + let sigma, typ = Typing.type_of env sigma c in + let sigma, typ' = Typing.type_of env sigma c' in + coerce_application sigma typ typ' c c' l l') + else + subco sigma + | x, y when EConstr.eq_constr sigma c c' -> + if Int.equal (Array.length l) (Array.length l') then + let sigma, lam_type = Typing.type_of env sigma c in + let sigma, lam_type' = Typing.type_of env sigma c' in + coerce_application sigma lam_type lam_type' c c' l l' + else subco sigma + | _ -> subco sigma) + | _, _ -> subco sigma + + and subset_coerce env sigma x y = + match disc_subset sigma x with + Some (u, p) -> + let sigma, c = coerce_unify env sigma u y in + let f sigma x = + let sigma, t = papp sigma sig_proj1 [| u; p; x |] in + app_opt env sigma c t + in sigma, Some f | None -> - match disc_subset !evdref y with + match disc_subset sigma y with Some (u, p) -> - let c = coerce_unify env x u in - Some - (fun x -> - let cx = app_opt env evdref c x in - let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |])) - in - (papp evdref sig_intro [| u; p; cx; evar |])) - | None -> - raise NoSubtacCoercion - in coerce_unify env x y - -let app_coercion env evdref coercion v = + let sigma, c = coerce_unify env sigma x u in + sigma, Some + (fun sigma x -> + let sigma, cx = app_opt env sigma c x in + let sigma, evar = make_existential ?loc Anonymous env sigma (mkApp (p, [| cx |])) + in + (papp sigma sig_intro [| u; p; cx; evar |])) + | None -> + raise NoSubtacCoercion + in coerce_unify env sigma x y + +let app_coercion env sigma coercion v = match coercion with - | None -> v + | None -> sigma, v | Some f -> - let sigma, v' = Typing.solve_evars env !evdref (f v) in - evdref := sigma; - whd_betaiota !evdref v' + let sigma, v' = f sigma v in + let sigma, v' = Typing.solve_evars env sigma v' in + sigma, whd_betaiota sigma v' -let coerce_itf ?loc env evd v t c1 = - let evdref = ref evd in - let coercion = coerce ?loc env evdref t c1 in - let t = app_coercion env evdref coercion v in - !evdref, t +let coerce_itf ?loc env sigma v t c1 = + let sigma, coercion = coerce ?loc env sigma t c1 in + app_coercion env sigma coercion v -let saturate_evd env evd = +let saturate_evd env sigma = Typeclasses.resolve_typeclasses - ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd + ~filter:Typeclasses.no_goals ~split:true ~fail:false env sigma type coercion_trace = | IdCoe @@ -388,7 +389,7 @@ let rec reapply_coercions sigma trace c = match trace with (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = - let j,t,trace,evd = + let j,t,trace,sigma = List.fold_left (fun (ja,typ_cl,trace,sigma) i -> let isid = i.coe_is_identity in @@ -415,129 +416,126 @@ let apply_coercion env sigma p hj typ_cl = in jres, jres.uj_type, trace, sigma) (hj,typ_cl,IdCoe,sigma) p - in evd, j, trace + in sigma, j, trace -let mu env evdref t = +let mu env sigma t = let rec aux v = - let v' = hnf env !evdref v in - match disc_subset !evdref v' with + let v' = hnf env sigma v in + match disc_subset sigma v' with | Some (u, p) -> - let f, ct, trace = aux u in - let p = hnf_nodelta env !evdref p in + let sigma, (f, ct, trace) = aux u in + let p = hnf_nodelta env sigma p in let p1 = delayed_force sig_proj1 in - let evd, p1 = Evarutil.new_global !evdref p1 in - evdref := evd; - (Some (fun x -> - app_opt env evdref + let sigma, p1 = Evarutil.new_global sigma p1 in + sigma, + (Some (fun sigma x -> + app_opt env sigma f (mkApp (p1, [| u; p; x |]))), ct, Coe {head=p1; args=[u;p]; previous=trace}) - | None -> (None, v, IdCoe) + | None -> sigma, (None, v, IdCoe) in aux t (* Try to coerce to a funclass; raise NoCoercion if not possible *) -let inh_app_fun_core ~program_mode env evd j = - let t = whd_all env evd j.uj_type in - match EConstr.kind evd t with - | Prod _ -> (evd,j,IdCoe) +let inh_app_fun_core ~program_mode env sigma j = + let t = whd_all env sigma j.uj_type in + match EConstr.kind sigma t with + | Prod _ -> (sigma,j,IdCoe) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product env evd ev in - (evd',{ uj_val = j.uj_val; uj_type = t },IdCoe) + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in + (sigma,{ uj_val = j.uj_val; uj_type = t },IdCoe) | _ -> try let t,p = - lookup_path_to_fun_from env evd j.uj_type in - apply_coercion env evd p j t + lookup_path_to_fun_from env sigma j.uj_type in + apply_coercion env sigma p j t with Not_found | NoCoercion -> if program_mode then try - let evdref = ref evd in - let coercef, t, trace = mu env evdref t in - let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in - (!evdref, res, trace) + let sigma, (coercef, t, trace) = mu env sigma t in + let sigma, uj_val = app_opt env sigma coercef j.uj_val in + let res = { uj_val ; uj_type = t } in + (sigma, res, trace) with NoSubtacCoercion | NoCoercion -> - (evd,j,IdCoe) + (sigma,j,IdCoe) else raise NoCoercion (* Try to coerce to a funclass; returns [j] if no coercion is applicable *) -let inh_app_fun ~program_mode resolve_tc env evd j = - try inh_app_fun_core ~program_mode env evd j +let inh_app_fun ~program_mode resolve_tc env sigma j = + try inh_app_fun_core ~program_mode env sigma j with | NoCoercion when not resolve_tc - || not (get_use_typeclasses_for_conversion ()) -> (evd, j, IdCoe) + || not (get_use_typeclasses_for_conversion ()) -> (sigma, j, IdCoe) | NoCoercion -> - try inh_app_fun_core ~program_mode env (saturate_evd env evd) j - with NoCoercion -> (evd, j, IdCoe) + try inh_app_fun_core ~program_mode env (saturate_evd env sigma) j + with NoCoercion -> (sigma, j, IdCoe) let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | _ -> error_not_a_type env sigma j -let inh_tosort_force ?loc env evd j = +let inh_tosort_force ?loc env sigma j = try - let t,p = lookup_path_to_sort_from env evd j.uj_type in - let evd,j1,_trace = apply_coercion env evd p j t in - let j2 = Environ.on_judgment_type (whd_evar evd) j1 in - (evd,type_judgment env evd j2) + let t,p = lookup_path_to_sort_from env sigma j.uj_type in + let sigma,j1,_trace = apply_coercion env sigma p j t in + let j2 = Environ.on_judgment_type (whd_evar sigma) j1 in + (sigma,type_judgment env sigma j2) with Not_found | NoCoercion -> - error_not_a_type ?loc env evd j + error_not_a_type ?loc env sigma j -let inh_coerce_to_sort ?loc env evd j = - let typ = whd_all env evd j.uj_type in - match EConstr.kind evd typ with - | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s }) +let inh_coerce_to_sort ?loc env sigma j = + let typ = whd_all env sigma j.uj_type in + match EConstr.kind sigma typ with + | Sort s -> (sigma,{ utj_val = j.uj_val; utj_type = ESorts.kind sigma s }) | Evar ev -> - let (evd',s) = Evardefine.define_evar_as_sort env evd ev in - (evd',{ utj_val = j.uj_val; utj_type = s }) + let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in + (sigma,{ utj_val = j.uj_val; utj_type = s }) | _ -> - inh_tosort_force ?loc env evd j + inh_tosort_force ?loc env sigma j -let inh_coerce_to_base ?loc ~program_mode env evd j = +let inh_coerce_to_base ?loc ~program_mode env sigma j = if program_mode then - let evdref = ref evd in - let ct, typ', trace = mu env evdref j.uj_type in - let res = - { uj_val = (app_coercion env evdref ct j.uj_val); - uj_type = typ' } - in !evdref, res - else (evd, j) - -let inh_coerce_to_prod ?loc ~program_mode env evd t = + let sigma, (ct, typ', _trace) = mu env sigma j.uj_type in + let sigma, uj_val = app_coercion env sigma ct j.uj_val in + let res = { uj_val; uj_type = typ' } in + sigma, res + else (sigma, j) + +let inh_coerce_to_prod ?loc ~program_mode env sigma t = if program_mode then - let evdref = ref evd in - let _, typ', _trace = mu env evdref t in - !evdref, typ' - else (evd, t) + let sigma, (_, typ', _trace) = mu env sigma t in + sigma, typ' + else (sigma, t) -let inh_coerce_to_fail flags env evd rigidonly v t c1 = +let inh_coerce_to_fail flags env sigma rigidonly v t c1 = if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr c1) && Heads.is_rigid env (EConstr.Unsafe.to_constr t)) then raise NoCoercion else - let evd, v', t', trace = + let sigma, v', t', trace = try - let t2,t1,p = lookup_path_between env evd (t,c1) in - let evd,j,trace = - apply_coercion env evd p + let t2,t1,p = lookup_path_between env sigma (t,c1) in + let sigma,j,trace = + apply_coercion env sigma p {uj_val = v; uj_type = t} t2 in - evd, j.uj_val, j.uj_type, trace + sigma, j.uj_val, j.uj_type, trace with Not_found -> raise NoCoercion in - try (unify_leq_delay ~flags env evd t' c1, v', trace) + try (unify_leq_delay ~flags env sigma t' c1, v', trace) with UnableToUnify _ -> raise NoCoercion let default_flags_of env = default_flags_of TransparentState.full -let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = - try (unify_leq_delay ~flags env evd t c1, v, IdCoe) - with UnableToUnify (best_failed_evd,e) -> - try inh_coerce_to_fail flags env evd rigidonly v t c1 +let rec inh_conv_coerce_to_fail ?loc env sigma ?(flags=default_flags_of env) rigidonly v t c1 = + try (unify_leq_delay ~flags env sigma t c1, v, IdCoe) + with UnableToUnify (best_failed_sigma,e) -> + try inh_coerce_to_fail flags env sigma rigidonly v t c1 with NoCoercion -> match - EConstr.kind evd (whd_all env evd t), - EConstr.kind evd (whd_all env evd c1) + EConstr.kind sigma (whd_all env sigma t), + EConstr.kind sigma (whd_all env sigma c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) @@ -551,45 +549,46 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid | na -> na) name in let open Context.Rel.Declaration in let env1 = push_rel (LocalAssum (name,u1)) env in - let (evd', v1, trace1) = - inh_conv_coerce_to_fail ?loc env1 evd rigidonly + let (sigma, v1, trace1) = + inh_conv_coerce_to_fail ?loc env1 sigma rigidonly (mkRel 1) (lift 1 u1) (lift 1 t1) in - let v2 = beta_applist evd' (lift 1 v,[v1]) in - let t2 = Retyping.get_type_of env1 evd' v2 in - let (evd'',v2',trace2) = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in + let v2 = beta_applist sigma (lift 1 v,[v1]) in + let t2 = Retyping.get_type_of env1 sigma v2 in + let (sigma,v2',trace2) = inh_conv_coerce_to_fail ?loc env1 sigma rigidonly v2 t2 u2 in let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in - (evd'', mkLambda (name, u1, v2'), trace) - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + (sigma, mkLambda (name, u1, v2'), trace) + | _ -> raise (NoCoercionNoUnifier (best_failed_sigma,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = - let (evd', val', otrace) = +let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env sigma cj t = + let (sigma, val', otrace) = try - let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t in - (evd', val', Some trace) - with NoCoercionNoUnifier (best_failed_evd,e) -> + let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma ~flags rigidonly cj.uj_val cj.uj_type t in + (sigma, val', Some trace) + with NoCoercionNoUnifier (best_failed_sigma,e) -> try if program_mode then - let (evd', val') = coerce_itf ?loc env evd cj.uj_val cj.uj_type t in - (evd', val', None) + let (sigma, val') = coerce_itf ?loc env sigma cj.uj_val cj.uj_type t in + (sigma, val', None) else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> - error_actual_type ?loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_sigma cj t e | NoSubtacCoercion -> - let evd' = saturate_evd env evd in + let sigma' = saturate_evd env sigma in try - if evd' == evd then - error_actual_type ?loc env best_failed_evd cj t e + if sigma' == sigma then + error_actual_type ?loc env best_failed_sigma cj t e else - let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t in - (evd', val', Some trace) - with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type ?loc env best_failed_evd cj t e + let sigma = sigma' in + let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma rigidonly cj.uj_val cj.uj_type t in + (sigma, val', Some trace) + with NoCoercionNoUnifier (_sigma,_error) -> + error_actual_type ?loc env best_failed_sigma cj t e in - (evd',{ uj_val = val'; uj_type = t },otrace) + (sigma,{ uj_val = val'; uj_type = t },otrace) -let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = - inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd -let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = - inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env evd +let inh_conv_coerce_to ?loc ~program_mode resolve_tc env sigma ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env sigma +let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env sigma ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env sigma diff --git a/pretyping/program.ml b/pretyping/program.ml index 9c478844aa..909ba6e44a 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,12 +11,11 @@ open CErrors open Util -let papp evdref r args = +let papp sigma r args = let open EConstr in let gr = delayed_force r in - let evd, hd = Evarutil.new_global !evdref gr in - evdref := evd; - mkApp (hd, args) + let evd, hd = Evarutil.new_global sigma gr in + sigma, mkApp (hd, args) let sig_typ () = Coqlib.lib_ref "core.sig.type" let sig_intro () = Coqlib.lib_ref "core.sig.intro" diff --git a/pretyping/program.mli b/pretyping/program.mli index 6604b3a854..7da0da1297 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -10,6 +10,7 @@ open Names open EConstr +open Evd (** A bunch of Coq constants used by Program *) @@ -38,7 +39,7 @@ val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) -val papp : Evd.evar_map ref -> (unit -> GlobRef.t) -> constr array -> constr +val papp : evar_map -> (unit -> GlobRef.t) -> constr array -> evar_map * constr val get_proofs_transparency : unit -> bool val is_program_cases : unit -> bool diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v new file mode 100644 index 0000000000..bb43edbe74 --- /dev/null +++ b/test-suite/bugs/closed/bug_9517.v @@ -0,0 +1,19 @@ +Declare Custom Entry expr. +Declare Custom Entry stmt. +Notation "x" := x (in custom stmt, x ident). +Notation "x" := x (in custom expr, x ident). + +Notation "1" := 1 (in custom expr). + +Notation "! x = y !" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr). +Notation "? x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr). +Notation "x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr). + +Notation "stmt:( s )" := s (s custom stmt). +Check stmt:(! _ = _ !). +Check stmt:(? _ = _). +Check stmt:(_ = _). +Check stmt:(! 1 = 1 !). +Check stmt:(? 1 = 1). +Check stmt:(1 = 1). +Check stmt:(_ = 1). diff --git a/test-suite/bugs/closed/bug_9521.v b/test-suite/bugs/closed/bug_9521.v new file mode 100644 index 0000000000..0464c62c09 --- /dev/null +++ b/test-suite/bugs/closed/bug_9521.v @@ -0,0 +1,23 @@ +(* Example from #9521 *) + +Module A. + +Declare Custom Entry expr. +Notation "expr0:( s )" := s (s custom expr at level 0). +Notation "#" := 0 (in custom expr at level 1). +Check expr0:(#). (* Should not be an anomaly "unknown level 0" *) + +End A. + +(* Another example from a comment at #11561 *) + +Module B. + +Declare Custom Entry special. +Declare Custom Entry expr. +Notation "## x" := (S x) (in custom expr at level 10, x custom special at level 10). +Notation "[ e ]" := e (e custom expr at level 10). +Notation "1" := 1 (in custom special). +Check [ ## 1 ]. + +End B. diff --git a/test-suite/bugs/closed/bug_9640.v b/test-suite/bugs/closed/bug_9640.v new file mode 100644 index 0000000000..4dc0bead7b --- /dev/null +++ b/test-suite/bugs/closed/bug_9640.v @@ -0,0 +1,23 @@ +(* Similar to #9521 (was an anomaly unknown level 150 *) + +Module A. + +Declare Custom Entry expr. +Notation "p" := (p) (in custom expr at level 150, p constr, right associativity). +Notation "** X" := (X) (at level 200, X custom expr at level 150). +Lemma t : ** True. +Abort. + +End A. + +(* Similar to #9517, #9519, #11331 *) + +Module B. + +Declare Custom Entry expr. +Notation "p" := (p) (in custom expr at level 100, p constr (* at level 200 *)). +Notation "** X" := (X) (at level 200, X custom expr at level 150). +Lemma t : ** True. +Abort. + +End B. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f65696e464..1c8f237bb8 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,6 +14,8 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat +[2 + 3] + : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] @@ -71,3 +73,7 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". +Entry constr:expr is +[ "201" RIGHTA + [ "{"; constr:operconstr LEVEL "200"; "}" ] ] + diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4de6ce19b4..4ab800c9ba 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,6 +22,9 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. +Notation "n" := n%nat (in custom myconstr at level 0, n bigint). +Check [ 2 + 3 ]. + End A. Module B. @@ -184,3 +187,11 @@ Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). End M. + +Module Bug11331. + +Declare Custom Entry expr. +Notation "{ p }" := (p) (in custom expr at level 201, p constr). +Print Custom Grammar expr. + +End Bug11331. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 74335da2f1..2e8af3ecb9 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1630,6 +1630,31 @@ End Fold_Right_Recursor. intros f g H l. rewrite filter_map. apply map_ext. assumption. Qed. + (** Remove by filtering *) + + Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + + Definition remove' (x : A) : list A -> list A := + filter (fun y => if eq_dec x y then false else true). + + Lemma remove_alt (x : A) (l : list A) : remove' x l = remove eq_dec x l. + Proof with intuition. + induction l... + simpl. destruct eq_dec; f_equal... + Qed. + + (** Counting occurrences by filtering *) + + Definition count_occ' (l : list A) (x : A) : nat := + length (filter (fun y => if eq_dec y x then true else false) l). + + Lemma count_occ_alt (l : list A) (x : A) : + count_occ' l x = count_occ eq_dec l x. + Proof with intuition. + unfold count_occ'. induction l... + simpl; destruct eq_dec; simpl... + Qed. + End Filtering. diff --git a/plugins/btauto/Algebra.v b/theories/btauto/Algebra.v index 4a603f2c52..4a603f2c52 100644 --- a/plugins/btauto/Algebra.v +++ b/theories/btauto/Algebra.v diff --git a/plugins/btauto/Btauto.v b/theories/btauto/Btauto.v index d3331ccf89..d3331ccf89 100644 --- a/plugins/btauto/Btauto.v +++ b/theories/btauto/Btauto.v diff --git a/plugins/btauto/Reflect.v b/theories/btauto/Reflect.v index 867fe69550..867fe69550 100644 --- a/plugins/btauto/Reflect.v +++ b/theories/btauto/Reflect.v diff --git a/plugins/derive/Derive.v b/theories/derive/Derive.v index d1046ae79b..d1046ae79b 100644 --- a/plugins/derive/Derive.v +++ b/theories/derive/Derive.v diff --git a/plugins/extraction/ExtrHaskellBasic.v b/theories/extraction/ExtrHaskellBasic.v index d08a81da64..d08a81da64 100644 --- a/plugins/extraction/ExtrHaskellBasic.v +++ b/theories/extraction/ExtrHaskellBasic.v diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/theories/extraction/ExtrHaskellNatInt.v index 267322d9ed..267322d9ed 100644 --- a/plugins/extraction/ExtrHaskellNatInt.v +++ b/theories/extraction/ExtrHaskellNatInt.v diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/theories/extraction/ExtrHaskellNatInteger.v index 4c5c71f58a..4c5c71f58a 100644 --- a/plugins/extraction/ExtrHaskellNatInteger.v +++ b/theories/extraction/ExtrHaskellNatInteger.v diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/theories/extraction/ExtrHaskellNatNum.v index 09b0444614..09b0444614 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/theories/extraction/ExtrHaskellNatNum.v diff --git a/plugins/extraction/ExtrHaskellString.v b/theories/extraction/ExtrHaskellString.v index 8c61f4e96b..8c61f4e96b 100644 --- a/plugins/extraction/ExtrHaskellString.v +++ b/theories/extraction/ExtrHaskellString.v diff --git a/plugins/extraction/ExtrHaskellZInt.v b/theories/extraction/ExtrHaskellZInt.v index 0345ffc4e8..0345ffc4e8 100644 --- a/plugins/extraction/ExtrHaskellZInt.v +++ b/theories/extraction/ExtrHaskellZInt.v diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/theories/extraction/ExtrHaskellZInteger.v index f7f9e2f80d..f7f9e2f80d 100644 --- a/plugins/extraction/ExtrHaskellZInteger.v +++ b/theories/extraction/ExtrHaskellZInteger.v diff --git a/plugins/extraction/ExtrHaskellZNum.v b/theories/extraction/ExtrHaskellZNum.v index 4141bd203f..4141bd203f 100644 --- a/plugins/extraction/ExtrHaskellZNum.v +++ b/theories/extraction/ExtrHaskellZNum.v diff --git a/plugins/extraction/ExtrOCamlFloats.v b/theories/extraction/ExtrOCamlFloats.v index 1891772cc2..1891772cc2 100644 --- a/plugins/extraction/ExtrOCamlFloats.v +++ b/theories/extraction/ExtrOCamlFloats.v diff --git a/plugins/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v index a2ee602313..a2ee602313 100644 --- a/plugins/extraction/ExtrOCamlInt63.v +++ b/theories/extraction/ExtrOCamlInt63.v diff --git a/plugins/extraction/ExtrOcamlBasic.v b/theories/extraction/ExtrOcamlBasic.v index 2f82b24862..2f82b24862 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/theories/extraction/ExtrOcamlBasic.v diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v index f8bc86d087..f8bc86d087 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/theories/extraction/ExtrOcamlBigIntConv.v diff --git a/plugins/extraction/ExtrOcamlChar.v b/theories/extraction/ExtrOcamlChar.v index 1e68365dd3..1e68365dd3 100644 --- a/plugins/extraction/ExtrOcamlChar.v +++ b/theories/extraction/ExtrOcamlChar.v diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v index 2de1906323..2de1906323 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/theories/extraction/ExtrOcamlIntConv.v diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v index a66d6e41fd..a66d6e41fd 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/theories/extraction/ExtrOcamlNatBigInt.v diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/theories/extraction/ExtrOcamlNatInt.v index 406a7f0d2b..406a7f0d2b 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/theories/extraction/ExtrOcamlNatInt.v diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/theories/extraction/ExtrOcamlNativeString.v index ec3da1e444..ec3da1e444 100644 --- a/plugins/extraction/ExtrOcamlNativeString.v +++ b/theories/extraction/ExtrOcamlNativeString.v diff --git a/plugins/extraction/ExtrOcamlString.v b/theories/extraction/ExtrOcamlString.v index 18c5ed3fe4..18c5ed3fe4 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/theories/extraction/ExtrOcamlString.v diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v index c36ea50755..c36ea50755 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/theories/extraction/ExtrOcamlZBigInt.v diff --git a/plugins/extraction/ExtrOcamlZInt.v b/theories/extraction/ExtrOcamlZInt.v index c7343d2468..c7343d2468 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/theories/extraction/ExtrOcamlZInt.v diff --git a/plugins/extraction/Extraction.v b/theories/extraction/Extraction.v index 207c95247e..207c95247e 100644 --- a/plugins/extraction/Extraction.v +++ b/theories/extraction/Extraction.v diff --git a/plugins/funind/FunInd.v b/theories/funind/FunInd.v index d58b169154..d58b169154 100644 --- a/plugins/funind/FunInd.v +++ b/theories/funind/FunInd.v diff --git a/plugins/funind/Recdef.v b/theories/funind/Recdef.v index cd3d69861f..cd3d69861f 100644 --- a/plugins/funind/Recdef.v +++ b/theories/funind/Recdef.v diff --git a/plugins/ltac/Ltac.v b/theories/ltac/Ltac.v index e69de29bb2..e69de29bb2 100644 --- a/plugins/ltac/Ltac.v +++ b/theories/ltac/Ltac.v diff --git a/plugins/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v index 7ad5e313e3..7ad5e313e3 100644 --- a/plugins/micromega/DeclConstant.v +++ b/theories/micromega/DeclConstant.v diff --git a/plugins/micromega/Env.v b/theories/micromega/Env.v index 8f4d4726b6..8f4d4726b6 100644 --- a/plugins/micromega/Env.v +++ b/theories/micromega/Env.v diff --git a/plugins/micromega/EnvRing.v b/theories/micromega/EnvRing.v index 2762bb6b32..2762bb6b32 100644 --- a/plugins/micromega/EnvRing.v +++ b/theories/micromega/EnvRing.v diff --git a/plugins/micromega/Fourier.v b/theories/micromega/Fourier.v index 0153de1dab..0153de1dab 100644 --- a/plugins/micromega/Fourier.v +++ b/theories/micromega/Fourier.v diff --git a/plugins/micromega/Fourier_util.v b/theories/micromega/Fourier_util.v index 95fa5b88df..95fa5b88df 100644 --- a/plugins/micromega/Fourier_util.v +++ b/theories/micromega/Fourier_util.v diff --git a/plugins/micromega/Lia.v b/theories/micromega/Lia.v index e53800d07d..e53800d07d 100644 --- a/plugins/micromega/Lia.v +++ b/theories/micromega/Lia.v diff --git a/plugins/micromega/Lqa.v b/theories/micromega/Lqa.v index 25fb62cfad..25fb62cfad 100644 --- a/plugins/micromega/Lqa.v +++ b/theories/micromega/Lqa.v diff --git a/plugins/micromega/Lra.v b/theories/micromega/Lra.v index 2403696696..2403696696 100644 --- a/plugins/micromega/Lra.v +++ b/theories/micromega/Lra.v diff --git a/plugins/micromega/MExtraction.v b/theories/micromega/MExtraction.v index 0e8c09ef1b..0e8c09ef1b 100644 --- a/plugins/micromega/MExtraction.v +++ b/theories/micromega/MExtraction.v diff --git a/plugins/micromega/OrderedRing.v b/theories/micromega/OrderedRing.v index d5884d9c1c..d5884d9c1c 100644 --- a/plugins/micromega/OrderedRing.v +++ b/theories/micromega/OrderedRing.v diff --git a/plugins/micromega/Psatz.v b/theories/micromega/Psatz.v index 16ae24ba81..16ae24ba81 100644 --- a/plugins/micromega/Psatz.v +++ b/theories/micromega/Psatz.v diff --git a/plugins/micromega/QMicromega.v b/theories/micromega/QMicromega.v index 4a02d1d01e..4a02d1d01e 100644 --- a/plugins/micromega/QMicromega.v +++ b/theories/micromega/QMicromega.v diff --git a/plugins/micromega/RMicromega.v b/theories/micromega/RMicromega.v index 0f7a02c2c9..0f7a02c2c9 100644 --- a/plugins/micromega/RMicromega.v +++ b/theories/micromega/RMicromega.v diff --git a/plugins/micromega/Refl.v b/theories/micromega/Refl.v index cd759029fa..cd759029fa 100644 --- a/plugins/micromega/Refl.v +++ b/theories/micromega/Refl.v diff --git a/plugins/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v index aa8876357a..aa8876357a 100644 --- a/plugins/micromega/RingMicromega.v +++ b/theories/micromega/RingMicromega.v diff --git a/plugins/micromega/Tauto.v b/theories/micromega/Tauto.v index a155207e2e..a155207e2e 100644 --- a/plugins/micromega/Tauto.v +++ b/theories/micromega/Tauto.v diff --git a/plugins/micromega/VarMap.v b/theories/micromega/VarMap.v index 6db62e8401..6db62e8401 100644 --- a/plugins/micromega/VarMap.v +++ b/theories/micromega/VarMap.v diff --git a/plugins/micromega/ZCoeff.v b/theories/micromega/ZCoeff.v index 08f3f39204..08f3f39204 100644 --- a/plugins/micromega/ZCoeff.v +++ b/theories/micromega/ZCoeff.v diff --git a/plugins/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index 9bedb47371..9bedb47371 100644 --- a/plugins/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v diff --git a/plugins/micromega/Zify.v b/theories/micromega/Zify.v index 18cd196148..18cd196148 100644 --- a/plugins/micromega/Zify.v +++ b/theories/micromega/Zify.v diff --git a/plugins/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v index 4060478363..4060478363 100644 --- a/plugins/micromega/ZifyBool.v +++ b/theories/micromega/ZifyBool.v diff --git a/plugins/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index d3f7f91074..d3f7f91074 100644 --- a/plugins/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v diff --git a/plugins/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v index df75cf2c05..df75cf2c05 100644 --- a/plugins/micromega/ZifyComparison.v +++ b/theories/micromega/ZifyComparison.v diff --git a/plugins/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index edfb5a2a94..edfb5a2a94 100644 --- a/plugins/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v diff --git a/plugins/micromega/Ztac.v b/theories/micromega/Ztac.v index 091f58a0ef..091f58a0ef 100644 --- a/plugins/micromega/Ztac.v +++ b/theories/micromega/Ztac.v diff --git a/plugins/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v index 896ee303cc..896ee303cc 100644 --- a/plugins/nsatz/Nsatz.v +++ b/theories/nsatz/Nsatz.v diff --git a/plugins/omega/Omega.v b/theories/omega/Omega.v index 4ceb530827..4ceb530827 100644 --- a/plugins/omega/Omega.v +++ b/theories/omega/Omega.v diff --git a/plugins/omega/OmegaLemmas.v b/theories/omega/OmegaLemmas.v index d2378569fc..d2378569fc 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/theories/omega/OmegaLemmas.v diff --git a/plugins/omega/OmegaPlugin.v b/theories/omega/OmegaPlugin.v index 303eb0527a..303eb0527a 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/theories/omega/OmegaPlugin.v diff --git a/plugins/omega/OmegaTactic.v b/theories/omega/OmegaTactic.v index 303eb0527a..303eb0527a 100644 --- a/plugins/omega/OmegaTactic.v +++ b/theories/omega/OmegaTactic.v diff --git a/plugins/omega/PreOmega.v b/theories/omega/PreOmega.v index 34533670f8..34533670f8 100644 --- a/plugins/omega/PreOmega.v +++ b/theories/omega/PreOmega.v diff --git a/plugins/rtauto/Bintree.v b/theories/rtauto/Bintree.v index 6b92445326..6b92445326 100644 --- a/plugins/rtauto/Bintree.v +++ b/theories/rtauto/Bintree.v diff --git a/plugins/rtauto/Rtauto.v b/theories/rtauto/Rtauto.v index 2e9b4347b9..2e9b4347b9 100644 --- a/plugins/rtauto/Rtauto.v +++ b/theories/rtauto/Rtauto.v diff --git a/plugins/setoid_ring/Algebra_syntax.v b/theories/setoid_ring/Algebra_syntax.v index 5f594d29cd..5f594d29cd 100644 --- a/plugins/setoid_ring/Algebra_syntax.v +++ b/theories/setoid_ring/Algebra_syntax.v diff --git a/plugins/setoid_ring/ArithRing.v b/theories/setoid_ring/ArithRing.v index 727e99f0b4..727e99f0b4 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/theories/setoid_ring/ArithRing.v diff --git a/plugins/setoid_ring/BinList.v b/theories/setoid_ring/BinList.v index 958832274b..958832274b 100644 --- a/plugins/setoid_ring/BinList.v +++ b/theories/setoid_ring/BinList.v diff --git a/plugins/setoid_ring/Cring.v b/theories/setoid_ring/Cring.v index df0313a624..df0313a624 100644 --- a/plugins/setoid_ring/Cring.v +++ b/theories/setoid_ring/Cring.v diff --git a/plugins/setoid_ring/Field.v b/theories/setoid_ring/Field.v index 9ff07948df..9ff07948df 100644 --- a/plugins/setoid_ring/Field.v +++ b/theories/setoid_ring/Field.v diff --git a/plugins/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v index a5390efc7f..a5390efc7f 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/theories/setoid_ring/Field_tac.v diff --git a/plugins/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v index 3736bc47a5..3736bc47a5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/theories/setoid_ring/Field_theory.v diff --git a/plugins/setoid_ring/InitialRing.v b/theories/setoid_ring/InitialRing.v index dc096554c8..dc096554c8 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/theories/setoid_ring/InitialRing.v diff --git a/plugins/setoid_ring/Integral_domain.v b/theories/setoid_ring/Integral_domain.v index f1394c51d5..f1394c51d5 100644 --- a/plugins/setoid_ring/Integral_domain.v +++ b/theories/setoid_ring/Integral_domain.v diff --git a/plugins/setoid_ring/NArithRing.v b/theories/setoid_ring/NArithRing.v index 8cda4ad714..8cda4ad714 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/theories/setoid_ring/NArithRing.v diff --git a/plugins/setoid_ring/Ncring.v b/theories/setoid_ring/Ncring.v index 8f3de26272..8f3de26272 100644 --- a/plugins/setoid_ring/Ncring.v +++ b/theories/setoid_ring/Ncring.v diff --git a/plugins/setoid_ring/Ncring_initial.v b/theories/setoid_ring/Ncring_initial.v index e40ef6056d..e40ef6056d 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/theories/setoid_ring/Ncring_initial.v diff --git a/plugins/setoid_ring/Ncring_polynom.v b/theories/setoid_ring/Ncring_polynom.v index 048c8eecf9..048c8eecf9 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/theories/setoid_ring/Ncring_polynom.v diff --git a/plugins/setoid_ring/Ncring_tac.v b/theories/setoid_ring/Ncring_tac.v index 65233873b1..65233873b1 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/theories/setoid_ring/Ncring_tac.v diff --git a/plugins/setoid_ring/RealField.v b/theories/setoid_ring/RealField.v index d83fcf3781..d83fcf3781 100644 --- a/plugins/setoid_ring/RealField.v +++ b/theories/setoid_ring/RealField.v diff --git a/plugins/setoid_ring/Ring.v b/theories/setoid_ring/Ring.v index 35e308565f..35e308565f 100644 --- a/plugins/setoid_ring/Ring.v +++ b/theories/setoid_ring/Ring.v diff --git a/plugins/setoid_ring/Ring_base.v b/theories/setoid_ring/Ring_base.v index 36e7890fbb..36e7890fbb 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/theories/setoid_ring/Ring_base.v diff --git a/plugins/setoid_ring/Ring_polynom.v b/theories/setoid_ring/Ring_polynom.v index 092114ff0b..092114ff0b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/theories/setoid_ring/Ring_polynom.v diff --git a/plugins/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v index 0a14c0ee5c..0a14c0ee5c 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/theories/setoid_ring/Ring_tac.v diff --git a/plugins/setoid_ring/Ring_theory.v b/theories/setoid_ring/Ring_theory.v index dc45853458..dc45853458 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/theories/setoid_ring/Ring_theory.v diff --git a/plugins/setoid_ring/Rings_Q.v b/theories/setoid_ring/Rings_Q.v index b3ed0be916..b3ed0be916 100644 --- a/plugins/setoid_ring/Rings_Q.v +++ b/theories/setoid_ring/Rings_Q.v diff --git a/plugins/setoid_ring/Rings_R.v b/theories/setoid_ring/Rings_R.v index ec91fa9e97..ec91fa9e97 100644 --- a/plugins/setoid_ring/Rings_R.v +++ b/theories/setoid_ring/Rings_R.v diff --git a/plugins/setoid_ring/Rings_Z.v b/theories/setoid_ring/Rings_Z.v index 8a51bcea02..8a51bcea02 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/theories/setoid_ring/Rings_Z.v diff --git a/plugins/setoid_ring/ZArithRing.v b/theories/setoid_ring/ZArithRing.v index 833e19a698..833e19a698 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/theories/setoid_ring/ZArithRing.v diff --git a/plugins/ssr/ssrbool.v b/theories/ssr/ssrbool.v index 475859fcc2..475859fcc2 100644 --- a/plugins/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v diff --git a/plugins/ssr/ssrclasses.v b/theories/ssr/ssrclasses.v index 0ae3f8c6a5..0ae3f8c6a5 100644 --- a/plugins/ssr/ssrclasses.v +++ b/theories/ssr/ssrclasses.v diff --git a/plugins/ssr/ssreflect.v b/theories/ssr/ssreflect.v index bc4a57dedd..bc4a57dedd 100644 --- a/plugins/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v diff --git a/plugins/ssr/ssrfun.v b/theories/ssr/ssrfun.v index dd847169b9..dd847169b9 100644 --- a/plugins/ssr/ssrfun.v +++ b/theories/ssr/ssrfun.v diff --git a/plugins/ssr/ssrsetoid.v b/theories/ssr/ssrsetoid.v index 7c5cd135fe..7c5cd135fe 100644 --- a/plugins/ssr/ssrsetoid.v +++ b/theories/ssr/ssrsetoid.v diff --git a/plugins/ssr/ssrunder.v b/theories/ssr/ssrunder.v index 7c529a6133..7c529a6133 100644 --- a/plugins/ssr/ssrunder.v +++ b/theories/ssr/ssrunder.v diff --git a/plugins/ssrmatching/ssrmatching.v b/theories/ssrmatching/ssrmatching.v index 23a16615f5..23a16615f5 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/theories/ssrmatching/ssrmatching.v diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index d3ed5e78b4..49fb88cd8c 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -91,6 +91,7 @@ COQDEP ?= "$(COQBIN)coqdep" COQDOC ?= "$(COQBIN)coqdoc" COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" # Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" @@ -455,13 +456,13 @@ all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` all.pdf: $(VFILES) $(SHOW)'COQDOC -pdf $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g @@ -747,12 +748,12 @@ $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) # If this makefile is created using a _CoqProject we have coqdep get # options from it. This avoids argument length limits for pathological diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index f62947ec67..96fb9710c7 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -213,7 +213,7 @@ let record_dune d ff = if Sys.file_exists sd && Sys.is_directory sd then let out = open_out (bpath [sd;"dune"]) in let fmt = formatter_of_out_channel out in - if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then + if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then fprintf fmt "(include plugin_base.dune)@\n"; out_install fmt d ff; List.iter (pp_dep d fmt) ff; @@ -285,8 +285,11 @@ let exec_ifile f = begin try let ic = open_in in_file in (try f ic - with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic) - with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file + with exn -> + eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); + close_in ic) + with _ -> + eprintf "Error: cannot open input file %s@\n%!" in_file end | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 950c784325..a96173c057 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -31,7 +31,6 @@ let option_sort = ref false let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; - eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; @@ -44,8 +43,6 @@ let usage () = eprintf " -vos : also output dependencies about .vos files\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -suffix s : \n"; - eprintf " -slash : deprecated, no effect\n"; eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 @@ -65,8 +62,6 @@ let treat_coqproject f = iter_sourced (fun f -> treat_file None f) (all_files project) let rec parse = function - (* TODO, deprecate option -c *) - | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll @@ -81,8 +76,6 @@ let rec parse = function | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: s :: ll -> suffixe := s ; parse ll - | "-suffix" :: [] -> usage () | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll @@ -114,11 +107,7 @@ let coqdep () = (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x)); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; - List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; - List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; - List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; if !option_sort then begin sort (); exit 0 end; - if !option_c then mL_dependencies (); coq_dependencies (); () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 5ece595f13..683165f026 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -31,15 +31,12 @@ module StrListMap = Map.Make(StrList) type dynlink = Opt | Byte | Both | No | Variable -let option_c = ref false let option_noglob = ref false let option_dynlink = ref Both let option_boot = ref false let norec_dirs = ref StrSet.empty -let suffixe = ref ".vo" - type dir = string option (** [get_extension f l] checks whether [f] has one of the extensions @@ -58,18 +55,6 @@ let basename_noext filename = let fn = Filename.basename filename in try Filename.chop_extension fn with Invalid_argument _ -> fn -(** ML Files specified on the command line. In the entries: - - the first string is the basename of the file, without extension nor - directory part - - the second string of [mlAccu] is the extension (either .ml or .mlg) - - the [dir] part is the directory, with None used as the current directory -*) - -let mlAccu = ref ([] : (string * string * dir) list) -and mliAccu = ref ([] : (string * dir) list) -and mllibAccu = ref ([] : (string * dir) list) -and mlpackAccu = ref ([] : (string * dir) list) - (** Coq files specifies on the command line: - first string is the full filename, with only its extension removed - second string is the absolute version of the previous (via getcwd) @@ -125,8 +110,6 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, _, search_ml_known = mkknown () -let add_mli_known, _, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () @@ -231,64 +214,6 @@ let file_name s = function | None -> s | Some d -> d // s -let depend_ML str = - match search_mli_known str, search_ml_known str with - | Some mlidir, Some mldir -> - let mlifile = file_name str mlidir - and mlfile = file_name str mldir in - (" "^mlifile^".cmi"," "^mlfile^".cmx") - | None, Some mldir -> - let mlfile = file_name str mldir in - (" "^mlfile^".cmo"," "^mlfile^".cmx") - | Some mlidir, None -> - let mlifile = file_name str mlidir in - (" "^mlifile^".cmi"," "^mlifile^".cmi") - | None, None -> "", "" - -let traite_fichier_ML md ext = - try - let chan = open_in (md ^ ext) in - let buf = Lexing.from_channel chan in - let deja_vu = ref (StrSet.singleton md) in - let a_faire = ref "" in - let a_faire_opt = ref "" in - begin try - while true do - let (Use_module str) = caml_action buf in - if StrSet.mem str !deja_vu then - () - else begin - deja_vu := StrSet.add str !deja_vu; - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt - end - done - with Fin_fichier -> () - end; - close_in chan; - (!a_faire, !a_faire_opt) - with Sys_error _ -> ("","") - -let traite_fichier_modules md ext = - try - let chan = open_in (md ^ ext) in - let list = mllib_list (Lexing.from_channel chan) in - List.fold_left - (fun a_faire str -> match search_mlpack_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire @ [file] - | None -> - match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire @ [file] - | None -> a_faire) [] list - with - | Sys_error _ -> [] - | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) - (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while backslashes themselves must be escaped only if part of a sequence @@ -418,10 +343,7 @@ let rec find_dependencies basename = | None -> match search_mlpack_known s with | Some mldir -> declare ".cmo" mldir s - | None -> - match search_ml_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> warning_declare f str + | None -> warning_declare f str end in List.iter decl sl @@ -449,59 +371,16 @@ let rec find_dependencies basename = with Sys_error _ -> [] (* TODO: report an error? *) -let mL_dependencies () = - List.iter - (fun (name,ext,dirname) -> - let fullname = file_name name dirname in - let (dep,dep_opt) = traite_fichier_ML fullname ext in - let intf = match search_mli_known name with - | None -> "" - | Some mldir -> " "^(file_name name mldir)^".cmi" - in - let efullname = escape fullname in - printf "%s.cmo:%s%s\n" efullname dep intf; - printf "%s.cmx:%s%s\n%!" efullname dep_opt intf) - (List.rev !mlAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let (dep,_) = traite_fichier_ML fullname ".mli" in - printf "%s.cmi:%s\n%!" (escape fullname) dep) - (List.rev !mliAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mllib" in - let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); - printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname) - (List.rev !mllibAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mlpack" in - let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); - printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in - List.iter (fun dep -> - printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) - dep; - printf "%!") - (List.rev !mlpackAccu) - let write_vos = ref false let coq_dependencies () = List.iter (fun (name,_) -> let ename = escape name in - let glob = if !option_noglob then "" else " "^ename^".glob" in + let glob = if !option_noglob then "" else ename^".glob " in let deps = find_dependencies name in - printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename - (string_of_dependency_list !suffixe deps); + printf "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename + (string_of_dependency_list ".vo" deps); printf "%s.vio: %s.v %s\n" ename ename (string_of_dependency_list ".vio" deps); if !write_vos then @@ -517,10 +396,8 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in + get_extension f [".mllib"; ".mlpack"] in match suff with - | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff - | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () @@ -605,18 +482,15 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with - | (base,".v") -> - let name = file_name base dirname - and absname = absolute_file_name base dirname in - addQueue vAccu (name, absname) - | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) - | (base,".mli") -> addQueue mliAccu (base,dirname) - | (base,".mllib") -> addQueue mllibAccu (base,dirname) - | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) - | _ -> ()) + (match get_extension name [".v"] with + | base,".v" -> + let name = file_name base dirname + and absname = absolute_file_name base dirname in + addQueue vAccu (name, absname) + | _ -> ()) | _ -> () +(* "[sort]" outputs `.v` files required by others *) let sort () = let seen = Hashtbl.create 97 in let rec loop file = @@ -639,7 +513,7 @@ let sort () = done with Fin_fichier -> close_in cin; - printf "%s%s " file !suffixe + printf "%s.v " file end in List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 1820db4a1e..aca68cc780 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -21,11 +21,9 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a val find_dir_logpath: string -> string list (** Options *) -val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val write_vos : bool ref -val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable val option_dynlink : dynlink ref @@ -36,18 +34,11 @@ type dir = string option val treat_file : dir -> string -> unit (** ML-related manipulation *) -val mlAccu : (string * string * dir) list ref -val mliAccu : (string * dir) list ref -val mllibAccu : (string * dir) list ref -val add_ml_known : string -> dir -> string -> unit -val add_mli_known : string -> dir -> string -> unit -val add_mllib_known : string -> dir -> string -> unit -val mL_dependencies : unit -> unit - val coq_dependencies : unit -> unit val add_known : bool -> string -> string list -> string -> unit val add_coqlib_known : bool -> string -> string list -> string -> unit +(* Used to locate plugins for [Declare ML Module] *) val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 018fc1b7a2..24452f203a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -8,12 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type mL_token = Use_module of string - type qualid = string list type coq_token = - Require of qualid option * qualid list + | Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string @@ -23,6 +21,3 @@ exception Fin_fichier exception Syntax_error of int * int val coq_action : Lexing.lexbuf -> coq_token -val caml_action : Lexing.lexbuf -> mL_token -val mllib_list : Lexing.lexbuf -> string list -val ocamldep_parse : Lexing.lexbuf -> string list diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 743da535b8..157c2b7dba 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -13,8 +13,6 @@ open Filename open Lexing - type mL_token = Use_module of string - type qualid = string list type coq_token = @@ -152,56 +150,6 @@ and add_loadpath_as path = parse | dot { AddLoadPath path } -and caml_action = parse - | space + - { caml_action lexbuf } - | "open" space* (caml_up_ident as id) - { Use_module (String.uncapitalize_ascii id) } - | "module" space+ caml_up_ident - { caml_action lexbuf } - | caml_low_ident { caml_action lexbuf } - | caml_up_ident - { qual_id (Lexing.lexeme lexbuf) lexbuf } - | ['0'-'9']+ - | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ - | '0' ['o' 'O'] ['0'-'7']+ - | '0' ['b' 'B'] ['0'-'1']+ - { caml_action lexbuf } - | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)? - { caml_action lexbuf } - | "\"" - { string lexbuf; caml_action lexbuf } - | "'" [^ '\\' '\''] "'" - { caml_action lexbuf } - | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" - { caml_action lexbuf } - | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" - { caml_action lexbuf } - | "(*" - { comment lexbuf; caml_action lexbuf } - | "#" | "&" | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".." - | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" - | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" - | "-." { caml_action lexbuf } - - | ['!' '?' '~'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['=' '<' '>' '@' '^' '|' '&' '$'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['+' '-'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | "**" - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['*' '/' '%'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - and comment = parse | "(*" { comment lexbuf; comment lexbuf } @@ -218,20 +166,6 @@ and comment = parse | _ { comment lexbuf } -and string = parse - | '"' (* '"' *) - { () } - | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] * - { string lexbuf } - | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*) - { string lexbuf } - | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] - { string lexbuf } - | eof - { raise Fin_fichier } - | _ - { string lexbuf } - and load_file = parse | '"' [^ '"']* '"' (*'"'*) { let s = lexeme lexbuf in @@ -320,20 +254,3 @@ and modules mllist = parse { syntax_error lexbuf } | _ { Declare (List.rev mllist) } - -and qual_id ml_module_name = parse - | '.' [^ '.' '(' '['] - { Use_module (String.uncapitalize_ascii ml_module_name) } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - -and mllib_list = parse - | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf) - in s :: mllib_list lexbuf } - | "*predef*" { mllib_list lexbuf } - | space+ { mllib_list lexbuf } - | eof { [] } - | _ { syntax_error lexbuf } - -and ocamldep_parse = parse - | [^ ':' ]* ':' { mllib_list lexbuf } diff --git a/tools/dune b/tools/dune index 204bd09535..c0e4e20f72 100644 --- a/tools/dune +++ b/tools/dune @@ -29,7 +29,15 @@ (modules coqdep_lexer coqdep_common coqdep) (libraries coq.lib)) -(ocamllex coqdep_lexer) +; Bare-bones mllib/mlpack parser +(executable + (name ocamllibdep) + (public_name ocamllibdep) + (modules ocamllibdep) + (package coq) + (libraries unix)) + +(ocamllex coqdep_lexer ocamllibdep) (executable (name coqwc) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 41a4e2a86a..2ecc20f1b0 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -195,6 +195,14 @@ let mllib_dependencies () = flush stdout) (List.rev !mllibAccu) +let coq_makefile_mode = ref false + +let print_for_pack modname d = + if !coq_makefile_mode then + printf "%s.cmx : FOR_PACK=-for-pack %s\n" d modname + else + printf "%s_FORPACK:= -for-pack %s\n" d modname + let mlpack_dependencies () = List.iter (fun (name,dirname) -> @@ -204,7 +212,7 @@ let mlpack_dependencies () = let sdeps = String.concat " " deps in let efullname = escape fullname in printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps; - List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps; + List.iter (print_for_pack modname) deps; printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" @@ -213,6 +221,7 @@ let mlpack_dependencies () = (List.rev !mlpackAccu) let rec parse = function + | "-c" :: r -> coq_makefile_mode := true; parse r | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ac348b9646..3aa9acfc52 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -51,12 +51,17 @@ let load_rcfile ~rcfile ~state = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise -(* Recursively puts dir in the LoadPath if -nois was not passed *) -let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = +(* Recursively puts `.v` files in the LoadPath if -nois was not passed *) +let build_stdlib_vo_path ~load_init ~unix_path ~coq_path = let open Loadpath in - let add_ml = if with_ml then AddRecML else AddNoML in { recursive = true; - path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } + path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = load_init } + } + +let build_stdlib_ml_path ~dir = + let open Loadpath in + { recursive = true + ; path_spec = MlPath dir } let build_userlib_path ~unix_path = @@ -100,9 +105,9 @@ let libs_init_load_path ~load_init = has_ml = AddTopML } } ] @ - (* then standard library and plugins *) - [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; - build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @ + (* then standard library *) + [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @ + [build_stdlib_vo_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) (if Sys.file_exists user_contrib then diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 07656f9715..5e98f5ddc0 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -200,41 +200,44 @@ let assoc_eq al ar = | LeftA, LeftA -> true | _, _ -> false -(* [adjust_level assoc from prod] where [assoc] and [from] are the name +(** [adjust_level assoc from prod] where [assoc] and [from] are the name and associativity of the level where to add the rule; the meaning of the result is - None = SELF - Some None = NEXT - Some (Some (n,cur)) = constr LEVEL n - s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = let open Gramlib.Gramext in function + DefaultLevel = entry name + NextLevel = NEXT + NumLevel n = constr LEVEL n *) +let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with +(* If a level in a different grammar, no other choice than denoting it by absolute level *) + | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> NumLevel n +(* If a default level in a different grammar, the entry name is ok *) + | (DefaultLevel,InternalProd) -> + if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel + | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> + if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel (* Associativity is None means force the level *) - | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) + | (NumLevel n,BorderProd (_,None)) -> NumLevel n + | (DefaultLevel,BorderProd (_,None)) -> assert false (* Compute production name on the right side *) (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> - Some None + | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) -> NextLevel (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some RightA)) -> - Some (Some (n,true)) + | (NumLevel n,BorderProd (Right,Some RightA)) -> NumLevel n + | (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel from (* Compute production name on the left side *) (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some NonA)) -> None + | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> - None + | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> + DefaultLevel (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (NumLevel n,BorderProd (Left,Some a)) -> - begin match a with - | LeftA -> Some (Some (n, true)) - | _ -> Some None - end + | (NumLevel n,BorderProd (Left,Some LeftA)) -> NumLevel n + | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> NextLevel (* None means NEXT *) - | (NextLevel,_) -> Some None + | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); NextLevel (* Compute production name elsewhere *) | (NumLevel n,InternalProd) -> - if from = n + 1 then Some None else Some (Some (n, Int.equal n from)) + if from = n + 1 then NextLevel else NumLevel n type _ target = | ForConstr : constr_expr target @@ -246,6 +249,7 @@ type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry +| TTString : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry @@ -311,13 +315,14 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function | ForConstr -> entry_for_constr | ForPattern -> entry_for_patttern -let is_self from e = match e with +let is_self custom (custom',from) e = Notation.notation_entry_eq custom custom' && match e with | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false | (NumLevel n, BorderProd (Left, _)) -> Int.equal from n | _ -> false -let is_binder_level from e = match e with -| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 +let is_binder_level custom (custom',from) e = match e with +| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> + custom = InConstrEntry && custom' = InConstrEntry && from = 200 | _ -> false let make_sep_rules = function @@ -338,15 +343,15 @@ type ('s, 'a) mayrec_symbol = | MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> - if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200")) - else if is_self from p then MayRecMay Aself + if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200")) + else if is_self custom from p then MayRecMay Aself else let g = target_entry custom forpat in - let lev = adjust_level assoc from p in + let lev = adjust_level custom assoc from p in begin match lev with - | None -> MayRecNo (Aentry g) - | Some None -> MayRecMay Anext - | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev)) + | DefaultLevel -> MayRecNo (Aentry g) + | NextLevel -> MayRecMay Anext + | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev)) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with @@ -365,12 +370,14 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) | TTBigint -> MayRecNo (Aentry Prim.bigint) +| TTString -> MayRecNo (Aentry Prim.string) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint +| ETProdString -> TTAny TTString | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) @@ -410,6 +417,11 @@ match e with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) end +| TTString -> + begin match forpat with + | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v)) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v)) + end | TTReference -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) @@ -503,19 +515,24 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = let empty = (pos, [(name, p4assoc, [])]) in ExtendRule (target_entry where forpat, reinit, empty) -let rec pure_sublevels' custom assoc from forpat level = function +let different_levels (custom,opt_level) (custom',string_level) = + match opt_level with + | None -> true + | Some level -> not (Notation.notation_entry_eq custom custom') || level <> int_of_string string_level + +let rec pure_sublevels' assoc from forpat level = function | [] -> [] | GramConstrNonTerminal (e,_) :: rem -> - let rem = pure_sublevels' custom assoc from forpat level rem in + let rem = pure_sublevels' assoc from forpat level rem in let push where p rem = - match symbol_of_target custom p assoc from forpat with - | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem + match symbol_of_target where p assoc from forpat with + | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem | _ -> rem in (match e with | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem | ETProdConstr (s,p) -> push s p rem | _ -> rem) -| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem +| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' assoc from forpat level rem let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> @@ -530,8 +547,8 @@ let extend_constr state forpat ng = let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key custom forpat n in let fold (accu, state) pt = - let AnyTyRule r = make_ty_rule assoc n forpat pt in - let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in + let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in + let pure_sublevels = pure_sublevels' assoc (custom,n) forpat level pt in let isforpat = target_to_bool forpat in let needed_levels, state = register_empty_levels state isforpat pure_sublevels in let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 728c678055..882be6449d 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1225,31 +1225,32 @@ GRAMMAR EXTEND Gram | { CAst.v = k }, Some s -> SetFormat(k,s) | s, None -> SetFormat ("text",s) end } | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at"; - lev = level -> { SetItemLevel (x::l,None,Some lev) } - | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) } - | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> - { SetItemLevel ([x],Some b,Some lev) } - | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) } + lev = level -> { SetItemLevel (x::l,None,lev) } + | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind -> + { SetItemLevel ([x],b,lev) } + | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) } | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) } ] ] ; syntax_extension_type: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } + | IDENT "string" -> { ETString } | IDENT "binder" -> { ETBinder true } - | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) } - | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } + | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } + | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } | IDENT "pattern" -> { ETPattern (false,None) } | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) } | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) } | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) } | IDENT "closed"; IDENT "binder" -> { ETBinder false } - | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind -> + | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InCustomEntry x,b,n) } ] ] ; - at_level: - [ [ "at"; n = level -> { n } ] ] + at_level_opt: + [ [ "at"; n = level -> { n } + | -> { DefaultLevel } ] ] ; constr_as_binder_kind: [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent } diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 0c39aba70a..d39ee60c25 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -297,7 +297,11 @@ let precedence_of_position_and_level from_level = function n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp | NumLevel n, InternalProd -> n, Prec n | NextLevel, _ -> from_level, L + | DefaultLevel, _ -> + (* Fake value, waiting for PR#5 at herbelin's fork *) 200, + Any +(** Computing precedences of subentries for parsing *) let precedence_of_entry_type (from_custom,from_level) = function | ETConstr (custom,_,x) when notation_entry_eq custom from_custom -> precedence_of_position_and_level from_level x @@ -309,6 +313,22 @@ let precedence_of_entry_type (from_custom,from_level) = function | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n | _ -> 0, E (* should not matter *) +(** Computing precedences for future insertion of parentheses at + the time of printing using hard-wired constr levels *) +let unparsing_precedence_of_entry_type from_level = function + | ETConstr (InConstrEntry,_,x) -> + (* Possible insertion of parentheses at printing time to deal + with precedence in a constr entry is managed using [prec_less] + in [ppconstr.ml] *) + snd (precedence_of_position_and_level from_level x) + | ETConstr (custom,_,_) -> + (* Precedence of printing for a custom entry is managed using + explicit insertion of entry coercions at the time of building + a [constr_expr] *) + Any + | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0) + | _ -> Any (* should not matter *) + (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) (* "x =S y" : "x /1 =S /1 y" (protect from confusion; each side for symmetry)*) @@ -374,9 +394,9 @@ let check_open_binder isopen sl m = let unparsing_metavar i from typs = let x = List.nth typs (i-1) in - let prec = snd (precedence_of_entry_type from x) in + let prec = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint -> + | ETConstr _ | ETGlobal | ETBigint | ETString -> UnpMetaVar (i,prec) | ETPattern _ -> UnpBinderMetaVar (i,prec) @@ -389,12 +409,12 @@ let unparsing_metavar i from typs = let index_id id l = List.index Id.equal id l -let make_hunks etyps symbols from = +let make_hunks etyps symbols from_level = let vars,typs = List.split etyps in let rec make b = function | NonTerminal m :: prods -> let i = index_id m vars in - let u = unparsing_metavar i from typs in + let u = unparsing_metavar i from_level typs in if is_next_non_terminal b prods then (None, u) :: add_break_if_none 1 b (make b prods) else @@ -428,7 +448,7 @@ let make_hunks etyps symbols from = | SProdList (m,sl) :: prods -> let i = index_id m vars in let typ = List.nth typs (i-1) in - let _,prec = precedence_of_entry_type from typ in + let prec = unparsing_precedence_of_entry_type from_level typ in let sl' = (* If no separator: add a break *) if List.is_empty sl then add_break 1 [] @@ -555,7 +575,7 @@ let read_recursive_format sl fmt = the names in the notation *) slfmt, res -let hunks_of_format (from,(vars,typs)) symfmt = +let hunks_of_format (from_level,(vars,typs)) symfmt = let rec aux = function | symbs, (_,(UnpTerminal s' as u)) :: fmt when String.equal s' (String.make (String.length s') ' ') -> @@ -565,13 +585,13 @@ let hunks_of_format (from,(vars,typs)) symfmt = let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') -> let i = index_id s vars in - let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l + let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from_level typs :: l | symbs, (_,(UnpCut _ as u)) :: fmt -> let symbs, l = aux (symbs,fmt) in symbs, u :: l | SProdList (m,sl) :: symbs, fmt when has_ldots fmt -> let i = index_id m vars in let typ = List.nth typs (i-1) in - let _,prec = precedence_of_entry_type from typ in + let prec = unparsing_precedence_of_entry_type from_level typ in let loc_slfmt,rfmt = read_recursive_format sl fmt in let sl, slfmt = aux (sl,loc_slfmt) in if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); @@ -666,6 +686,7 @@ let prod_entry_type = function | ETIdent -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint + | ETString -> ETProdString | ETBinder _ -> assert false (* See check_binder_type *) | ETConstr (s,_,p) -> ETProdConstr (s,p) | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) @@ -955,18 +976,23 @@ let is_only_printing mods = (* Compute precedences from modifiers (or find default ones) *) -let set_entry_type from etyps (x,typ) = +let set_entry_type from n etyps (x,typ) = + let make_lev n s = match typ with + | BorderProd _ -> NumLevel n + | InternalProd -> DefaultLevel in let typ = try match List.assoc x etyps, typ with - | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) -> + | ETConstr (s,bko,DefaultLevel), _ -> + if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ)) + else ETConstr (s,bko,(DefaultLevel,typ)) + | ETConstr (s,bko,n), BorderProd (left,_) -> ETConstr (s,bko,(n,BorderProd (left,None))) - | ETConstr (s,bko,Some n), (_,InternalProd) -> - ETConstr (s,bko,(n,InternalProd)) + | ETConstr (s,bko,n), InternalProd -> + ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x - | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ) + | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> - ETConstr (from,None,typ) + ETConstr (from,None,(make_lev n from,typ)) in (x,typ) let join_auxiliary_recursive_types recvars etyps = @@ -986,7 +1012,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETBigint | ETGlobal + | ETConstr _ | ETBigint | ETString | ETGlobal | ETIdent | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = @@ -1008,7 +1034,7 @@ let make_interpretation_type isrec isonlybinding = function (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) - | ETBigint | ETGlobal -> NtnTypeConstr + | ETBigint | ETString | ETGlobal -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.") @@ -1072,6 +1098,8 @@ type entry_coercion_kind = | IsEntryCoercion of notation_entry_level | IsEntryGlobal of string * int | IsEntryIdent of string * int + | IsEntryNumeral of string * int + | IsEntryString of string * int let is_coercion = function | Some (custom,n,_,[e]) -> @@ -1083,6 +1111,8 @@ let is_coercion = function else Some (IsEntryCoercion subentry) | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) + | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n)) + | ETString, InCustomEntry s -> Some (IsEntryString (s,n)) | _ -> None) | Some _ -> assert false | None -> None @@ -1123,8 +1153,8 @@ let find_precedence custom lev etyps symbols onlyprint = else user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with - | ETConstr (s,_,Some _), s' when s = s' -> test () - | (ETIdent | ETBigint | ETGlobal), _ -> + | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () + | (ETIdent | ETBigint | ETString | ETGlobal), _ -> begin match lev with | None -> ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) @@ -1216,14 +1246,13 @@ module SynData = struct end let find_subentry_types from n assoc etyps symbols = - let innerlevel = NumLevel 200 in let typs = find_symbols - (NumLevel n,BorderProd(Left,assoc)) - (innerlevel,InternalProd) - (NumLevel n,BorderProd(Right,assoc)) + (BorderProd(Left,assoc)) + (InternalProd) + (BorderProd(Right,assoc)) symbols in - let sy_typs = List.map (set_entry_type from etyps) typs in + let sy_typs = List.map (set_entry_type from n etyps) typs in let prec = List.map (assoc_of_type from n) sy_typs in sy_typs, prec @@ -1351,6 +1380,8 @@ let open_notation i (_, nobj) = | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n + | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n + | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n | None -> ()) end @@ -1445,7 +1476,7 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in let custom,level,_,_ = sd.level in let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in - let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in { + let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in { synext_level = sd.level; synext_notation = fst sd.info; synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b31ecea112..c6ba4e2c29 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -107,8 +107,11 @@ open Pputils | InCustomEntry s -> keyword "custom" ++ spc () ++ str s let pr_at_level = function - | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n - | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n + | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + | DefaultLevel -> mt () + + let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n let pr_constr_as_binder_kind = let open Notation_term in function | AsIdent -> spc () ++ keyword "as ident" @@ -120,19 +123,15 @@ open Pputils let pr_set_entry_type pr = function | ETIdent -> str"ident" | ETGlobal -> str"global" - | ETPattern (b,None) -> pr_strict b ++ str"pattern" - | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) + | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko | ETBigint -> str "bigint" + | ETString -> str "string" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" - let pr_at_level_opt = function - | None -> mt () - | Some n -> spc () ++ pr_at_level n - let pr_set_simple_entry_type = - pr_set_entry_type pr_at_level_opt + pr_set_entry_type pr_at_level let pr_comment pr_c = function | CommentConstr c -> pr_c c @@ -402,7 +401,7 @@ let string_of_theorem_kind = let open Decls in function let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> - prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++ + prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++ pr_opt pr_constr_as_binder_kind bko | SetLevel n -> pr_at_level (NumLevel n) | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n)) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f9cde7a005..45018a246c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -180,7 +180,7 @@ type proof_expr = ident_decl * (local_binder_expr list * constr_expr) type syntax_modifier = - | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option + | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level | SetLevel of int | SetCustomEntry of string * int option | SetAssoc of Gramlib.Gramext.g_assoc |