diff options
59 files changed, 354 insertions, 408 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7ec3ba1bd7..744fe1c743 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -74,18 +74,3 @@ jobs: make -j "$NJOBS" test-suite PRINT_LOGS=1 env: NJOBS: "2" - - - name: Create the dmg bundle - run: | - eval $(opam env) - export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig - export OUTDIR="$(pwd)/_install_ci" - ./dev/build/osx/make-macos-dmg.sh - env: - MACOSX_DEPLOYMENT_TARGET: "10.11" - NJOBS: "2" - - - uses: actions/upload-artifact@v2 - with: - name: coq-macOS-installer - path: _build/*.dmg diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 19ee32dd84..52b03e455b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -20,7 +20,7 @@ variables: # Format: $IMAGE-V$DATE-$hash # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g. # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10) - CACHEKEY: "bionic_coq-V2021-04-14-4d961e49fc" + CACHEKEY: "bionic_coq-V2021-04-14-802aebab96" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/Makefile.build b/Makefile.build index cbd4f4efbe..2b626506a3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -256,17 +256,6 @@ BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/% user-contrib/%,$@),, -I ide/coqide -I ide/coqide/protocol) -# On MacOS, the binaries are signed, except our private ones -ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) -LINKMETADATA=$(if $(filter $(PRIVATEBINARIES),$@),,-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist") -CODESIGN=$(if $(filter $(PRIVATEBINARIES),$@),true,codesign -s -) -CODESIGN_HIDE=$(CODESIGN) -else -LINKMETADATA= -CODESIGN=true -CODESIGN_HIDE=$(HIDE)true -endif - ifeq ($(STRIP),true) STRIP_HIDE=$(HIDE)true else @@ -293,7 +282,7 @@ endef define bestocaml $(if $(OPT),\ -$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ +$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -o $@ -linkpkg $(1) $^ && $(STRIP) $@,\ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^) endef @@ -431,9 +420,8 @@ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \ $(SYSMOD) \ - $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ + $(LINKCMX) $(OPTFLAGS) $< -o $@ $(STRIP_HIDE) $@ - $(CODESIGN_HIDE) $@ bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' diff --git a/Makefile.checker b/Makefile.checker index ad296e0e88..320b03fea7 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -38,9 +38,8 @@ ifeq ($(BEST),opt) $(CHICKEN): config/config.cmxa clib/clib.cmxa lib/lib.cmxa kernel/kernel.cmxa \ checker/check.cmxa $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ + $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) -o $@ $^ $(STRIP_HIDE) $@ - $(CODESIGN_HIDE) $@ else $(CHICKEN): $(CHICKENBYTE) rm -f $@ && cp $< $@ diff --git a/Makefile.ide b/Makefile.ide index 6e3713c7bf..e721e90628 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -28,8 +28,6 @@ COQIDEBYTE:=bin/coqide.byte$(EXE) COQIDE:=bin/coqide$(EXE) -COQIDEAPP:=bin/CoqIDE_$(VERSION).app -COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide ## CoqIDE source directory and files @@ -154,9 +152,8 @@ $(IDETOP): ide/coqide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide/coqide -I ide/coqide/protocol/ \ $(SYSMOD) \ - $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ + $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $< -o $@ $(STRIP_HIDE) $@ - $(CODESIGN_HIDE) $@ $(IDETOPBYTE): ide/coqide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) $(SHOW)'COQMKTOP -o $@' @@ -217,7 +214,7 @@ ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) endif -install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time +install-ide-files: $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) ide/coqide/coq.png ide/coqide/*.lang ide/coqide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) @@ -227,76 +224,6 @@ install-ide-info: $(INSTALLLIB) ide/coqide/FAQ $(FULLDOCDIR)/FAQ-CoqIde ########################################################################### -# CoqIde MacOS special targets -########################################################################### - -.PHONY: $(COQIDEAPP)/Contents - -$(COQIDEAPP)/Contents: - $(MKDIR) $@ - sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/coqide/MacOS/Info.plist.template > $@/Info.plist - $(MKDIR) "$@/MacOS" - -$(COQIDEINAPP): ide/coqide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ - -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP_HIDE) $@ - -$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents - $(MKDIR) $@/coq/ - $(INSTALLLIB) ide/coqide/coq.png ide/coqide/*.lang ide/coqide/coq_style.xml $(IDEBINDINGS) $@/coq/ - $(MKDIR) $@/gtksourceview-3.0/{language-specs,styles} - $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-3.0/language-specs/ - $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/ - cp -R "$(GTKSHARE)/"locale $@ - cp -R "$(GTKSHARE)/"themes $@ - $(MKDIR) $@/glib-2.0/schemas - glib-compile-schemas --targetdir=$@/glib-2.0/schemas "$(GTKSHARE)/"glib-2.0/schemas/ - cp -R "$(ADWAITASHARE)/"icons $@ - -$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents - $(MKDIR) $@ - $(INSTALLLIB) $$("$(PIXBUFBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ - -$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents - $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.dylib $@ || $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.so $@ - - -$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib - $(MKDIR) $@/xdg/coq - $(MKDIR) $@/gtk-3.0 - { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ - sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-3.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.{dylib,so} |\ - sed -e "s!/.*\(/immodules/.*.dylib\)!@executable_path/../Resources/\1!" |\ - sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ - sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-3.0/gtk-immodules.loaders - $(MKDIR) $@/pango - echo "[Pango]" > $@/pango/pangorc - -$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) - $(MKDIR) $@ - macpack -d ../Resources/lib $(COQIDEINAPP) - for i in $@/../bin/*; \ - do \ - macpack -d ../lib $$i; \ - done - for i in $@/../loaders/*.so $@/../immodules/*.{dylib,so}; \ - do \ - macpack -d ../lib $$i; \ - done - -$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share - $(INSTALLLIB) ide/coqide/MacOS/*.icns $@ - -$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources - $(CODESIGN_HIDE) $@ - -########################################################################### # CoqIde for Windows special targets ########################################################################### diff --git a/Makefile.make b/Makefile.make index 9f0e06dffc..dc123820ee 100644 --- a/Makefile.make +++ b/Makefile.make @@ -277,7 +277,7 @@ cacheclean: find theories user-contrib test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq distclean: clean cleanconfig cacheclean timingclean diff --git a/configure.ml b/configure.ml index abea59bd60..68e4621cd5 100644 --- a/configure.ml +++ b/configure.ml @@ -13,15 +13,9 @@ open Printf let coq_version = "8.14+alpha" -let coq_macos_version = "8.13.90" (** "[...] should be a string comprised of -three non-negative, period-separated integers [...]" *) let vo_magic = 81391 let state_magic = 581391 let is_a_released_version = false -let distributed_exec = - ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; - "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep";"votour"] - let verbose = ref false (* for debugging this script *) let red, yellow, reset = @@ -1159,7 +1153,6 @@ let write_makefile f = List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs; pr "\n# Coq version\n"; pr "VERSION=%s\n" coq_version; - pr "VERSION4MACOS=%s\n\n" coq_macos_version; pr "# Objective-Caml compile command\n"; pr "OCAML=%S\n" camlexec.top; pr "OCAMLFIND=%S\n" camlexec.find; @@ -1235,33 +1228,6 @@ let write_dune_c_flags f = let _ = write_dune_c_flags "config/dune.c_flags" -let write_macos_metadata exec = - let f = "config/Info-"^exec^".plist" in - let () = safe_remove f in - let o = open_out f in - let pr s = fprintf o s in - pr "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n"; - pr "<!DOCTYPE plist PUBLIC \"-//Apple//DTD PLIST 1.0//EN\" \"http://www.apple.com/DTDs/PropertyList-1.0.dtd\">\n"; - pr "<plist version=\"1.0\">\n"; - pr "<dict>\n"; - pr " <key>CFBundleIdentifier</key>\n"; - pr " <string>fr.inria.coq.%s</string>\n" exec; - pr " <key>CFBundleName</key>\n"; - pr " <string>%s</string>\n" exec; - pr " <key>CFBundleVersion</key>\n"; - pr " <string>%s</string>\n" coq_macos_version; - pr " <key>CFBundleShortVersionString</key>\n"; - pr " <string>%s</string>\n" coq_macos_version; - pr " <key>CFBundleInfoDictionaryVersion</key>\n"; - pr " <string>6.0</string>\n"; - pr "</dict>\n"; - pr "</plist>\n"; - let () = close_out o in - Unix.chmod f 0o444 - -let () = - if arch = "Darwin" then List.iter write_macos_metadata distributed_exec - let write_configpy f = safe_remove f; let o = open_out f in diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh deleted file mode 100755 index 2550cbb31c..0000000000 --- a/dev/build/osx/make-macos-dmg.sh +++ /dev/null @@ -1,37 +0,0 @@ -#!/bin/bash - -# Fail on first error -set -e - -# Configuration setup -DMGDIR=$PWD/_dmg -VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) -APP=bin/CoqIDE_${VERSION}.app - -# Install Coq into the .app file -make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources" install-coq install-ide-toploop - -# Fill .app file with metadata and other .app specific stuff (like non-system .so) -make PRIVATEBINARIES="$APP" -j 1 -l2 "$APP" VERBOSE=1 - -# Create the dmg bundle -mkdir -p "$DMGDIR" -ln -sf /Applications "$DMGDIR/Applications" -cp -r "$APP" "$DMGDIR" - -mkdir -p _build - -# Temporary countermeasure to hdiutil error 5341 -# head -c9703424 /dev/urandom > $DMGDIR/.padding - -hdi_opts=(-volname "coq-$VERSION-installer-macos" - -srcfolder "$DMGDIR" - -ov # overwrite existing file - -format UDZO - -imagekey "zlib-level=9" - - # needed for backward compat since macOS 10.14 which uses APFS by default - # see discussion in #11803 - -fs hfs+ - ) -hdiutil create "${hdi_opts[@]}" "_build/coq-$VERSION-installer-macos.dmg" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index b90457add7..00729cd168 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc, pytest for coqtail -RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ +RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \ pytest==5.4.3 diff --git a/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh b/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh new file mode 100644 index 0000000000..29f2386797 --- /dev/null +++ b/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh @@ -0,0 +1,2 @@ +overlay equations https://github.com/Zimmi48/Coq-Equations coq-13911 13911 remove_type_cast +overlay elpi https://github.com/Zimmi48/coq-elpi patch-1 13911 remove_type_cast diff --git a/doc/changelog/02-specification-language/13911-master.rst b/doc/changelog/02-specification-language/13911-master.rst new file mode 100644 index 0000000000..a0b37dd2d9 --- /dev/null +++ b/doc/changelog/02-specification-language/13911-master.rst @@ -0,0 +1,4 @@ +- **Removed:** + The little used `:>` type cast, which was only interpreted in Program-mode + (`#13911 <https://github.com/coq/coq/pull/13911>`_, + by Jim Fehrle and Théo Zimmermann). diff --git a/doc/changelog/04-tactics/14089-ltac2_unify.rst b/doc/changelog/04-tactics/14089-ltac2_unify.rst new file mode 100644 index 0000000000..5887781db9 --- /dev/null +++ b/doc/changelog/04-tactics/14089-ltac2_unify.rst @@ -0,0 +1,5 @@ +- **Added:** + Ltac2 now has a `unify` tactic + (`#14089 <https://github.com/coq/coq/pull/14089>`_, + fixes `#14083 <https://github.com/coq/coq/issues/14083>`_, + by Samuel Gruetter). diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index abb08d98cc..e262a9305d 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -267,6 +267,11 @@ code span.error { color: inherit !important; } + +.coqdoc-comment { + color: #808080 !important +} + /* make the error message index readable */ .indextable code { white-space: inherit; /* break long lines */ diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d718454364..24e35dd85a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. -.. cmd:: Add Zify @add_zify @one_term +.. cmd:: Add Zify @add_zify @qualid .. insertprodn add_zify add_zify @@ -304,6 +304,9 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. | {| PropOp | PropBinOp | PropUOp | Saturate } Registers an instance of the specified typeclass. + The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that + the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`) + is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`. .. cmd:: Show Zify @show_zify diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a011c81f15..52e47b52ae 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in: The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not produce an equality, contrary to the let pattern construct :g:`let '(x1,..., xn) := t in b`. -Also, :g:`term :>` explicitly asks the system to -coerce term to its support type. It can be useful in notations, for -example: - -.. coqtop:: all - - Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). - -This notation denotes equality on subset types using equality on their -support types, avoiding uses of proof-irrelevance that would come up -when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts :cmd:`Definition` and :cmd:`Fixpoint` diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 06b6c61ea9..e53e6ea1cb 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -4,10 +4,80 @@ Conversion rules ---------------- Coq has conversion rules that can be used to determine if two -terms are equal by definition, or :term:`convertible`. +terms are equal by definition in |CiC|, or :term:`convertible`. Conversion rules consist of reduction rules and expansion rules. -See :ref:`applyingconversionrules`, -which describes tactics that apply these conversion rules. +Equality is determined by +converting both terms to a normal form, then verifying they are syntactically +equal (ignoring differences in the names of bound variables by +:term:`alpha-conversion <alpha-convertible>`). + +.. seealso:: :ref:`applyingconversionrules`, which describes tactics that apply these conversion rules. + +:gdef:`Reductions <reduction>` convert terms to something that is incrementally +closer to its normal form. For example, :term:`zeta-reduction` removes +:n:`let @ident := @term__1 in @term__2` constructs from a term by replacing +:n:`@ident` with :n:`@term__1` wherever :n:`@ident` appears in :n:`@term__2`. +The resulting term may be longer or shorter than the original. + +.. coqtop:: all + + Eval cbv zeta in let i := 1 in i + i. + +:gdef:`Expansions <expansion>` are reductions applied in the opposite direction, +for example expanding `2 + 2` to `let i := 2 in i + i`. While applying +reductions gives a unique result, the associated +expansion may not be unique. For example, `2 + 2` could also be +expanded to `let i := 2 in i + 2`. Reductions that have a unique inverse +expansion are also referred to as :gdef:`contractions <contraction>`. + +The normal form is defined as the result of applying a particular +set of conversion rules (beta-, delta-, iota- and zeta-reduction and eta-expansion) +repeatedly until it's no longer possible to apply any of them. + +Sometimes the result of a reduction tactic will be a simple value, for example reducing +`2*3+4` with `cbv beta delta iota` to `10`, which requires applying several +reduction rules repeatedly. In other cases, it may yield an expression containing +variables, axioms or opaque contants that can't be reduced. + +The useful conversion rules are shown below. All of them except for eta-expansion +can be applied with conversion tactics such as :tacn:`cbv`: + + .. list-table:: + :header-rows: 1 + + * - Conversion name + - Description + + * - beta-reduction + - eliminates `fun` + + * - delta-reduction + - replaces a defined variable or constant with its definition + + * - zeta-reduction + - eliminates `let` + + * - eta-expansion + - replaces a term `f` of type `forall a : A, B` with `fun x : A => f x` + + * - match-reduction + - eliminates `match` + + * - fix-reduction + - replaces a `fix` with a :term:`beta-redex`; + recursive calls to the symbol are replaced with the `fix` term + + * - cofix-reduction + - replaces a `cofix` with a :term:`beta-redex`; + recursive calls to the symbol are replaced with the `cofix` term + + * - iota-reduction + - match-, fix- and cofix-reduction together + +:ref:`applyingconversionrules` +describes tactics that only apply conversion rules. +(Other tactics may use conversion rules in addition +to other changes to the proof state.) α-conversion ~~~~~~~~~~~~ @@ -123,7 +193,7 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. .. math:: λ x:T.~(t~x)~\not\triangleright_η~t - This is because, in general, the type of :math:`t` need not to be convertible + This is because, in general, the type of :math:`t` need not be convertible to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that: .. math:: @@ -142,6 +212,30 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. +Examples +~~~~~~~~ + + .. example:: Simple delta, fix, beta and match reductions + + ``+`` is a :ref:`notation <Notations>` for ``Nat.add``, which is defined + with a :cmd:`Fixpoint`. + + .. coqtop:: all abort + + Print Nat.add. + Goal 1 + 1 = 2. + cbv delta. + cbv fix. + cbv beta. + cbv match. + + The term can be fully reduced with `cbv`: + + .. coqtop:: all abort + + Goal 1 + 1 = 2. + cbv. + .. _proof-irrelevance: Proof Irrelevance diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index fcf61a5bf4..1a729ced4e 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -42,7 +42,6 @@ Type cast term_cast ::= @term10 : @type | @term10 <: @type | @term10 <<: @type - | @term10 :> The expression :n:`@term10 : @type` is a type cast expression. It enforces the type of :n:`@term10` to be :n:`@type`. @@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`). :n:`@term10 <<: @type` specifies that compilation to OCaml will be used to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`). -:n:`@term10 :>` casts to the support type in Program mode. -See :ref:`syntactic_control`. - .. _gallina-definitions: Top-level definitions diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bab9d35099..d4749f781a 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -609,7 +609,7 @@ Abbreviations |SSR| extends the :tacn:`set` tactic by supplying: - + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic; + + an open syntax, similarly to the :tacn:`pose <pose (ssreflect)>` tactic; + a more aggressive matching algorithm; + an improved interpretation of wildcards, taking advantage of the matching algorithm; @@ -899,7 +899,7 @@ context of a goal thanks to the ``in`` tactical. .. tacv:: set @ident := @term in {+ @ident} - This variant of :tacn:`set (ssreflect)` introduces a defined constant + This variant of :tacn:`set <set (ssreflect)>` introduces a defined constant called :token:`ident` in the context, and folds it in the context entries mentioned on the right hand side of ``in``. The body of :token:`ident` is the first subterm matching these context @@ -1202,7 +1202,7 @@ The move tactic. Goal not False. move. - More precisely, the :tacn:`move` tactic inspects the goal and does nothing + More precisely, the :tacn:`move <move (ssreflect)>` tactic inspects the goal and does nothing (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a product or a ``let … in``, and performs :tacn:`hnf` otherwise. @@ -1301,7 +1301,7 @@ The apply tactic this use of the :tacn:`refine` tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms. -:tacn:`apply (ssreflect)` has a special behavior on goals containing +:tacn:`apply <apply (ssreflect)>` has a special behavior on goals containing existential metavariables of sort :g:`Prop`. .. example:: @@ -2461,7 +2461,7 @@ The have tactic. redex, and introduces the lemma under a fresh name, automatically chosen. -Like in the case of the :n:`pose (ssreflect)` tactic (see section :ref:`definitions_ssr`), the types of +Like in the case of the :n:`pose <pose (ssreflect)>` tactic (see section :ref:`definitions_ssr`), the types of the holes are abstracted in term. .. example:: @@ -3775,7 +3775,7 @@ involves the following steps: ``forall n, F1 n = F2 n`` for ``eq_map``). 3. If so :tacn:`under` puts these n goals in head normal form (using - the defective form of the tactic :tacn:`move`), then executes + the defective form of the tactic :tacn:`move <move (ssreflect)>`), then executes the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals @@ -5665,6 +5665,7 @@ Tactics respectively. .. tacn:: move + :name: move (ssreflect) :tacn:`idtac` or :tacn:`hnf` (see :ref:`bookkeeping_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fad02b2645..7bc009fcfe 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1148,7 +1148,7 @@ Managing the local context or at the bottom of the local context. All hypotheses on which the new hypothesis depends are moved too so as to respect the order of dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` - followed by the appropriate call to :tacn:`move … after …`, + followed by the appropriate call to :tacn:`move`, :tacn:`move … before …`, :tacn:`move … at top`, or :tacn:`move … at bottom`. @@ -1235,7 +1235,6 @@ Managing the local context hypotheses that depend on it. .. tacn:: move @ident__1 after @ident__2 - :name: move … after … This moves the hypothesis named :n:`@ident__1` in the local context after the hypothesis named :n:`@ident__2`, where “after” is in reference to the @@ -1256,7 +1255,7 @@ Managing the local context :name: move … before … This moves :n:`@ident__1` towards and just before the hypothesis - named :n:`@ident__2`. As for :tacn:`move … after …`, dependencies + named :n:`@ident__2`. As for :tacn:`move`, dependencies over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies) or in the type of :n:`@ident__1` (when :n:`@ident__1` comes after :n:`@ident__2` in the order of @@ -2502,7 +2501,7 @@ and an explanation of the underlying technique. :name: inversion ... using ... .. todo using … instead of ... in the name above gives a Sphinx error, even though - this works just find for :tacn:`move … after …` + this works just find for :tacn:`move` Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index 32d3e87e68..dd1d6051b5 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -15,7 +15,7 @@ .. |c_i| replace:: `c`\ :math:`_{i}` .. |c_n| replace:: `c`\ :math:`_{n}` .. |Cic| replace:: CIC -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{βδιζ}` .. |Latex| replace:: :smallcaps:`LaTeX` .. |Ltac| replace:: `L`:sub:`tac` .. |p_1| replace:: `p`\ :math:`_{1}` diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 522b9900a5..51e26a9082 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -28,7 +28,7 @@ from bs4 import BeautifulSoup from bs4.element import NavigableString COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', - '-s', '--html', '--stdout', '--utf8'] + '-s', '--html', '--stdout', '--utf8', '--parse-comments'] COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) @@ -68,8 +68,19 @@ def lex(source): if isinstance(elem, NavigableString): yield [], elem elif elem.name == "span": - cls = "coqdoc-{}".format(elem['title']) - yield [cls], elem.string + if elem.string: + cls = "coqdoc-{}".format(elem.get("title", "comment")) + yield [cls], elem.string + else: + # handle multi-line comments + children = list(elem.children) + mlc = children[0].startswith("(*") and children[-1].endswith ("*)") + for elem2 in children: + if isinstance(elem2, NavigableString): + cls = ["coqdoc-comment"] if mlc else [] + yield cls, elem2 + elif elem2.name == 'br': + pass elif elem.name == 'br': pass else: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1428dae7ef..468b6b648d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -938,10 +938,11 @@ class CoqtopBlocksTransform(Transform): @staticmethod def split_lines(source): - r"""Split Coq input in chunks + r"""Split Coq input into chunks, which may include single- or + multi-line comments. Nested comments are not supported. A chunk is a minimal sequence of consecutive lines of the input that - ends with a '.' + ends with a '.' or '*)' >>> split_lines('A.\nB.''') ['A.', 'B.'] @@ -962,8 +963,14 @@ class CoqtopBlocksTransform(Transform): >>> split_lines('SearchHead le.\nSearchHead (@eq bool).') ['SearchHead le.', 'SearchHead (@eq bool).'] + + >>> split_lines("(* *) x. (* *)\ny.\n") + ['(* *) x. (* *)', 'y.'] + + >>> split_lines("(* *) x (* \n *)\ny.\n") + ['(* *) x (* \n *)', 'y.'] """ - return re.split(r"(?<=(?<!\.)\.)\n", source.strip()) + return re.split(r"(?:(?<=(?<!\.)\.)|(?<=\*\)))\n", source.strip()) @staticmethod def parse_options(node): @@ -1039,7 +1046,11 @@ class CoqtopBlocksTransform(Transform): if options['warn']: repl.sendone('Set Warnings "default".') for sentence in self.split_lines(node.rawsource): - pairs.append((sentence, repl.sendone(sentence))) + comment = re.compile(r"\s*\(\*.*?\*\)\s*", re.DOTALL) + wo_comments = re.sub(comment, "", sentence) + has_tac = wo_comments != "" and not wo_comments.isspace() + output = repl.sendone(sentence) if has_tac else "" + pairs.append((sentence, output)) if options['abort']: repl.sendone('Abort All.') if options['fail']: @@ -1052,9 +1063,10 @@ class CoqtopBlocksTransform(Transform): # Use Coqdoc to highlight input in_chunks = highlight_using_coqdoc(sentence) dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input'])) - # Parse ANSI sequences to highlight output - out_chunks = AnsiColorsParser().colorize_str(output) - dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) + if output: + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) node.clear() node.rawsource = self.make_rawsource(pairs, options['input'], options['output']) node['classes'].extend(self.block_classes(options['input'] or options['output'])) @@ -1180,8 +1192,7 @@ class StdGlossaryIndex(Index): if type == 'term': entries = content[itemname[0].lower()] entries.append([itemname, 0, docname, anchor, '', '', '']) - content = sorted(content.items()) - return content, False + return content.items(), False def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): """A grammar production not included in a ``prodn`` directive. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index fd1c3c0260..5c211d82e9 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -365,7 +365,6 @@ term100: [ | REPLACE term99 ":" term200 | WITH term99 ":" type | MOVETO term_cast term99 ":" type -| MOVETO term_cast term99 ":>" ] constr: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 0c8980b1bd..fe166524bf 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,6 +1,15 @@ (* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) DOC_GRAMMAR +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry +] + Constr.ident: [ | Prim.ident ] @@ -75,7 +84,6 @@ term100: [ | term99 "<:" term200 | term99 "<<:" term200 | term99 ":" term200 -| term99 ":>" | term99 ] @@ -478,15 +486,6 @@ strategy_level: [ | "transparent" ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry -] - opt_hintbases: [ | | ":" LIST1 IDENT diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 40bb980e90..2b09263cc4 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -553,7 +553,6 @@ term_cast: [ | term10 ":" type | term10 "<:" type | term10 "<<:" type -| term10 ":>" ] term_match: [ diff --git a/ide/coqide/MacOS/Info.plist.template b/ide/coqide/MacOS/Info.plist.template deleted file mode 100644 index e4fb0e5980..0000000000 --- a/ide/coqide/MacOS/Info.plist.template +++ /dev/null @@ -1,89 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd"> -<plist version="1.0"> -<dict> - <key>CFBundleDocumentTypes</key> - <array> - <dict> - <key>CFBundleTypeExtensions</key> - <array> - <string>*</string> - </array> - <key>CFBundleTypeName</key> - <string>NSStringPboardType</string> - <key>CFBundleTypeOSTypes</key> - <array> - <string>****</string> - </array> - <key>CFBundleTypeRole</key> - <string>Editor</string> - </dict> - <dict> - <key>CFBundleTypeIconFile</key> - <string>coqfile.icns</string> - <key>CFBundleTypeName</key> - <string>Coq file</string> - <key>CFBundleTypeRole</key> - <string>Editor</string> - <key>CFBundleTypeMIMETypes</key> - <array> - <string>text/plain</string> - </array> - <key>CFBundleTypeExtensions</key> - <array> - <string>v</string> - </array> - <key>LSHandlerRank</key> - <string>Owner</string> - </dict> - <dict> - <key>CFBundleTypeName</key> - <string>All</string> - <key>CFBundleTypeRole</key> - <string>Editor</string> - <key>CFBundleTypeMIMETypes</key> - <array> - <string>text/plain</string> - </array> - <key>LSHandlerRank</key> - <string>Default</string> - <key>CFBundleTypeExtensions</key> - <array> - <string>*</string> - </array> - </dict> - </array> - <key>CFBundleIconFile</key> - <string>coqide.icns</string> - <key>CFBundleVersion</key> - <string>390</string> - <key>CFBundleName</key> - <string>CoqIDE</string> - <key>CFBundleShortVersionString</key> - <string>VERSION</string> - <key>CFBundleDisplayName</key> - <string>Coq Proof Assistant vVERSION</string> - <key>CFBundleGetInfoString</key> - <string>Coq_vVERSION</string> - <key>NSHumanReadableCopyright</key> - <string>Copyright 1999-2019, Inria, CNRS and contributors</string> - <key>CFBundleHelpBookFolder</key> - <string>share/doc/coq/html/</string> - <key>CFAppleHelpAnchor</key> - <string>index</string> - <key>CFBundleExecutable</key> - <string>coqide</string> - <key>CFBundlePackageType</key> - <string>APPL</string> - <key>CFBundleInfoDictionaryVersion</key> - <string>6.0</string> - <key>CFBundleIdentifier</key> - <string>fr.inria.coq.coqide</string> - <key>LSApplicationCategoryType</key> - <string>public.app-category.developer-tools</string> - <key>CFBundleDevelopmentRegion</key> - <string>English</string> - <key>NSPrincipalClass</key> - <string>NSApplication</string> -</dict> -</plist> diff --git a/ide/coqide/configwin_ihm.ml b/ide/coqide/configwin_ihm.ml index e768131dcf..da1553d751 100644 --- a/ide/coqide/configwin_ihm.ml +++ b/ide/coqide/configwin_ihm.ml @@ -31,6 +31,10 @@ let set_help_tip wev = function | None -> () | Some help -> GtkBase.Widget.Tooltip.set_text wev#as_widget help +let select_arch m m_osx = + if Coq_config.arch = "Darwin" then m_osx else m + +(* How the modifiers are named in the preference box *) let modifiers_to_string m = let rec iter m s = match m with @@ -41,6 +45,7 @@ let modifiers_to_string m = `CONTROL -> "<ctrl>" | `SHIFT -> "<shft>" | `LOCK -> "<lock>" + | `META -> select_arch "<meta>" "<cmd>" | `MOD1 -> "<alt>" | `MOD2 -> "<mod2>" | `MOD3 -> "<mod3>" @@ -773,7 +778,7 @@ let modifiers ?(editable=true) ?(expand=true) ?help - ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) + ?(allow=[`CONTROL;`SHIFT;`LOCK;`META;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) ?(f=(fun _ -> ())) label v = Modifiers_param { diff --git a/ide/coqide/preferences.ml b/ide/coqide/preferences.ml index 8361cc3940..838da6303d 100644 --- a/ide/coqide/preferences.ml +++ b/ide/coqide/preferences.ml @@ -321,18 +321,21 @@ let attach_modifiers (pref : string preference) prefix = in pref#connect#changed ~callback:cb -let select_arch m m_osx = - if Coq_config.arch = "Darwin" then m_osx else m - let modifier_for_navigation = new preference ~name:["modifier_for_navigation"] - ~init:(select_arch "<Control>" "<Control><Primary>") ~repr:Repr.(string) + (* Note: on Darwin, this will give "<Control><Meta>", i.e. Ctrl and Command; on other + architectures, "<Primary>" binds to "<Control>" so it will give "<Control>" alone *) + ~init:"<Control><Primary>" ~repr:Repr.(string) let modifier_for_templates = new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string) +let select_arch m m_osx = + if Coq_config.arch = "Darwin" then m_osx else m + let modifier_for_display = new preference ~name:["modifier_for_display"] + (* Note: <Primary> (i.e. <Meta>, i.e. "Command") on Darwin, i.e. MacOS X, but <Alt> elsewhere *) ~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string) let modifier_for_queries = @@ -348,7 +351,9 @@ let attach_modifiers_callback () = () let modifiers_valid = - new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string) + new preference ~name:["modifiers_valid"] + (* Note: <Primary> is providing <Meta> (i.e. "Command") for Darwin, i.e. MacOS X *) + ~init:"<Alt><Control><Shift><Primary>" ~repr:Repr.(string) let browser_cmd_fmt = try diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index f02874253e..40fe13784a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -261,11 +261,9 @@ and cast_expr_eq c1 c2 = match c1, c2 with | CastConv t1, CastConv t2 | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> constr_expr_eq t1 t2 -| CastCoerce, CastCoerce -> true | CastConv _, _ | CastVM _, _ -| CastNative _, _ -| CastCoerce, _ -> false +| CastNative _, _ -> false let constr_loc c = CAst.(c.loc) let cases_pattern_expr_loc cp = CAst.(cp.loc) @@ -343,7 +341,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CLetIn (na,a,t,b) -> f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ea5e2a1ad4..ea95655c18 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -35,9 +35,8 @@ let rec alpha_var id1 id2 = function let cast_type_iter2 f t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> f t1 t2 | CastVM t1, CastVM t2 -> f t1 t2 - | CastCoerce, CastCoerce -> () | CastNative t1, CastNative t2 -> f t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit + | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit (* used to update the notation variable with the local variables used in NList and NBinderList, since the iterator has its own variable *) @@ -1319,12 +1318,9 @@ let match_cast match_fun sigma c1 c2 = | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> match_fun sigma t1 t2 - | CastCoerce, CastCoerce -> - sigma | CastConv _, _ | CastVM _, _ - | CastNative _, _ - | CastCoerce, _ -> raise No_match + | CastNative _, _ -> raise No_match let does_not_come_from_already_eta_expanded_var glob = (* This is hack to avoid looping on a rule with rhs of the form *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ddbd5fa0a7..13044958dc 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -23,7 +23,7 @@ open Context.Rel.Declaration type mind_specif = mutual_inductive_body * one_inductive_body -(* raise Not_found if not an inductive type *) +(* raises an anomaly if not an inductive type *) let lookup_mind_specif env (kn,tyi) = let mib = Environ.lookup_mind kn env in if tyi >= Array.length mib.mind_packets then diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 5808a3fa65..4afc7c439a 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -30,7 +30,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body (** {6 ... } *) (** Fetching information in the environment about an inductive type. - Raises [Not_found] if the inductive type is not found. *) + Raises an anomaly if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index efe4bfd7f6..d0d1071c26 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -151,9 +151,7 @@ GRAMMAR EXTEND Gram | c1 = term; "<<:"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } | c1 = term; ":"; c2 = term LEVEL "200" -> - { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = term; ":>" -> - { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] + { CAst.make ~loc @@ CCast(c1, CastConv c2) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index cfdaac710b..268d4bf9e9 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1525,8 +1525,7 @@ let inline_test r t = else let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in let has_body = - try constant_has_body (Global.lookup_constant c) - with Not_found -> false + Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c) in has_body && (let t1 = eta_red t in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index cbdebb7bbc..6236a5147d 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) = let sigma = Evd.from_env env in let c, c_body = match f_ref with - | GlobRef.ConstRef c -> ( - try (c, Global.lookup_constant c) - with Not_found -> + | GlobRef.ConstRef c -> + if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else CErrors.user_err Pp.( str "Cannot find " - ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) ) + ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) | _ -> CErrors.user_err Pp.(str "Not a function reference") in match Global.body_of_constant_body Library.indirect_accessor c_body with diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 164a446fe3..fb00d2f202 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -342,7 +342,7 @@ let is_free_in id = | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false | GHole _ -> false | GCast (b, (CastConv t | CastVM t | CastNative t)) -> - is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b + is_free_in b || is_free_in t | GInt _ | GFloat _ -> false | GArray (_u, t, def, ty) -> Array.exists is_free_in t || is_free_in def || is_free_in ty) diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index b780c1833e..3ea7408067 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -46,6 +46,7 @@ let mkrel = lazy (zify "mkrel") let iff_refl = lazy (zify "iff_refl") let eq_iff = lazy (zify "eq_iff") let rew_iff = lazy (zify "rew_iff") +let rew_iff_rev = lazy (zify "rew_iff_rev") (* propositional logic *) @@ -621,14 +622,20 @@ module MakeTable (E : Elt) = struct failwith ("Cannot register term " ^ t) | Some a -> E.mk_elt evd i a + let safe_ref evd c = + try + fst (EConstr.destRef evd c) + with DestKO -> CErrors.user_err Pp.(str "Add Zify "++str E.name ++ str ": the term "++ + gl_pr_constr c ++ str " should be a global reference") + let register_hint evd t elt = match EConstr.kind evd t with | App (c, _) -> - let gr = fst (EConstr.destRef evd c) in - E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table + let gr = safe_ref evd c in + E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table | _ -> - let gr = fst (EConstr.destRef evd t) in - E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table + let gr = safe_ref evd t in + E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table let register_constr env evd c = let c = EConstr.of_constr c in @@ -1365,7 +1372,15 @@ let trans_concl prfp = Tactics.change_concl t') | TProof (t, prf) -> Proofview.Goal.enter (fun gl -> - Equality.general_rewrite true Locus.AllOccurrences true false prf) + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + let typ = get_type_of env evd prf in + match EConstr.kind evd typ with + | App (c, a) when Array.length a = 2 -> + Tactics.apply + (EConstr.mkApp (Lazy.force rew_iff_rev, [|a.(0); a.(1); prf|])) + | _ -> + raise (CErrors.anomaly Pp.(str "zify cannot transform conclusion"))) let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 86d2cc78e0..5a8ac32ffa 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -104,9 +104,8 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with let cast_type_eq eq t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> eq t1 t2 | CastVM t1, CastVM t2 -> eq t1 t2 - | CastCoerce, CastCoerce -> true | CastNative t1, CastNative t2 -> eq t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + | (CastConv _ | CastVM _ | CastNative _), _ -> false let matching_var_kind_eq k1 k2 = match k1, k2 with | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 @@ -188,14 +187,12 @@ let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce | CastNative a -> CastNative (f a) let smartmap_cast_type f c = match c with | CastConv a -> let a' = f a in if a' == a then c else CastConv a' | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce | CastNative a -> let a' = f a in if a' == a then c else CastNative a' let map_glob_constr_left_to_right f = DAst.map (function @@ -275,7 +272,7 @@ let fold_glob_constr f acc = DAst.with_val (function Array.fold_left f (Array.fold_left f acc tyl) bv | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f acc t in f acc c | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc @@ -318,7 +315,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function Array.fold_left_i f' acc idl | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f v acc t in f v acc c | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 9f93e5e6c1..d480c12834 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -57,7 +57,6 @@ and glob_fix_kind = type 'a cast_type = | CastConv of 'a | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) | CastNative of 'a (** The kind of patterns that occurs in "match ... with ... end" diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 21b2137f09..4c2fc26b45 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1166,9 +1166,6 @@ struct let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = match k with - | CastCoerce -> - let sigma, cj = pretype empty_tycon env sigma c in - Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4c410c3170..e08a494c2e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -673,8 +673,7 @@ let tag_var = tag Tag.variable match b with | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b - | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b - | CastCoerce -> str ":>"), + | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b), lcast ) | CNotation (_,(_,"( _ )"),([t],[],[],[])) -> diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 9bf765717f..9ba64717d9 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -529,7 +529,6 @@ let match_goals ot nt = | CastVM a, CastVM a2 | CastNative a, CastNative a2 -> constr_expr ogname a a2 - | CastCoerce, CastCoerce -> () | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)")) | CNotation (_,ntn,args), CNotation (_,ntn2,args2) -> constr_notation_substitution ogname args args2 diff --git a/tactics/equality.ml b/tactics/equality.ml index 633b9da053..497ce4ae1a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -379,11 +379,10 @@ let find_elim hdcncl lft2rgt dep cls ot = let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - try - let _ = Global.lookup_constant c1' in c1' - with Not_found -> + if not (Environ.mem_constant c1' (Global.env ())) then user_err ~hdr:"Equality.find_elim" - (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") + (str "Cannot find rewrite principle " ++ Label.print l' ++ str "."); + c1' end | _ -> begin match if is_eq then eq_elimination_ref false sort else None with diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5338e0eef5..783a317b3a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -293,31 +293,34 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if Coqlib.check_ind_ref "core.eq.type" ind then - Some (build_coq_eq_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if Coqlib.check_ind_ref "core.identity.type" ind then - Some (build_coq_identity_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if Coqlib.check_ind_ref "core.JMeq.type" ind then - Some (build_coq_jmeq_data()),hdapp, - HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else - let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let nconstr = Array.length mip.mind_consnames in - if Int.equal nconstr 1 then - let (ctx, cty) = constr_types.(0) in - let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - if is_matching env sigma coq_refl_leibniz1_pattern cty then - None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching env sigma coq_refl_leibniz2_pattern cty then - None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching env sigma coq_refl_jm_pattern cty then - None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else raise NoEquationFound - else raise NoEquationFound - | _ -> raise NoEquationFound + (try + if Coqlib.check_ind_ref "core.eq.type" ind then + Some (build_coq_eq_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.identity.type" ind then + Some (build_coq_identity_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.JMeq.type" ind then + Some (build_coq_jmeq_data()),hdapp, + HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else + let (mib,mip) = Global.lookup_inductive ind in + let constr_types = mip.mind_nf_lc in + let nconstr = Array.length mip.mind_consnames in + if Int.equal nconstr 1 then + let (ctx, cty) = constr_types.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + if is_matching env sigma coq_refl_leibniz1_pattern cty then + None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) + else if is_matching env sigma coq_refl_leibniz2_pattern cty then + None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if is_matching env sigma coq_refl_jm_pattern cty then + None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else raise NoEquationFound + else raise NoEquationFound + with UserError _ -> + raise NoEquationFound) + | _ -> raise NoEquationFound (* Note: An "equality type" is any type with a single argument-free constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also diff --git a/test-suite/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v new file mode 100644 index 0000000000..611464458e --- /dev/null +++ b/test-suite/bugs/closed/bug_14131.v @@ -0,0 +1,19 @@ +Set Implicit Arguments. +Unset Elimination Schemes. + +Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := + JMeq_refl : JMeq x x. + +Set Elimination Schemes. + +Register JMeq as core.JMeq.type. + +Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq x y -> P y. + +Register JMeq_ind as core.JMeq.ind. + +Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq y x -> P y. +Proof. intros. try rewrite H0. +Abort. diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v new file mode 100644 index 0000000000..39b620a6ac --- /dev/null +++ b/test-suite/ltac2/std_tactics.v @@ -0,0 +1,29 @@ +Require Import Ltac2.Ltac2. + +Axiom f: nat -> nat. +Definition g := f. + +Axiom Foo1: nat -> Prop. +Axiom Foo2: nat -> Prop. +Axiom Impl: forall n: nat, Foo1 (f n) -> Foo2 (f n). + +Create HintDb foo discriminated. +#[export] Hint Constants Opaque : foo. +#[export] Hint Resolve Impl : foo. + +Goal forall x, Foo1 (f x) -> Foo2 (g x). +Proof. + auto with foo. + #[export] Hint Transparent g : foo. + auto with foo. +Qed. + +Goal forall (x: nat), exists y, f x = g y. +Proof. + intros. + eexists. + unify f g. + lazy_match! goal with + | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs + end. +Abort. diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v new file mode 100644 index 0000000000..e62b5b8d9e --- /dev/null +++ b/test-suite/micromega/bug_11089.v @@ -0,0 +1,13 @@ +Require Import Lia. +Unset Lia Cache. +Definition t := nat. +Goal forall (n : t), n = n. +Proof. + intros. + lia. +Qed. +Goal let t' := nat in forall (n : t'), n = n. +Proof. + intros. + lia. +Qed. diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v index a12623c3c0..2ea320047d 100644 --- a/test-suite/micromega/zify.v +++ b/test-suite/micromega/zify.v @@ -167,6 +167,12 @@ Goal @zero znat = 0%nat. reflexivity. Qed. +Require Import ZifyBool. +Instance Op_bool_inj : UnOp (inj : bool -> bool) := + { TUOp := id; TUOpInj := fun _ => eq_refl }. +Add Zify UnOp Op_bool_inj. + + Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y), (F P + 1 = 1 + F P)%positive. Proof. @@ -228,6 +234,7 @@ Proof. intros. lia. Qed. + Ltac Zify.zify_pre_hook ::= unfold is_true in *. Goal forall x y : nat, is_true (Nat.eqb x 1) -> diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index a1a4da6f37..575d773c77 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -43,7 +43,7 @@ Class EqDec A R {equiv : Equivalence R} := take precedence of [==] defined in the type scope, hence we can have both at the same time. *) -Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. +Notation " x == y " := (equiv_dec x y) (no associativity, at level 70) : equiv_scope. Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index f4220e3aa1..435dacbd4c 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -42,7 +42,7 @@ Class EqDec `(S : Setoid A) := take precedence of [==] defined in the type scope, hence we can have both at the same time. *) -Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70). +Notation " x == y " := (equiv_dec x y) (no associativity, at level 70). Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index b2bdd8099a..717e3191ea 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -33,8 +33,6 @@ Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scop (** Coerces objects to their support before comparing them. *) -Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope. - Require Import Coq.Bool.Sumbool. (** Construct a dependent disjunction from a boolean. *) diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index 019d11d951..25d9fa9104 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Set Primitive Projections. (** An alternative to [zify] in ML parametrised by user-provided classes instances. @@ -220,6 +219,13 @@ Proof. exact (fun H => proj1 IFF H). Qed. +Lemma rew_iff_rev (P Q : Prop) (IFF : P <-> Q) : Q -> P. +Proof. + exact (fun H => proj2 IFF H). +Qed. + + + (** Registering constants for use by the plugin *) Register eq_iff as ZifyClasses.eq_iff. Register target_prop as ZifyClasses.target_prop. @@ -247,6 +253,7 @@ Register eq as ZifyClasses.eq. Register mkinjprop as ZifyClasses.mkinjprop. Register iff_refl as ZifyClasses.iff_refl. Register rew_iff as ZifyClasses.rew_iff. +Register rew_iff_rev as ZifyClasses.rew_iff_rev. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v index 931d753521..6ddad8f1c9 100644 --- a/user-contrib/Ltac2/Notations.v +++ b/user-contrib/Ltac2/Notations.v @@ -593,6 +593,8 @@ Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0))) Ltac2 Notation typeclasses_eauto := typeclasses_eauto. +Ltac2 Notation "unify" x(constr) y(constr) := Std.unify x y. + (** Congruence *) Ltac2 f_equal0 () := ltac1:(f_equal). diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v index b69a95faf3..3675df9f75 100644 --- a/user-contrib/Ltac2/Std.v +++ b/user-contrib/Ltac2/Std.v @@ -259,3 +259,5 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto". Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto". + +Ltac2 @ external unify : constr -> constr -> unit := "ltac2" "tac_unify". diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index 206f4df19d..0171ddfcf8 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -468,7 +468,7 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme = let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" (fun (env, t) -> - strbrk "The following expression should have type unit but has type " ++ + strbrk "This expression should have type unit but has type " ++ pr_glbtype env t ++ str ".") let warn_redundant_clause = diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml index 895b6d3975..c7dfb3e69e 100644 --- a/user-contrib/Ltac2/tac2stdlib.ml +++ b/user-contrib/Ltac2/tac2stdlib.ml @@ -572,3 +572,7 @@ end let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs -> Tac2tactics.typeclasses_eauto str n dbs end + +let () = define_prim2 "tac_unify" constr constr begin fun x y -> + Tac2tactics.unify x y +end diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 54f5a2cf68..a30f6e7945 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -414,6 +414,8 @@ let typeclasses_eauto strategy depth dbs = in Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs +let unify x y = Tactics.unify x y + (** Inversion *) let inversion knd arg pat ids = diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli index f63f7e722a..47a3fd5987 100644 --- a/user-contrib/Ltac2/tac2tactics.mli +++ b/user-contrib/Ltac2/tac2tactics.mli @@ -119,6 +119,8 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list -> val typeclasses_eauto : Class_tactics.search_strategy option -> int option -> Id.t list option -> unit Proofview.tactic +val unify : constr -> constr -> unit tactic + val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic val contradiction : constr_with_bindings option -> unit tactic diff --git a/vernac/record.ml b/vernac/record.ml index fccc3e4fbd..53f3508806 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -766,11 +766,9 @@ let add_inductive_class env sigma ind = let k = let ctx = oneind.mind_arity_ctxt in let univs = Declareops.inductive_polymorphic_context mind in - let env = push_context ~strict:false (Univ.AUContext.repr univs) env in - let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in let ty = Inductive.type_of_inductive ((mind, oneind), inst) in - let r = Inductive.relevance_of_inductive env ind in + let r = oneind.mind_relevance in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; cl_context = ctx; |