diff options
128 files changed, 2371 insertions, 891 deletions
diff --git a/.gitignore b/.gitignore index 4116190801..8a0c54f8fe 100644 --- a/.gitignore +++ b/.gitignore @@ -119,10 +119,6 @@ g_*.ml ide/project_file.ml parsing/compat.ml -grammar/q_util.ml -grammar/tacextend.ml -grammar/vernacextend.ml -grammar/argextend.ml parsing/cLexer.ml ltac/coretactics.ml ltac/extratactics.ml @@ -161,3 +157,4 @@ dev/myinclude /doc/refman/Reference-Manual.optidx /doc/refman/Reference-Manual.optind user-contrib +.*.sw* @@ -52,6 +52,7 @@ Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-5 Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> Evgeny Makarov <emakarov@gforge> emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@cs.harvard.edu> +Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@gmail.com> Lionel Elie Mamane <lmamane@gforge> lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> Claude Marché <marche@gforge> marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> Micaela Mayero <mayero@gforge> mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -69,6 +70,8 @@ Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-54 Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> +Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> +Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@gforge> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -79,7 +82,8 @@ Arnaud Spiwack <arnaud@spiwack.net> aspiwack <aspiwack@85f007b7-5 Enrico Tassi <Enrico.Tassi@inria.fr> gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <enrico.tassi@inria.fr> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <gares@fettunta.org> -Laurent Théry <thery@gforge> thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> +Laurent Théry <laurent.thery@inria.fr> thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> +Laurent Théry <laurent.thery@inria.fr> thery <thery@sophia.inria.fr> Benjamin Werner <werner@gforge> werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7> # Anonymous accounts @@ -1,5 +1,6 @@ Changes beyond V8.5 =================== + Bugfixes - #4527: when typechecking the statement of a lemma using universe polymorphic @@ -9,6 +10,9 @@ Bugfixes compatible). - #4726: treat user-provided sorts of universe polymorphic records as rigid (i.e. non-minimizable). +- #4592, #4932: notations sharing recursive patterns or sharing + binders made more robust. +- #4780: Induction with universe polymorphism on was creating ill-typed terms. Specification language @@ -79,11 +83,27 @@ Tools computation associated with printing the "dependent evars: " line in -emacs mode +Changes from V8.5pl2 to V8.5pl3 +=============================== + +Critical bugfix +- #4876: Guard checker incompleteness when using primitive projections + +Other bugfixes + +- #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #4673: regression in setoid_rewrite, unfolding let-ins for type unification. +- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. +- #4769: Anomaly with universe polymorphic schemes defined inside sections. +- #3886: Program: duplicate obligations of mutual fixpoints + Changes from V8.5pl1 to V8.5pl2 =============================== Critical bugfix - Checksums of .vo files dependencies were not correctly checked. +- Unicode-to-ASCII translation was not injective, leading in a soundness bug in + the native compiler. Other bugfixes @@ -101,10 +121,17 @@ Other bugfixes - #4818: "Admitted" fails due to undefined universe anomaly after calling "destruct" - #4823: remote counter: avoid thread race on sockets +- #4841: -verbose flag changed semantics in 8.5, is much harder to use +- #4851: [nsatz] cannot handle duplicated hypotheses +- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant + of nsatz +- #4880: [nsatz_compute] generates invalid certificates if given redundant + hypotheses - #4881: synchronizing "Declare Implicit Tactic" with backtrack. - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. triggered by CoqIDE +- #4069, #4718: congruence fails when universes are involved. Universes - Disallow silently dropping universe instances applied to variables @@ -1,6 +1,6 @@ The Coq proof assistant -Copyright 1999-2015 The Coq development team, INRIA, CNRS, University +Copyright 1999-2016 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by @@ -55,6 +55,8 @@ QUICK INSTALLATION PROCEDURE. 1. ./configure 2. make 3. make install (you may need superuser rights) +4. make clean + INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= @@ -130,13 +132,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). make - to compile Coq in the best OCaml mode available (native-code if supported, - bytecode otherwise). + to compile Coq in Objective Caml bytecode (and native-code if supported). This will compile the entire system. This phase can take more or less time, - depending on your architecture and is fairly verbose. On a multi-core machine, - it is recommended to compile in parallel, via make -jN where N is your number - of cores. + depending on your architecture and is fairly verbose. 6- You can now install the Coq system. Executables, libraries, manual pages and emacs mode are copied in some standard places of your system, defined at @@ -152,19 +151,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -7- Optionally, you could build the bytecode version of Coq via: - - make byte - - and install it via - - make install-byte - - This version is quite slower than the native code version of Coq, but could - be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml - toplevel accessible via the Drop command. - -8- You can now clean all the sources. (You can even erase them.) +7- You can now clean all the sources. (You can even erase them.) make clean @@ -202,14 +189,11 @@ THE AVAILABLE COMMANDS. coqtop The Coq toplevel coqc The Coq compiler - Under architecture where ocamlopt is available, coqtop is the native code - version of Coq. On such architecture, you could additionally request - the build of the bytecode version of Coq via 'make byte' and install it via - 'make install-byte'. This will create an extra binary named coqtop.byte, - that could be used for debugging purpose. If native code isn't available, - coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte. - coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop - and coqc selects a particular binary. + Under architecture where ocamlopt is available, there are actually two + binaries for the interactive system, coqtop.byte and coqtop (respectively + bytecode and native code versions of Coq). coqtop is a link to coqtop.byte + otherwise. coqc also invokes the fastest version of Coq. Options -opt and + -byte to coqtop and coqc selects a particular binary. * `coqtop' launches Coq in the interactive mode. By default it loads basic logical definitions and tactics from the Init directory. @@ -109,17 +109,16 @@ NOARG: world .PHONY: NOARG help noconfig submake help: - @echo "Please use either:" + @echo "Please use either" @echo " ./configure" @echo " make world" @echo " make install" @echo " make clean" @echo "or make archclean" + @echo @echo "For make to be verbose, add VERBOSE=1" - @echo "Bytecode compilation is now a separate target:" - @echo " make byte" - @echo " make install-byte" - @echo "Please do mix bytecode and native targets in the same make -j" + @echo + @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1" UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES @@ -160,7 +159,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean clean: objclean cruftclean depclean docclean devdocclean @@ -221,9 +220,6 @@ clean-ide: ml4clean: rm -f $(GENML4FILES) -ml4depclean: - find . -name '*.ml4.d' | xargs rm -f - depclean: find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f diff --git a/Makefile.build b/Makefile.build index 90834ec8c9..95df69c2dc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -10,6 +10,40 @@ # some variables. ########################################################################### +# User-customizable variables +########################################################################### + +# The following variables could be modified via the command-line of make, +# either with the syntax 'make XYZ=1' or 'XYZ=1 make' + +# To see the actual commands launched by make instead of shortened versions, +# set this variable to 1 (or any non-empty value): +VERBOSE ?= + +# If set to 1 (or non-empty) then *.ml files corresponding to *.ml4 files +# will be generated in a human-readable format rather than in a binary format. +READABLE_ML4 ?= + +# When non-empty, a time command is performed at each .v compilation. +# To collect compilation timings of .v and import them in a spreadsheet, +# you could hence consider: make TIMED=1 2> timings.csv +TIMED ?= + +# When $(TIMED) is set, the time command used by default is $(STDTIME) +# (see below), unless the following variable is non-empty. For instance, +# it could be set to "'/usr/bin/time -p'". +TIMECMD ?= + +# Non-empty skips the update of all dependency .d files: +NO_RECALC_DEPS ?= + +# Non-empty runs the checker on all produced .vo files: +VALIDATE ?= + +# Is "-xml" when building XML library: +COQ_XML ?= + +########################################################################### # Default starting rule ########################################################################### @@ -17,16 +51,9 @@ world: coq coqide documentation revision -coq: coqlib coqbinaries tools +coq: coqlib coqbinaries tools printers -# Note: 'world' do not build the bytecode binaries anymore. -# For that, you can use the 'byte' rule. Native and byte compilations -# shouldn't be done in a same make -j... run, otherwise both ocamlc and -# ocamlopt might race for access to the same .cmi files. - -byte: coqbyte coqide-byte pluginsbyte printers - -.PHONY: world coq byte +.PHONY: world coq ########################################################################### # Includes @@ -64,41 +91,17 @@ DEPENDENCIES := \ # Compilation options ########################################################################### -# Variables meant to be modifiable via the command-line of make - -VERBOSE= -NO_RECOMPILE_ML4= -NO_RECALC_DEPS= -READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary -VALIDATE= -COQ_XML= # is "-xml" when building XML library - -TIMED= # non-empty will activate a default time command - # when compiling .v (see $(STDTIME) below) - -TIMECMD= # if you prefer a specific time command instead of $(STDTIME) - # e.g. "'time -p'" +# Default timing command +STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" -# NB: if you want to collect compilation timings of .v and import them -# in a spreadsheet, I suggest something like: -# make TIMED=1 2> timings.csv +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # NB: do not use a variable named TIME, since this variable controls # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile - -# The SHOW and HIDE variables control whether make will echo complete commands -# or only abbreviated versions. -# Quiet mode is ON by default except if VERBOSE=1 option is given to make - -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) +BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -152,7 +155,7 @@ else CAMLP4USE=-D$(CAMLVERSION) endif -PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 +PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) SYSMOD:=str unix dynlink threads SYSCMA:=$(addsuffix .cma,$(SYSMOD)) @@ -169,6 +172,13 @@ endif # Infrastructure for the rest of the Makefile ########################################################################### +# The SHOW and HIDE variables control whether make will echo complete commands +# or only abbreviated versions. +# Quiet mode is ON by default except if VERBOSE=1 option is given to make + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + define order-only-template ifeq "order-only" "$(1)" ORDER_ONLY_SEP:=| @@ -181,7 +191,7 @@ ifndef ORDER_ONLY_SEP $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.)) endif -VO_TOOLS_DEP := $(COQTOPBEST) +VO_TOOLS_DEP := $(COQTOPEXE) ifdef COQ_XML VO_TOOLS_DEP += $(COQDOC) endif @@ -189,13 +199,8 @@ ifdef VALIDATE VO_TOOLS_DEP += $(CHICKEN) endif -ifdef NO_RECALC_DEPS - D_DEPEND_BEFORE_SRC:=| - D_DEPEND_AFTER_SRC:= -else - D_DEPEND_BEFORE_SRC:= - D_DEPEND_AFTER_SRC:=| -endif +D_DEPEND_BEFORE_SRC := $(if $(NO_RECALC_DEPS),|,) +D_DEPEND_AFTER_SRC := $(if $(NO_RECALC_DEPS),,|) ## When a rule redirects stdout of a command to the target file : cmd > $@ ## then the target file will be created even if cmd has failed. @@ -320,11 +325,11 @@ grammar/%.cmi: grammar/%.mli # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -.PHONY: coqbinaries coqbyte +.PHONY: coqbinaries -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \ + $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE) -coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) @@ -510,13 +515,18 @@ test-suite: world $(ALLSTDLIB).v # For plugin packs +# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's +# apparently no way to avoid that (no -intf-suffix hack as below). +# We at least ensure that these two commands won't run at the same time, by a fake +# dependency from the packed .cmx to the packed .cmo. + %.cmo: %.mlpack $(SHOW)'OCAMLC -pack -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -%.cmx: %.mlpack +%.cmx: %.mlpack %.cmo $(SHOW)'OCAMLOPT -pack -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^) COND_BYTEFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) @@ -532,6 +542,27 @@ COND_OPTFLAGS= \ $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< +## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. +## This can lead to nasty things with make -j. To avoid that: +## 1) We make .cmx always depend on .cmi +## 2) This .cmi will be created from the .mli, or trigger the compilation of the +## .cmo if there's no .mli (see rule below about MLWITHOUTMLI) +## 3) We tell ocamlopt to use the .cmi as the interface source file. With this +## hack, everything goes as if there is a .mli, and the .cmi is preserved +## and the .cmx is checked with respect to this .cmi + +HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi) + +define diff + $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) +endef + +MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml)) + +$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case + +$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo + # NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep # The only exceptions are the sources of the csdpcert binary. # To avoid warnings, we set them manually here: @@ -542,11 +573,11 @@ plugins/micromega/csdpcert_FORPACK:= plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< %.cmx: %.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< %.cmxs: %.cmx $(SHOW)'OCAMLOPT -shared -o $@' @@ -631,7 +662,7 @@ endif %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) ########################################################################### diff --git a/Makefile.checker b/Makefile.checker index 435d8e8f64..3ea0baced6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -71,7 +71,7 @@ checker/%.cmo: checker/%.ml checker/%.cmx: checker/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $< + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $< md5chk: $(SHOW)'MD5SUM cic.mli' diff --git a/Makefile.common b/Makefile.common index aacd801b52..49fe1fd939 100644 --- a/Makefile.common +++ b/Makefile.common @@ -41,26 +41,10 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) # Object and Source files ########################################################################### -ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) - # static link of plugins, do not mention them in .v.d - DYNDEP:=-dyndep no -else - DYNDEP:=-dyndep var -endif - -# Which coqtop do we use to build .vo file ? The best ;-) -# Note: $(BEST) could be overridden by the user if a byte build is desired -# Note: coqdep -dyndep var will use $(DYNOBJ) and $(DYNLIB) extensions -# for Declare ML Module files. - -ifeq ($(BEST),opt) -COQTOPBEST:=$(COQTOPEXE) -DYNOBJ:=.cmxs -DYNLIB:=.cmxs +ifeq ($(HASNATDYNLINK)-$(BEST),true-opt) + DEPNATDYN:= else -COQTOPBEST:=$(COQTOPBYTE) -DYNOBJ:=.cmo -DYNLIB:=.cma + DEPNATDYN:=-natdynlink no endif INSTALLBIN:=install diff --git a/Makefile.dev b/Makefile.dev index 26092e8dc8..501a7744a1 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -134,7 +134,7 @@ ltac: ltac/ltac.cma ###################### init: $(filter theories/Init/%, $(THEORIESVO)) -logic: $(filter theories/Logic/%, %(THEORIESVO)) +logic: $(filter theories/Logic/%, $(THEORIESVO)) arith: $(filter theories/Arith/%, $(THEORIESVO)) bool: $(filter theories/Bool/%, $(THEORIESVO)) parith: $(filter theories/PArith/%, $(THEORIESVO)) diff --git a/Makefile.ide b/Makefile.ide index 0cfbdeb4e0..48a269ab7c 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -61,30 +61,23 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) # CoqIde special targets ########################################################################### -.PHONY: coqide coqide-opt coqide-byte coqide-files -.PHONY: ide-toploop ide-byteloop ide-optloop +.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files +.PHONY: ide-toploop # target to build CoqIde -coqide: coqide-files coqide-opt theories/Init/Prelude.vo +coqide: coqide-files coqide-binaries theories/Init/Prelude.vo -ifeq ($(HASCOQIDE),opt) -coqide-opt: $(COQIDE) ide-toploop -else -coqide-opt: ide-toploop -endif - -ifeq ($(HASCOQIDE),no) -coqide-byte: ide-byteloop +coqide-binaries: coqide-$(HASCOQIDE) ide-toploop +coqide-no: +coqide-byte: $(COQIDEBYTE) $(COQIDE) +coqide-opt: $(COQIDEBYTE) $(COQIDE) +coqide-files: $(IDEFILES) +ifeq ($(BEST),opt) +ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) else -coqide-byte: $(COQIDEBYTE) ide-byteloop +ide-toploop: $(IDETOPLOOPCMA) endif -coqide-files: $(IDEFILES) - -ide-byteloop: $(IDETOPLOOPCMA) -ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs) -ide-toploop: ide-$(BEST)loop - ifeq ($(HASCOQIDE),opt) $(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' @@ -116,14 +109,14 @@ ide/%.cmo: ide/%.ml ide/%.cmx: ide/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $< #################### ## Install targets #################### -.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte +.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles ifeq ($(HASCOQIDE),no) install-coqide: install-ide-toploop @@ -131,26 +124,20 @@ else install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles endif -# Apparently, coqide.byte is not meant to be installed - -install-ide-byte: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ - install-ide-bin: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) install-ide-toploop: + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ ifeq ($(BEST),opt) $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ endif install-ide-devfiles: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) \ + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) diff --git a/Makefile.install b/Makefile.install index b4aad7bdd4..4dad8cf0d4 100644 --- a/Makefile.install +++ b/Makefile.install @@ -61,26 +61,15 @@ endif install-coq: install-binaries install-library install-coq-info install-devfiles -ifeq ($(BEST),byte) -install-coq: install-byte -endif - install-binaries: install-tools $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ ifeq ($(BEST),opt) $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ endif -install-byte: install-ide-byte - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR) - $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS) -ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) -endif install-tools: $(MKDIR) $(FULLBINDIR) @@ -104,7 +93,7 @@ install-devfiles: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) @@ -112,8 +101,11 @@ endif install-library: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(MKDIR) $(FULLCOQLIB)/user-contrib +ifndef CUSTOM + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) diff --git a/checker/inductive.ml b/checker/inductive.ml index cb344c7fd6..c4ffc141ff 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -989,6 +989,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") | Sort _ -> assert (l = []) @@ -998,8 +1002,6 @@ let check_one_fix renv recpos trees def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - | Proj (p, c) -> check_rec_call renv [] c - and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body diff --git a/configure.ml b/configure.ml index 06d8e713b3..d152c406ee 100644 --- a/configure.ml +++ b/configure.ml @@ -13,7 +13,7 @@ open Printf let coq_version = "trunk" let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of -three non-negative, period-separed integers [...]" *) +three non-negative, period-separated integers [...]" *) let vo_magic = 8511 let state_magic = 58511 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; @@ -809,7 +809,8 @@ let strip = (** * md5sum command *) let md5sum = - if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum" + if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"] + then "md5 -q" else "md5sum" (** * Documentation : do we have latex, hevea, ... *) @@ -934,7 +935,7 @@ let print_summary () = pr "\n"; pr " Architecture : %s\n" arch; if operating_system <> "" then - pr " Operating system : %s\n" operating_system; + pr " Operating system : %s\n" operating_system; pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags); pr " Other bytecode link flags : %s\n" custom_flag; pr " OS dependent libraries : %s\n" osdeplibs; diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index b0f9ae2c38..fcee79e07e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -190,8 +190,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id Now it is represented as: - Context.Rel.t = LocalAssum of Names.Name.t * Constr.t - | LocalDef of Names.Name.t * Constr.t * Constr.t + Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t + | LocalDef of Names.Name.t * Constr.t * Constr.t - Originally, named-context was represented as: @@ -199,8 +199,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id Now it is represented as: - Context.Named.t = LocalAssum of Names.Id.t * Constr.t - | LocalDef of Names.Id.t * Constr.t * Constr.t + Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t + | LocalDef of Names.Id.t * Constr.t * Constr.t - The various EXTEND macros do not handle specially the Coq-defined entries anymore. Instead, they just output a name that have to exist in the scope diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 023835af76..e09477014b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,8 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pp x = Feedback.msg_notice x -let pppp x = Feedback.msg_notice x +let pp x = Pp.pp_with !Pp_control.std_ft x (** Future printer *) @@ -316,7 +315,7 @@ let constr_display csr = | Anonymous -> "Anonymous" in - Feedback.msg_notice (str (term_display csr) ++fnl ()) + pp (str (term_display csr) ++fnl ()) open Format;; @@ -514,7 +513,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (CErrors.print e) + e -> pp (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -530,7 +529,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (CErrors.print e) + e -> pp (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 6a8bda35d6..919e7b5cdc 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -87,7 +87,7 @@ is restored when the current \emph{section} ends. \item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\ This command switches {\rm\sl flag} off. The original state of {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl flag} is switched on when the file is +if set in a file, {\rm\sl flag} is switched off when the file is {\tt Require}-d. \end{Variants} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index e91480ded3..92107b750b 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -589,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := (t at level 39). \end{coq_example*} +Recursive patterns can occur several times on the right-hand side. +Here is an example: + +\begin{coq_example*} +Notation "[> a , .. , b <]" := + (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). +\end{coq_example*} + Notations with recursive patterns can be reserved like standard notations, they can also be declared within interpretation scopes (see section \ref{scopes}). @@ -634,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders: \begin{coq_example*} Notation "'mylet' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (x closed binder, y closed binder, at level 200, right associativity). + (at level 200, x closed binder, y closed binder, right associativity). +\end{coq_example*} + +A recursive pattern for binders can be used in position of a recursive +pattern for terms. Here is an example: + +\begin{coq_example*} +Notation ``'FUNAPP' x .. y , f'' := + (fun x => .. (fun y => (.. (f x) ..) y ) ..) + (at level 200, x binder, y binder, right associativity). \end{coq_example*} \subsection{Summary} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index fb45777e7f..9216c81fcd 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -616,5 +616,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq84.v theories/Compat/Coq85.v + theories/Compat/Coq86.v </dd> </dl> diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b63391913f..bd86f4bd27 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -290,78 +290,107 @@ let make_pure_subst evi args = * we have the property that u and phi(t) are convertible in env. *) +let csubst_subst (k, s) c = + let rec subst n c = match Constr.kind c with + | Rel m -> + if m <= n then c + else if m - n <= k then Int.Map.find (k - m + n) s + else mkRel (m - k) + | _ -> Constr.map_with_binders succ subst n c + in + if k = 0 then c else subst 0 c + let subst2 subst vsubst c = - substl subst (replace_vars vsubst c) + csubst_subst subst (replace_vars vsubst c) -let push_rel_context_to_named_context env typ = - (* compute the instances relative to the named context and rel_context *) +let next_ident_away id avoid = + let avoid id = Id.Set.mem id avoid in + next_ident_away_from id avoid + +let next_name_away na avoid = + let avoid id = Id.Set.mem id avoid in + let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in + next_ident_away_from id avoid + +type csubst = int * Constr.t Int.Map.t + +let empty_csubst = (0, Int.Map.empty) + +type ext_named_context = + csubst * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + +let push_var id (n, s) = + let s = Int.Map.add n (mkVar id) s in + (succ n, s) + +let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open Context.Named.Declaration in - let ids = List.map get_id (named_context env) in - let inst_vars = List.map mkVar ids in - let inst_rels = List.rev (rel_list 0 (nb_rel env)) in let replace_var_named_declaration id0 id decl = let id' = get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in decl |> set_id id' |> map_constr (replace_vars vsubst) in - let replace_var_named_context id0 id env = - let nc = Environ.named_context env in - let nc' = List.map (replace_var_named_declaration id0 id) nc in - Environ.reset_with_named_context (val_of_named_context nc') env - in let extract_if_neq id = function | Anonymous -> None | Name id' when id_ord id id' = 0 -> None | Name id' -> Some id' in + let open Context.Rel.Declaration in + let (na, c, t) = to_tuple decl in + let open Context.Named.Declaration in + let id = + (* ppedrot: we want to infer nicer names for the refine tactic, but + keeping at the same time backward compatibility in other code + using this function. For now, we only attempt to preserve the + old behaviour of Program, but ultimately, one should do something + about this whole name generation problem. *) + if Flags.is_program_mode () then next_name_away na avoid + else + (** id_of_name_using_hdchar only depends on the rel context which is empty + here *) + next_ident_away (id_of_name_using_hdchar empty_env t na) avoid + in + match extract_if_neq id na with + | Some id0 when not (is_section_variable id0) -> + (* spiwack: if [id<>id0], rather than introducing a new + binding named [id], we will keep [id0] (the name given + by the user) and rename [id0] into [id] in the named + context. Unless [id] is a section variable. *) + let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in + let vsubst = (id0,mkVar id)::vsubst in + let d = match c with + | None -> LocalAssum (id0, subst2 subst vsubst t) + | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) + in + let nc = List.map (replace_var_named_declaration id0 id) nc in + (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) + | _ -> + (* spiwack: if [id0] is a section variable renaming it is + incorrect. We revert to a less robust behaviour where + the new binder has name [id]. Which amounts to the same + behaviour than when [id=id0]. *) + let d = match c with + | None -> LocalAssum (id, subst2 subst vsubst t) + | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) + in + (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) + +let push_rel_context_to_named_context env typ = + (* compute the instances relative to the named context and rel_context *) + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + let inst_vars = List.map mkVar ids in + let inst_rels = List.rev (rel_list 0 (nb_rel env)) in (* move the rel context to a named context and extend the named instance *) (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, vsubst, _, env) = - Context.Rel.fold_outside - (fun decl (subst, vsubst, avoid, env) -> - let open Context.Rel.Declaration in - let na = get_name decl in - let c = get_value decl in - let t = get_type decl in - let open Context.Named.Declaration in - let id = - (* ppedrot: we want to infer nicer names for the refine tactic, but - keeping at the same time backward compatibility in other code - using this function. For now, we only attempt to preserve the - old behaviour of Program, but ultimately, one should do something - about this whole name generation problem. *) - if Flags.is_program_mode () then next_name_away na avoid - else next_ident_away (id_of_name_using_hdchar env t na) avoid - in - match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> - (* spiwack: if [id<>id0], rather than introducing a new - binding named [id], we will keep [id0] (the name given - by the user) and rename [id0] into [id] in the named - context. Unless [id] is a section variable. *) - let subst = List.map (replace_vars [id0,mkVar id]) subst in - let vsubst = (id0,mkVar id)::vsubst in - let d = match c with - | None -> LocalAssum (id0, subst2 subst vsubst t) - | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) - in - let env = replace_var_named_context id0 id env in - (mkVar id0 :: subst, vsubst, id::avoid, push_named d env) - | _ -> - (* spiwack: if [id0] is a section variable renaming it is - incorrect. We revert to a less robust behaviour where - the new binder has name [id]. Which amounts to the same - behaviour than when [id=id0]. *) - let d = match c with - | None -> LocalAssum (id, subst2 subst vsubst t) - | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) - in - (mkVar id :: subst, vsubst, id::avoid, push_named d env) - ) - (rel_context env) ~init:([], [], ids, env) in - (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + Context.Rel.fold_outside push_rel_decl_to_named_context + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in + (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) (*------------------------------------* * Entry points to define new evars * diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 111d0f3e8c..c0c81442d5 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,8 +199,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types +type csubst + +val empty_csubst : csubst +val csubst_subst : csubst -> Constr.t -> Constr.t + +type ext_named_context = + csubst * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + +val push_rel_decl_to_named_context : + Context.Rel.Declaration.t -> ext_named_context -> ext_named_context + val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * constr list * (identifier*constr) list + named_context_val * types * constr list * csubst * (identifier*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index 196f44760a..e4b174bcb3 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -790,16 +790,16 @@ let merge_universe_subst evd subst = let with_context_set ?loc rigid d (a, ctx) = (merge_context_set ?loc rigid d ctx, a) -let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_level_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?loc ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in +let new_sort_variable ?loc ?name rigid d = + let (d', u) = new_univ_variable ?loc rigid ?name d in (d', Type u) let add_global_univ d u = diff --git a/engine/evd.mli b/engine/evd.mli index d6cf83525c..9424145113 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -508,9 +508,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map diff --git a/engine/proofview.ml b/engine/proofview.ml index 905e1c0792..576569cf5f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -366,8 +366,9 @@ let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in CErrors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) - | _ -> raise CErrors.Unhandled + (str "No such " ++ str (String.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) + | _ -> raise CErrors.Unhandled end (** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where diff --git a/engine/sigma.ml b/engine/sigma.ml index c7b0bb5a50..9381a33af1 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,16 +36,16 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) -let new_univ_level_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in +let new_univ_level_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) -let new_univ_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in +let new_univ_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) -let new_sort_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in +let new_sort_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) let fresh_sort_in_family ?loc ?rigid env sigma s = diff --git a/engine/sigma.mli b/engine/sigma.mli index aaf603efd8..7473a251b7 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -68,11 +68,11 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_sort_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 2ec6430fdd..a1b3f4f255 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -111,8 +111,8 @@ let declare_tactic loc s c cl = match cl with declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in - Tacenv.register_ml_tactic $se$ [|$tac$|]; - Mltop.declare_cache_obj obj $plugin_name$; } >> + let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in + Mltop.declare_cache_obj obj $plugin_name$ } >> ] | _ -> (** Otherwise we add parsing and printing rules to generate a call to a diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 18557ab6b4..50b3f2c0a0 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -339,8 +339,11 @@ object(self) method private show_goals_aux ?(move_insert=false) () = Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin - buffer#place_cursor ~where:self#get_start_of_input; - script#recenter_insert; + let dest = self#get_start_of_input in + if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin + buffer#place_cursor ~where:dest; + script#recenter_insert + end end; Coq.bind (Coq.goals ~logger:messages#push ()) (function | Fail x -> self#handle_failure_aux ~move_insert x diff --git a/ide/ideutils.ml b/ide/ideutils.ml index f0698a54a3..fe69be9e48 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -112,6 +112,24 @@ let try_convert s = "(* Fatal error: wrong encoding in input. \ Please choose a correct encoding in the preference panel.*)";; +let export file_name s = + let oc = open_out_bin file_name in + let ending = line_ending#get in + let is_windows = ref false in + for i = 0 to String.length s - 1 do + match s.[i] with + | '\r' -> is_windows := true + | '\n' -> + begin match ending with + | `DEFAULT -> + if !is_windows then (output_char oc '\r'; output_char oc '\n') + else output_char oc '\n' + | `WINDOWS -> output_char oc '\r'; output_char oc '\n' + | `UNIX -> output_char oc '\n' + end + | c -> output_char oc c + done; + close_out oc let try_export file_name s = let s = @@ -134,11 +152,7 @@ let try_export file_name s = Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); s in - try - let oc = open_out file_name in - output_string oc s; - close_out oc; - true + try export file_name s; true with e -> Minilib.log (Printexc.to_string e);false type timer = { run : ms:int -> callback:(unit->bool) -> unit; diff --git a/ide/preferences.ml b/ide/preferences.ml index 3a33bbb1d8..3241a962dc 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -121,6 +121,18 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] + +let line_end_of_string = function +| "unix" -> `UNIX +| "windows" -> `WINDOWS +| _ -> `DEFAULT + +let line_end_to_string = function +| `UNIX -> "unix" +| `WINDOWS -> "windows" +| `DEFAULT -> "default" + let use_default_doc_url = "(automatic)" module Repr = @@ -381,6 +393,10 @@ let stop_before = let reset_on_tab_switch = new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool) +let line_ending = + let repr = Repr.custom line_end_to_string line_end_of_string in + new preference ~name:["line_ending"] ~init:`DEFAULT ~repr + let vertical_tabs = new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool) @@ -818,6 +834,15 @@ let configure ?(apply=(fun () -> ())) () = (string_of_inputenc encoding#get) in + let line_ending = + combo + "EOL character" + ~f:(fun s -> line_ending#set (line_end_of_string s)) + ~new_allowed:false + ["unix"; "windows"; "default"] + (line_end_to_string line_ending#get) + in + let source_style = combo "Highlighting style:" ~f:source_style#set ~new_allowed:false @@ -973,7 +998,7 @@ let configure ?(apply=(fun () -> ())) () = Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings; + encodings; line_ending; ]); Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; diff --git a/ide/preferences.mli b/ide/preferences.mli index 426b0a328e..801869d1dc 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -11,6 +11,7 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] type tag = { tag_fg_color : string option; @@ -79,6 +80,7 @@ val window_height : int preference val auto_complete : bool preference val stop_before : bool preference val reset_on_tab_switch : bool preference +val line_ending : line_ending preference val vertical_tabs : bool preference val opposite_tabs : bool preference val background_color : string preference diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7476871890..e71daef999 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -848,10 +848,11 @@ and extern_local_binder scopes vars = function | (Inr p,bk,Some bd,ty)::l -> assert false | (Inr p,bk,None,ty)::l -> - let ty = extern_typ scopes vars ty in + let ty = + if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l) + (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1c50253d9c..fb1baae0a8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -481,9 +481,14 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let bl' = List.map (fun a -> BDRawDef a) bl' in env, bl' @ bl | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in + let indef = intern env def in + let term, ty = + match indef with + | GCast (loc, b, Misctypes.CastConv t) -> b, t + | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) + in (push_name_env lvar (impls_term_list indef) env locna, - (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl) + (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl) | LocalPattern (loc,p,ty) -> let tyc = match ty with @@ -599,31 +604,52 @@ let rec subordinate_letins intern letins = function | [] -> letins,[] -let rec subst_iterator y t = function - | GVar (_,id) as x -> if Id.equal id y then t else x - | x -> map_glob_constr (subst_iterator y t) x +let terms_of_binders bl = + let rec term_of_pat = function + | PatVar (loc,Name id) -> CRef (Ident (loc,id), None) + | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term." + | PatCstr (loc,c,l,_) -> + let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in + let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in + let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in + CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in + let rec extract_variables = function + | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l + | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l + | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term." + | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l + | [] -> [] in + extract_variables bl let instantiate_notation_constr loc intern ntnvars subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in - let rec aux (terms,binderopt as subst') (renaming,env) c = + let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with + | NVar id when Id.equal id ldots_var -> Option.get terminopt | NVar id -> subst_var subst' (renaming, env) id - | NList (x,_,iter,terminator,lassoc) -> - (try + | NList (x,y,iter,terminator,lassoc) -> + let l,(scopt,subscopes) = (* All elements of the list are in scopes (scopt,subscopes) *) - let (l,(scopt,subscopes)) = Id.Map.find x termlists in - let termin = aux subst' subinfos terminator in - let fold a t = - let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in - subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter) - in - List.fold_right fold (if lassoc then List.rev l else l) termin - with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + try + let l,scopes = Id.Map.find x termlists in + (if lassoc then List.rev l else l),scopes + with Not_found -> + try + let (bl,(scopt,subscopes)) = Id.Map.find x binders in + let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in + terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[]) + with Not_found -> + anomaly (Pp.str "Inconsistent substitution of recursive notation") in + let termin = aux (terms,None,None) subinfos terminator in + let fold a t = + let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in + aux (nterms,None,Some t) subinfos iter + in + List.fold_right fold l termin | NHole (knd, naming, arg) -> let knd = match knd with | Evar_kinds.BinderType (Name id as na) -> @@ -658,16 +684,15 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = Some arg in GHole (loc, knd, naming, arg) - | NBinderList (x,_,iter,terminator) -> + | NBinderList (x,y,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in let letins,bl = subordinate_letins intern [] bl in - let termin = aux subst' (renaming,env) terminator in + let termin = aux (terms,None,None) (renaming,env) terminator in let res = List.fold_left (fun t binder -> - subst_iterator ldots_var t - (aux (terms,Some(x,binder)) subinfos iter)) + aux (terms,Some(y,binder),Some t) subinfos iter) termin bl in make_letins letins res with Not_found -> @@ -695,7 +720,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = | t -> glob_constr_of_notation_constr_with_binders loc (traverse_binder subst avoid) (aux subst') subinfos t - and subst_var (terms, binderopt) (renaming, env) id = + and subst_var (terms, _binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try @@ -708,7 +733,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) GVar (loc,id) - in aux (terms,None) infos c + in aux (terms,None,None) infos c let split_by_type ids = List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> @@ -1324,7 +1349,7 @@ let drop_notations_pattern looked_for = RCPatCstr (loc, g, List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) - | NList (x,_,iter,terminator,lassoc) -> + | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); (try @@ -1332,7 +1357,7 @@ let drop_notations_pattern looked_for = let (l,(scopt,subscopes)) = Id.Map.find x substlist in let termin = in_not top loc scopes fullsubst [] terminator in List.fold_right (fun a t -> - let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in + let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in let u = in_not false loc scopes (nsubst, substlist) [] iter in subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) termin @@ -1609,11 +1634,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (merge_impargs l args) loc | CRecord (loc, fs) -> - let fields = - sort_fields ~complete:true loc fs - (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None)) - in - begin + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + let fields = + sort_fields ~complete:true loc fs + (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st), + Misctypes.IntroAnonymous, None)) + in + begin match fields with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> @@ -1683,7 +1710,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k, naming, solve) -> let k = match k with - | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true) + | None -> + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + Evar_kinds.QuestionMark st | Some k -> k in let solve = match solve with @@ -2030,11 +2059,13 @@ let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> + let t' = + if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t + else t + in + let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t' = locate_if_hole (loc_of_glob_constr t) na t in - let t = - understand_tcc_evars env evdref ~expected_type:IsType t' in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2044,8 +2075,8 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_judgment_tcc env evdref b in - let d = LocalDef (na, c.uj_val, c.uj_type) in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) in (env, par), impls diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 198bd2216a..f3e0682bd7 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -237,7 +237,9 @@ let check_is_hole id = function GHole _ -> () | t -> strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") -let compare_recursive_parts found f (iterator,subc) = +let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' + +let compare_recursive_parts found f f' (iterator,subc) = let diff = ref None in let terminator = ref None in let rec aux c1 c2 = match c1,c2 with @@ -284,16 +286,26 @@ let compare_recursive_parts found f (iterator,subc) = user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> - let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in + let newfound,x,y,lassoc = + if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || + List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) + then + !found,x,y,lassoc + else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) || + List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found) + then + !found,y,x,not lassoc + else + (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in let iterator = - f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator - else iterator) in + f' (if lassoc then iterator + else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,None) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in - let iterator = f iterator in + let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; NBinderList (x,y,iterator,f (Option.get !terminator)) @@ -305,7 +317,7 @@ let notation_constr_and_vars_of_glob_constr a = let rec aux c = let keepfound = !found in (* n^2 complexity but small and done only once per notation *) - try compare_recursive_parts found aux' (split_at_recursive_part c) + try compare_recursive_parts found aux aux' (split_at_recursive_part c) with Not_found -> found := keepfound; match c with @@ -357,8 +369,6 @@ let notation_constr_and_vars_of_glob_constr a = (* Side effect *) t, !found -let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' - let check_variables nenv (found,foundrec,foundrecbinding) = let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in @@ -585,6 +595,10 @@ let rec alpha_var id1 id2 = function | _::idl -> alpha_var id1 id2 idl | [] -> Id.equal id1 id2 +let alpha_rename alpmetas v = + if alpmetas == [] then v + else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match + let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = (* Check that no capture of binding variables occur *) (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..." @@ -610,16 +624,29 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the choice of exact variable be done there; but again, this would be a non-trivial refinement *) - if alpmetas != [] then raise No_match; + let v = alpha_rename alpmetas v in (* TODO: handle the case of multiple occs in different scopes *) ((var,v)::terms,onlybinders,termlists,binderlists) +let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl = + if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match; + let vl = List.map (alpha_rename alpmetas) vl in + (terms,onlybinders,(var,vl)::termlists,binderlists) + let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) (terms,(var,v)::onlybinders,termlists,binderlists) let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = - (terms,onlybinders,termlists,(x,List.rev bl)::binderlists) + (terms,onlybinders,termlists,(x,bl)::binderlists) + +let rec pat_binder_of_term = function + | GVar (loc, id) -> PatVar (loc, Name id) + | GApp (loc, GRef (_,ConstructRef cstr,_), l) -> + let nparams = Inductiveops.inductive_nparams (fst cstr) in + let _,l = List.chop nparams l in + PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous) + | _ -> raise No_match let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try @@ -630,10 +657,53 @@ let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in add_env alp sigma var v | _, _ -> - if glob_constr_eq v v' then sigma + if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma else raise No_match with Not_found -> add_env alp sigma var v +let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl = + try + let vl' = Id.List.assoc var termlists in + let unify_term v v' = + match v, v' with + | GHole _, _ -> v' + | _, GHole _ -> v + | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in + let rec unify vl vl' = + match vl, vl' with + | [], [] -> [] + | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl' + | _ -> raise No_match in + let vl = unify vl vl' in + let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in + add_termlist_env alp sigma var vl + with Not_found -> add_termlist_env alp sigma var vl + +let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = + try + match Id.List.assoc var terms with + | GVar (_,id') -> + (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), + sigma + | _ -> anomaly (str "A term which can be a binder has to be a variable") + with Not_found -> + (* The matching against a term allowing to find the instance has not been found yet *) + (* If it will be a different name, we shall unfortunately fail *) + (* TODO: look at the consequences for alp *) + alp, add_env alp sigma var (GVar (Loc.ghost,id)) + +let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = + try + let v' = Id.List.assoc var onlybinders in + match v' with + | Anonymous -> + (* Should not occur, since the term has to be bound upwards *) + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + add_binding_env alp sigma var (Name id) + | Name id' -> + if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match + with Not_found -> add_binding_env alp sigma var (Name id) + let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try let v' = Id.List.assoc var onlybinders in @@ -647,6 +717,109 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var else (fst alp,(id1,id2)::snd alp),sigma with Not_found -> alp, add_binding_env alp sigma var v +let rec map_cases_pattern_name_left f = function + | PatVar (loc,na) -> PatVar (loc,f na) + | PatCstr (loc,c,l,na) -> PatCstr (loc,c,List.map_left (map_cases_pattern_name_left f) l,f na) + +let rec fold_cases_pattern_eq f x p p' = match p, p' with + | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na) + | PatCstr (loc,c,l,na), PatCstr (_,c',l',na') when eq_constructor c c' -> + let x,l = fold_cases_pattern_list_eq f x l l' in + let x,na = f x na na' in + x, PatCstr (loc,c,l,na) + | _ -> failwith "Not equal" + +and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with + | [], [] -> x, [] + | p::pl, p'::pl' -> + let x, p = fold_cases_pattern_eq f x p p' in + let x, pl = fold_cases_pattern_list_eq f x pl pl' in + x, p :: pl + | _ -> assert false + +let rec cases_pattern_eq p1 p2 = match p1, p2 with +| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2 +| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 +| _ -> false + +let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl = + let bl = List.rev bl in + try + let bl' = Id.List.assoc var binderlists in + let unify_name alp na na' = + match na, na' with + | Anonymous, na' -> alp, na' + | na, Anonymous -> alp, na + | Name id, Name id' -> + if Id.equal id id' then alp, na' + else (fst alp,(id,id')::snd alp), na' in + let unify_pat alp p p' = + try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in + let unify_term alp v v' = + match v, v' with + | GHole _, _ -> v' + | _, GHole _ -> v + | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in + let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in + let unify_binder alp b b' = + match b, b' with + | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> + let alp, na = unify_name alp na na' in + alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t') + | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) -> + let alp, na = unify_name alp na na' in + alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t') + | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) -> + let alp, p = unify_pat alp p p' in + alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') + | _ -> raise No_match in + let rec unify alp bl bl' = + match bl, bl' with + | [], [] -> alp, [] + | b :: bl, b' :: bl' -> + let alp,b = unify_binder alp b b' in + let alp,bl = unify alp bl bl' in + alp, b :: bl + | _ -> raise No_match in + let alp, bl = unify alp bl bl' in + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + alp, add_bindinglist_env sigma var bl + with Not_found -> + alp, add_bindinglist_env sigma var bl + +let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl = + try + let bl' = Id.List.assoc var binderlists in + let unify_id id na' = + match na' with + | Anonymous -> Name (rename_var (snd alp) id) + | Name id' -> + if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in + let unify_pat p p' = + if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p' + else raise No_match in + let unify_term_binder c b' = + match c, b' with + | GVar (_, id), (Inl na', bk', None, t') (* assum *) -> + (Inl (unify_id id na'), bk', None, t') + | c, (Inr p', bk', None, t') (* pattern *) -> + let p = pat_binder_of_term c in + (Inr (unify_pat p p'), bk', None, t') + | _ -> raise No_match in + let rec unify cl bl' = + match cl, bl' with + | [], [] -> [] + | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl' + | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl' + | _ -> raise No_match in + let bl = unify cl bl' in + let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in + add_bindinglist_env sigma var bl + with Not_found -> + anomaly (str "There should be a binder list bindings this list of terms") + let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 @@ -670,8 +843,8 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with bind_binding_env alp sigma id2 na1 | (Name id1,Name id2) when is_term_meta id2 metas -> (* We let the non-binding occurrence define the rhs and hence reason up to *) - (* alpha-conversion for the given occurrence of the name (see #)) *) - (fst alp,(id1,id2)::snd alp), sigma + (* alpha-conversion for the given occurrence of the name (see #4592)) *) + bind_term_as_binding_env alp sigma id2 id1 | (Anonymous,Name id2) when is_term_meta id2 metas -> (* We let the non-binding occurrence define the rhs *) alp, sigma @@ -691,8 +864,14 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function + | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + when islambda && Id.equal p e -> + match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b | GLambda (_,na,bk,t,b) when islambda -> match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b + | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + when not islambda && Id.equal p e -> + match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b | GProd (_,(Name _ as na),bk,t,b) when not islambda -> match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b | GLetIn (loc,na,c,b) when glue_letin_with_decls -> @@ -703,35 +882,51 @@ let rec match_iterated_binders islambda decls = function let remove_sigma x (terms,onlybinders,termlists,binderlists) = (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists) +let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) = + (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists) + let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas -let match_abinderlist_with_app match_fun metas sigma rest x iter termin = - let rec aux sigma acc rest = +let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas + +let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin = + let rec aux sigma bl rest = try - let (terms,_,_,binderlists as sigma) = match_fun (add_ldots_var metas) sigma rest iter in + let metas = add_ldots_var (add_meta_bindinglist y metas) in + let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in let rest = Id.List.assoc ldots_var terms in let b = - match Id.List.assoc x binderlists with [b] -> b | _ ->assert false + match Id.List.assoc y binderlists with [b] -> b | _ ->assert false in - let sigma = remove_sigma x (remove_sigma ldots_var sigma) in - aux sigma (b::acc) rest - with No_match when not (List.is_empty acc) -> - acc, match_fun metas sigma rest termin in - let bl,sigma = aux sigma [] rest in - add_bindinglist_env sigma x bl + let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in + aux sigma (b::bl) rest + with No_match when not (List.is_empty bl) -> + bl, rest, sigma in + let bl,rest,sigma = aux sigma [] rest in + let alp,sigma = bind_bindinglist_env alp sigma x bl in + match_fun alp metas sigma rest termin + +let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas -let match_alist match_fun metas sigma rest x iter termin lassoc = +let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = let rec aux sigma acc rest = try - let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in + let metas = add_ldots_var (add_meta_term y metas) in + let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in let rest = Id.List.assoc ldots_var terms in - let t = Id.List.assoc x terms in - let sigma = remove_sigma x (remove_sigma ldots_var sigma) in + let t = Id.List.assoc y terms in + let sigma = remove_sigma y (remove_sigma ldots_var sigma) in aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in - (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) + let l = if lassoc then l else List.rev l in + if is_bindinglist_meta x metas then + (* This is a recursive pattern for both bindings and terms; it is *) + (* registered for binders *) + bind_bindinglist_as_term_env alp sigma x l + else + bind_termlist_env alp sigma x l let does_not_come_from_already_eta_expanded_var = (* This is hack to avoid looping on a rule with rhs of the form *) @@ -750,46 +945,58 @@ let rec match_ inner u alp metas sigma a1 a2 = (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1 - | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> snd (bind_binding_env alp sigma id2 (Name id1)) + | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1 + | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1 (* Matching recursive notations for terms *) - | r1, NList (x,_,iter,termin,lassoc) -> - match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc + | r1, NList (x,y,iter,termin,lassoc) -> + match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) - | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])), - NBinderList (x,_,NLambda (Name id2,_,b2),(NVar v as termin)) when p = e -> - let decls = [(Inr cp,bk,None,t1)] in - match_in u alp metas (add_bindinglist_env sigma x decls) t termin + | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e -> + let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> + | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) - match_in u alp metas (add_bindinglist_env sigma x decls) b termin + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) - | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])), - NBinderList (x,_,NProd (Name id2,_,b2),(NVar v as termin)) when p = e -> - let decls = [(Inr cp,bk,None,t1)] in - match_in u alp metas (add_bindinglist_env sigma x decls) t termin + | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e -> + let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin - | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) + | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) when na1 != Anonymous -> let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) - match_in u alp metas (add_bindinglist_env sigma x decls) b termin + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin (* Matching recursive notations for binders: general case *) - | r, NBinderList (x,_,iter,termin) -> - match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin + | r, NBinderList (x,y,iter,termin) -> + match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin (* Matching individual binders as part of a recursive pattern *) + | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + NLambda (Name id,_,b2) + when is_bindinglist_meta id metas -> + let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in + match_in u alp metas sigma b1 b2 | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2 + let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + match_in u alp metas sigma b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) when is_bindinglist_meta id metas && na != Anonymous -> - match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2 + let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + match_in u alp metas sigma b1 b2 (* Matching compositionally *) | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma @@ -876,7 +1083,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then - alp, add_bindinglist_env sigma id [(Inl (Name id'),Explicit,None,t1)] + bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)] else match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 @@ -944,7 +1151,21 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = (* TODO: handle the case of multiple occs in different scopes *) (var,v)::terms,x,termlists,y -let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 = +let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = + let rec aux sigma acc rest = + try + let metas = add_ldots_var (add_meta_term y metas) in + let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in + let rest = Id.List.assoc ldots_var terms in + let t = Id.List.assoc y terms in + let sigma = remove_sigma y (remove_sigma ldots_var sigma) in + aux sigma (t::acc) rest + with No_match when not (List.is_empty acc) -> + acc, match_fun metas sigma rest termin in + let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in + (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) + +let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = match (a1,a2) with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) @@ -960,9 +1181,9 @@ let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 = else let l1',more_args = Util.List.chop le2 l1 in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) - | r1, NList (x,_,iter,termin,lassoc) -> - (match_alist (match_cases_pattern_no_more_args) - metas (terms,(),termlists,()) r1 x iter termin lassoc),(0,[]) + | r1, NList (x,y,iter,termin,lassoc) -> + (match_cases_pattern_list (match_cases_pattern_no_more_args) + metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 0f1b1a8756..854e222e30 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -23,7 +23,7 @@ val subst_interpretation : val ldots_var : Id.t -(** {5 Translation back and forth between [glob_constr] and [notation_constr] *) +(** {5 Translation back and forth between [glob_constr] and [notation_constr]} *) (** Translate a [glob_constr] into a notation given the list of variables bound by the notation; also interpret recursive patterns *) @@ -40,7 +40,7 @@ val glob_constr_of_notation_constr_with_binders : Loc.t -> val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr -(** {5 Matching a notation pattern against a [glob_constr] *) +(** {5 Matching a notation pattern against a [glob_constr]} *) (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) @@ -64,5 +64,5 @@ val match_notation_constr_ind_pattern : ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (int * cases_pattern list) -(** {5 Matching a notation pattern against a [glob_constr] *) +(** {5 Matching a notation pattern against a [glob_constr]} *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7b2d927162..3c4c2796ee 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -990,6 +990,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var id -> begin let open Context.Named.Declaration in @@ -1009,8 +1013,6 @@ let check_one_fix renv recpos trees def = | (Evar _ | Meta _) -> () | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - - | Proj (p, c) -> check_rec_call renv [] c and check_nested_fix_body renv decr recArgsDecrArg body = if Int.equal decr 0 then diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 23c0c1c31b..09f7bd75cd 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -851,6 +851,9 @@ let export ?except senv dir = let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; + if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then + CErrors.errorlabstrm "Safe_typing.import" + (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.push_context_set ~strict:true diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c729a6ce29..894f5296a8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -116,14 +116,14 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env ?from:(from=0) k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in diff --git a/lib/cList.ml b/lib/cList.ml index 602bba6a5c..c8283e3c71 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -601,19 +601,35 @@ let filter2 f l1 l2 = filter2_loop f c1 c2 l1 l2; (c1.tail, c2.tail) -let rec map_filter f = function - | [] -> [] - | x::l -> - let l' = map_filter f l in - match f x with None -> l' | Some y -> y::l' +let rec map_filter_loop f p = function + | [] -> () + | x :: l -> + match f x with + | None -> map_filter_loop f p l + | Some y -> + let c = { head = y; tail = [] } in + p.tail <- cast c; + map_filter_loop f c l + +let map_filter f l = + let c = { head = Obj.magic 0; tail = [] } in + map_filter_loop f c l; + c.tail -let map_filter_i f = - let rec aux i = function - | [] -> [] - | x::l -> - let l' = aux (succ i) l in - match f i x with None -> l' | Some y -> y::l' - in aux 0 +let rec map_filter_i_loop f i p = function + | [] -> () + | x :: l -> + match f i x with + | None -> map_filter_i_loop f (succ i) p l + | Some y -> + let c = { head = y; tail = [] } in + p.tail <- cast c; + map_filter_i_loop f (succ i) c l + +let map_filter_i f l = + let c = { head = Obj.magic 0; tail = [] } in + map_filter_i_loop f 0 c l; + c.tail let rec filter_with filter l = match filter, l with | [], [] -> [] diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 7b8dc2b9b5..78fa84f333 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -48,7 +48,7 @@ let create ~name ~category ?(default=Enabled) pp = CErrors.user_err_loc (loc,"_",pp x) | Enabled -> let msg = - pp x ++ str " [" ++ str name ++ str "," ++ + pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ str category ++ str "]" in let loc = Option.default !current_loc loc in @@ -204,7 +204,7 @@ let pr_loc_pos loc = int (fst loc) ++ str"-" ++ int (snd loc) let pr_loc loc = - if Loc.is_ghost loc then str"<unknown>" + if Loc.is_ghost loc then str"<unknown>" ++ fnl () else let fname = loc.Loc.fname in if CString.equal fname "" then diff --git a/library/declare.mli b/library/declare.mli index 8dd24d2780..7824506da0 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -34,14 +34,6 @@ val declare_variable : variable -> variable_declaration -> object_name type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent - - *) type internal_flag = | UserAutomaticRequest | InternalTacticRequest @@ -53,6 +45,12 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry +(** [declare_constant id cd] declares a global declaration + (constant/parameter) with name [id] in the current section; it returns + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent *) val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 0556191be8..47c78ae5c2 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -438,14 +438,22 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) +let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = + pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') + +let problem_inclusion x y = + List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x + let evd_convertible env evd x y = try - let evd = Evarconv.the_conv_x env x y evd in (* Unfortunately, the_conv_x might say they are unifiable even if some - unsolvable constraints remain, so we check them here *) - let evd = Evarconv.consider_remaining_unif_problems env evd in - let () = Evarconv.check_problems_are_solved env evd in - Some evd + unsolvable constraints remain, so we check that this unification + does not introduce any new problem. *) + let _, pbs = Evd.extract_all_conv_pbs evd in + let evd' = Evarconv.the_conv_x env x y evd in + let _, pbs' = Evd.extract_all_conv_pbs evd' in + if evd' == evd || problem_inclusion pbs' pbs then Some evd' + else None with e when CErrors.noncritical e -> None let convertible env evd x y = @@ -581,9 +589,9 @@ let general_rewrite_unif_flags () = let core_flags = { rewrite_core_unif_flags with Unification.modulo_conv_on_closed_terms = Some ts; - Unification.use_evars_eagerly_in_conv_on_closed_terms = false; + Unification.use_evars_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; - Unification.modulo_delta_types = ts; + Unification.modulo_delta_types = full_transparent_state; Unification.modulo_betaiota = true } in { Unification.core_unify_flags = core_flags; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8ecc7d015a..199ef9fcee 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -490,9 +490,6 @@ GEXTEND Gram [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac | -> None ] ] ; - rename : - [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] - ; rewriter : [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c) @@ -518,12 +515,6 @@ GEXTEND Gram | _,_,Some _ -> err () | _,_,None -> (ic,el) ]] ; - move_location: - [ [ IDENT "after"; id = id_or_meta -> MoveAfter id - | IDENT "before"; id = id_or_meta -> MoveBefore id - | "at"; IDENT "top" -> MoveFirst - | "at"; IDENT "bottom" -> MoveLast ] ] - ; simple_tactic: [ [ (* Basic tactics *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a4bceeb67c..c09693b364 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -211,11 +211,11 @@ GEXTEND Gram | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical)) - | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional)) - | kwd = IDENT "Axioms" -> (kwd, (None, Logical)) - | kwd = IDENT "Parameters" -> (kwd, (None, Definitional)) - | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ] + [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical)) + | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional)) + | IDENT "Axioms" -> ("Axioms", (None, Logical)) + | IDENT "Parameters" -> ("Parameters", (None, Definitional)) + | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index aff60eaa4e..fd46d80695 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -82,8 +82,10 @@ let rec decompose_term env sigma t= | Proj (p, c) -> let canon_const kn = constant_of_kn (canonical_con kn) in let p' = Projection.map canon_const p in - (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) - | _ ->if closed0 t then (Symb t) else raise Not_found + (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) + | _ -> + let t = strip_outer_cast t in + if closed0 t then Symb t else raise Not_found (* decompose equality in members and type *) open Globnames @@ -233,10 +235,10 @@ let build_projection intype (cstr:pconstructor) special default gls= let _M =mkMeta -let app_global f args k = +let app_global f args k = Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) -let new_app_global f args k = +let new_app_global f args k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) let new_refine c = Proofview.V82.tactic (refine c) @@ -246,7 +248,19 @@ let assert_before n c = let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) end } - + +let refresh_type env evm ty = + Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true + (Some false) env evm ty + +let refresh_universes ty k = + Proofview.Goal.enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let evm = Tacmach.New.project gl in + let evm, ty = refresh_type env evm ty in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty) + end } + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in @@ -256,35 +270,31 @@ let rec proof_tac p : unit Proofview.tactic = | SymAx c -> let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - let typ = (* Termops.refresh_universes *) type_of l in - new_app_global _sym_eq [|typ;r;l;c|] exact_check + refresh_universes (type_of l) (fun typ -> + new_app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in - let typ = (* Termops.refresh_universes *) type_of lr in - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check + refresh_universes (type_of lr) (fun typ -> + new_app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - let typ = (* Termops.refresh_universes *) (type_of t2) in + refresh_universes (type_of t2) (fun typ -> let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in - Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)] + Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - let typf = (* Termops.refresh_universes *)(type_of tf1) in - let typx = (* Termops.refresh_universes *) (type_of tx1) in - let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in + refresh_universes (type_of tf1) (fun typf -> + refresh_universes (type_of tx1) (fun typx -> + refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = - app_global _f_equal - [|typf;typfx;appx1;tf1;tf2;_M 1|] in - let lemma2= - app_global _f_equal - [|typx;typfx;tf2;tx1;tx2;_M 1|] in + let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in + let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in let prf = app_global _trans_eq [|typfx; @@ -298,34 +308,33 @@ let rec proof_tac p : unit Proofview.tactic = reflexivity; Tacticals.New.tclZEROMSG (Pp.str - "I don't know how to handle dependent equality")]] + "I don't know how to handle dependent equality")]]))) | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype = (* Termops.refresh_universes *) (type_of ti) in - let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in + refresh_universes (type_of ti) (fun intype -> + refresh_universes (type_of default) (fun outtype -> let proj = Tacmach.New.of_old (build_projection intype cstr special default) gl in let injt= app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in - Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } let refute_tac c t1 t2 p = Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl - in - let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in + let k intype = + let neweq= new_app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] + in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k end } let refine_exact_check c gl = @@ -335,16 +344,15 @@ let refine_exact_check c gl = let convert_to_goal_tac c t1 t2 p = Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl - in - let neweq= new_app_global _eq [|sort;tt1;tt2|] in - let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in - let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + let k sort = + let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in + let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let identity=mkLambda (Name x,sort,mkRel 1) in + let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end } let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -360,33 +368,28 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.nf_enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl - in + let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) - (* let outsort = mkSort outsort in *) let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) - (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in + let evm = Tacmach.New.project gl in + let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in - let pred=mkLambda(Name xid,outtype,mkRel 1) in + let pred = mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in let injt=app_global _f_equal - [|intype;outtype;proj;t1;t2;mkVar hid|] in + [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = injt (fun injt -> - app_global _eq_rect - [|outtype;trivial;pred;identity;concl;injt|] k) in + app_global _eq_rect + [|outtype;trivial;pred;identity;concl;injt|] k) in let neweq=new_app_global _eq [|intype;t1;t2|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) - (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) end } (* wrap everything *) @@ -470,7 +473,7 @@ let congruence_tac depth l = This isn't particularly related with congruence, apart from the fact that congruence is called internally. *) - + let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> Proofview.Goal.enter { enter = begin fun gl -> @@ -482,7 +485,7 @@ let mk_eq f c1 c2 k = Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) end }) - + let f_equal = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 864d90a0f2..60fe8e7620 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -310,7 +310,7 @@ let base_r = function let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = let needed = ref Refset'.empty and needed_mps = ref MPset.empty in - ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), + ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v index a19e9df904..7e3ef89293 100644 --- a/plugins/micromega/Env.v +++ b/plugins/micromega/Env.v @@ -93,7 +93,7 @@ End S. Ltac jump_simpl := repeat match goal with - | |- appcontext [jump xH] => rewrite (jump_simpl xH) - | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p)) - | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p)) + | |- context [jump xH] => rewrite (jump_simpl xH) + | |- context [jump (xO ?p)] => rewrite (jump_simpl (xO p)) + | |- context [jump (xI ?p)] => rewrite (jump_simpl (xI p)) end. diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli deleted file mode 100644 index 57c4e50cad..0000000000 --- a/plugins/micromega/sos_types.mli +++ /dev/null @@ -1,40 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* The type of positivstellensatz -- used to communicate with sos *) - -type vname = string;; - -type term = -| Zero -| Const of Num.num -| Var of vname -| Inv of term -| Opp of term -| Add of (term * term) -| Sub of (term * term) -| Mul of (term * term) -| Div of (term * term) -| Pow of (term * int);; - -val output_term : out_channel -> term -> unit - -type positivstellensatz = - Axiom_eq of int - | Axiom_le of int - | Axiom_lt of int - | Rational_eq of Num.num - | Rational_le of Num.num - | Rational_lt of Num.num - | Square of term - | Monoid of int list - | Eqmul of term * positivstellensatz - | Sum of positivstellensatz * positivstellensatz - | Product of positivstellensatz * positivstellensatz;; - -val output_psatz : out_channel -> positivstellensatz -> unit diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 3068b53470..b11d15e5ca 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont := match goal with | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => intros _; + let lci := fresh "lci" in set (lci:=lci0); + let lq := fresh "lq" in set (lq:=lq0); kont c rr lq lci end. @@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar := end in SplitPolyList ltac:(fun p lp => + let p21 := fresh "p21" in + let lp21 := fresh "lp21" in set (p21:=p) ; set (lp21:=lp); (* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + let q := fresh "q" in set (q := PEmul c (PEpow p21 r)); let Hg := fresh "Hg" in assert (Hg:check lp21 q (lci,lq) = true); diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 93dad18d98..36bce780bd 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -468,6 +468,44 @@ let theoremedeszeros lpol p = open Ideal +(* Remove zero polynomials and duplicates from the list of polynomials lp + Return (clp, lb) + where clp is the reduced list and lb is a list of booleans + that has the same size than lp and where true indicates an + element that has been removed + *) +let rec clean_pol lp = + let t = Hashpol.create 12 in + let find p = try Hashpol.find t p + with + Not_found -> Hashpol.add t p true; false in + let rec aux lp = + match lp with + | [] -> [], [] + | p :: lp1 -> + let clp, lb = aux lp1 in + if equal p zeroP || find p then clp, true::lb + else + (p :: clp, false::lb) in + aux lp + +(* Expand the list of polynomials lp putting zeros where the list of + booleans lb indicates there is a missing element + Warning: + the expansion is relative to the end of the list in reversed order + lp cannot have less elements than lb +*) +let expand_pol lb lp = + let rec aux lb lp = + match lb with + | [] -> lp + | true :: lb1 -> zeroP :: aux lb1 lp + | false :: lb1 -> + match lp with + [] -> assert false + | p :: lp1 -> p :: aux lb1 lp1 + in List.rev (aux lb (List.rev lp)) + let theoremedeszeros_termes lp = nvars:=0;(* mise a jour par term_pol_sparse *) List.iter set_nvars_term lp; @@ -518,20 +556,29 @@ let theoremedeszeros_termes lp = | [] -> assert false | p::lp1 -> let lpol = List.rev lp1 in + (* preprocessing : + we remove zero polynomials and duplicate that are not handled by in_ideal + lb is kept in order to fix the certificate in the post-processing + *) + let lpol, lb = clean_pol lpol in let (cert,lp0,p,_lct) = theoremedeszeros lpol p in info "cert ok\n"; let lc = cert.last_comb::List.rev cert.gb_comb in match remove_zeros (fun x -> equal x zeroP) lc with | [] -> assert false | (lq::lci) -> + (* post-processing : we apply the correction for the last line *) + let lq = expand_pol lb lq in (* lci commence par les nouveaux polynomes *) - let m= !nvars in + let m = !nvars in let c = pol_sparse_to_term m (polconst m cert.coef) in let r = Pow(Zero,cert.power) in let lci = List.rev lci in + (* post-processing we apply the correction for the other lines *) + let lci = List.map (expand_pol lb) lci in let lci = List.map (List.map (pol_sparse_to_term m)) lci in let lq = List.map (pol_sparse_to_term m) lq in - info ("number of parametres: "^string_of_int nparam^"\n"); + info ("number of parameters: "^string_of_int nparam^"\n"); info "term computed\n"; (c,r,lci,lq) ) diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 5e43dfc42d..187601fc62 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1451,27 +1451,27 @@ Ltac loop t := | (Tint ?X1) => loop X1 (* Eliminations *) | match ?X1 with - | EqTerm x x0 => _ - | LeqTerm x x0 => _ + | EqTerm _ _ => _ + | LeqTerm _ _ => _ | TrueTerm => _ | FalseTerm => _ - | Tnot x => _ - | GeqTerm x x0 => _ - | GtTerm x x0 => _ - | LtTerm x x0 => _ - | NeqTerm x x0 => _ - | Tor x x0 => _ - | Tand x x0 => _ - | Timp x x0 => _ - | Tprop x => _ + | Tnot _ => _ + | GeqTerm _ _ => _ + | GtTerm _ _ => _ + | LtTerm _ _ => _ + | NeqTerm _ _ => _ + | Tor _ _ => _ + | Tand _ _ => _ + | Timp _ _ => _ + | Tprop _ => _ end => destruct X1; auto; Simplify | match ?X1 with - | Tint x => _ - | (x + x0)%term => _ - | (x * x0)%term => _ - | (x - x0)%term => _ - | (- x)%term => _ - | [x]%term => _ + | Tint _ => _ + | (_ + _)%term => _ + | (_ * _)%term => _ + | (_ - _)%term => _ + | (- _)%term => _ + | [_]%term => _ end => destruct X1; auto; Simplify | (if beq ?X1 ?X2 then _ else _) => let H := fresh "H" in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 985ad4b0d3..447a4c487c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1329,14 +1329,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn *) -let mk_case pb (ci,pred,c,brs) = - let mib = lookup_mind (fst ci.ci_ind) pb.env in - match mib.mind_record with - | Some (Some (_, cs, pbs)) -> - Reduction.beta_appvect brs.(0) - (Array.map (fun p -> mkProj (Projection.make p true, c)) cs) - | _ -> mkCase (ci,pred,c,brs) - (**********************************************************************) (* Main compiling descent *) let rec compile pb = @@ -1383,7 +1375,9 @@ and match_current pb (initial,tomatch) = pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota !(pb.evdref) pred in - let case = mk_case pb (ci,pred,current,brvals) in + let case = + make_case_or_project pb.env indf ci pred current brvals + in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist typ inst } diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 338ac43009..6c8677855a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,8 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) + pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh status dir t = @@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' + | Sort (Prop Pos as s) when refreshset && not dir -> + let s' = evd_comb0 (new_sort_variable status) evdref in + let evd = set_leq_sort env !evdref s s' in + modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> mkProd (na,u,refresh status dir v) | _ -> t diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 918ba12f0f..f94c83b6dc 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,8 +34,12 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : ?status:Evd.rigid -> - ?onlyalg:bool (* Only algebraic universes *) -> +val refresh_universes : + ?status:Evd.rigid -> + ?onlyalg:bool (* Only algebraic universes *) -> + ?refreshset:bool -> + (* Also refresh Prop and Set universes, so that the returned type can be any supertype + of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 5c8060996a..51660818f4 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -470,6 +470,78 @@ let loc_of_glob_constr = function | GCast (loc,_,_) -> loc (**********************************************************************) +(* Alpha-renaming *) + +let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l +let test_id l id = if collide_id l id then raise Not_found +let test_na l na = name_iter (test_id l) na + +let update_subst na l = + let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in + let l' = name_fold Id.List.remove_assoc na l in + name_fold + (fun id _ -> + if in_range id l' then + let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in + Name id', (id,id')::l + else na,l) + na (na,l) + +exception UnsoundRenaming + +let rename_var l id = + try + let id' = Id.List.assoc id l in + (* Check that no other earlier binding hide the one found *) + let _,(id'',_) = List.extract_first (fun (_,id) -> Id.equal id id') l in + if Id.equal id id'' then id' else raise UnsoundRenaming + with Not_found -> + if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming + else id + +let rec rename_glob_vars l = function + | GVar (loc,id) as r -> + let id' = rename_var l id in + if id == id' then r else GVar (loc,id') + | GRef (_,VarRef id,_) as r -> + if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming + else r + | GProd (loc,na,bk,t,c) -> + let na',l' = update_subst na l in + GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLambda (loc,na,bk,t,c) -> + let na',l' = update_subst na l in + GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLetIn (loc,na,b,c) -> + let na',l' = update_subst na l in + GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) + | GCases (loc,ci,po,tomatchl,cls) -> + let test_pred_pat (na,ino) = + test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in + let test_clause idl = List.iter (test_id l) idl in + let po = Option.map (rename_glob_vars l) po in + let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in + let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in + GCases (loc,ci,po,tomatchl,cls) + | GLetTuple (loc,nal,(na,po),c,b) -> + List.iter (test_na l) (na::nal); + GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po), + rename_glob_vars l c,rename_glob_vars l b) + | GIf (loc,c,(na,po),b1,b2) -> + test_na l na; + GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), + rename_glob_vars l b1,rename_glob_vars l b2) + | GRec (loc,k,idl,decls,bs,ts) -> + Array.iter (test_id l) idl; + GRec (loc,k,idl, + Array.map (List.map (fun (na,k,bbd,bty) -> + test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, + Array.map (rename_glob_vars l) bs, + Array.map (rename_glob_vars l) ts) + | r -> map_glob_constr (rename_glob_vars l) r + +(**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) let rec cases_pattern_of_glob_constr na = function diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index c2b27ca6ab..55e6b6533f 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -44,6 +44,16 @@ val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t val glob_visible_short_qualid : glob_constr -> Id.t list +(* Renaming free variables using a renaming map; fails with + [UnsoundRenaming] if applying the renaming would introduce + collision, as in, e.g., renaming [P x y] using substitution [(x,y)]; + inner alpha-conversion done only for forall, fun, let but + not for cases and fix *) + +exception UnsoundRenaming +val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t +val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr + (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. It is used to diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0c80bd0193..39aeb41f77 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -36,12 +36,14 @@ type dep_flag = bool type recursion_scheme_error = | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive + | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error let make_prod_dep dep env = if dep then mkProd_name env else mkProd let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) + (*******************************************) (* Building curryfied elimination *) (*******************************************) @@ -375,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u = (Anonymous,depind',concl)) arsign' in - let obj = - let projs = get_projections env indf in - match projs with - | None -> (mkCase (ci, pred, - mkRel 1, - branches)) - | Some ps -> - let branch = branches.(0) in - let ctx, br = decompose_lam_assum branch in - let n, subst = - List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na,t) -> - let t = mkProj (Projection.make ps.(i) true, mkRel 1) in - i + 1, t :: subst - | LocalDef (na,b,t) -> - i, mkRel 0 :: subst) - ctx (0, []) - in - let term = substl subst br in - term + let obj = + Inductiveops.make_case_or_project env indf ci pred + (mkRel 1) branches in it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) @@ -483,6 +467,8 @@ let mis_make_indrec env sigma listdepkind mib u = let build_case_analysis_scheme env sigma pity dep kind = let (mib,mip) = lookup_mind_specif env (fst pity) in + if dep && not (Inductiveops.has_dependent_elim mib) then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity))); mis_make_case_com dep env sigma pity (mib,mip) kind let is_in_prop mip = @@ -492,7 +478,7 @@ let is_in_prop mip = let build_case_analysis_scheme_default env sigma pity kind = let (mib,mip) = lookup_mind_specif env (fst pity) in - let dep = not (is_in_prop mip) in + let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in mis_make_case_com dep env sigma pity (mib,mip) kind (**********************************************************************) @@ -553,6 +539,8 @@ let check_arities env listdepkind = let build_mutual_induction_scheme env sigma = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in + if dep && not (Inductiveops.has_dependent_elim mib) then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind))); let (sp,tyi) = mind in let listdepkind = ((mind,u),mib,mip,dep,s):: @@ -572,6 +560,8 @@ let build_mutual_induction_scheme env sigma = function let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in + if dep && not (Inductiveops.has_dependent_elim mib) then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind))); let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in sigma, List.hd l diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index f0736d2dda..192b64a5ed 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -16,6 +16,7 @@ open Evd type recursion_scheme_error = | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive + | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error @@ -28,13 +29,15 @@ type dep_flag = bool val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive -> dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma -(** Build a dependent case elimination predicate unless type is in Prop *) +(** Build a dependent case elimination predicate unless type is in Prop + or is a recursive record with primitive projections. *) val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive -> sorts_family -> (constr, 'r) Sigma.sigma (** Builds a recursive induction scheme (Peano-induction style) in the same - sort family as the inductive family; it is dependent if not in Prop *) + sort family as the inductive family; it is dependent if not in Prop + or a recursive record with primitive projections. *) val build_induction_scheme : env -> evar_map -> pinductive -> dep_flag -> sorts_family -> evar_map * constr diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index fbad0d949d..214e19fecf 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -269,6 +269,11 @@ let projection_nparams_env env p = let projection_nparams p = projection_nparams_env (Global.env ()) p +let has_dependent_elim mib = + match mib.mind_record with + | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | _ -> true + (* Annotation for cases *) let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -338,6 +343,35 @@ let get_projections env (ind,params) = | Some (Some (id, projs, pbs)) -> Some projs | _ -> None +let make_case_or_project env indf ci pred c branches = + let projs = get_projections env indf in + match projs with + | None -> (mkCase (ci, pred, c, branches)) + | Some ps -> + assert(Array.length branches == 1); + let () = + let _, _, t = destLambda pred in + let (ind, _), _ = dest_ind_family indf in + let mib, _ = Inductive.lookup_mind_specif env ind in + if (* dependent *) not (noccurn 1 t) && + not (has_dependent_elim mib) then + errorlabstrm "make_case_or_project" + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) + in + let branch = branches.(0) in + let ctx, br = decompose_lam_n_assum (Array.length ps) branch in + let n, subst = + List.fold_right + (fun decl (i, subst) -> + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, substl subst b :: subst)) + ctx (0, []) + in substl subst br + (* substitution in a signature *) let substnl_rel_context subst n sign = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index d25f8a8378..7bd616591f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -122,11 +122,16 @@ val inductive_has_local_defs : inductive -> bool val allowed_sorts : env -> inductive -> sorts_family list +(** (Co)Inductive records with primitive projections do not have eta-conversion, + hence no dependent elimination. *) +val has_dependent_elim : mutual_inductive_body -> bool + (** Primitive projections *) val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + constr -> types -> types + (** Extract information from an inductive family *) @@ -175,6 +180,14 @@ val type_case_branches_with_names : (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info +(** Make a case or substitute projections if the inductive type is a record + with primitive projections. + Fail with an error if the elimination is dependent while the + inductive type does not allow dependent elimination. *) +val make_case_or_project : + env -> inductive_family -> case_info -> + (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c8f61c66b8..1ef96e0344 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -68,6 +68,61 @@ open Inductiveops (************************************************************************) +module ExtraEnv = +struct + +type t = { + env : Environ.env; + extra : Evarutil.ext_named_context Lazy.t; + (** Delay the computation of the evar extended environment *) +} + +let get_extra env = + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + Context.Rel.fold_outside push_rel_decl_to_named_context + (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + +let make_env env = { env = env; extra = lazy (get_extra env) } +let rel_context env = rel_context env.env + +let push_rel d env = { + env = push_rel d env.env; + extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); +} + +let pop_rel_context n env = make_env (pop_rel_context n env.env) + +let push_rel_context ctx env = { + env = push_rel_context ctx env.env; + extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); +} + +let lookup_named id env = lookup_named id env.env + +let e_new_evar env evdref ?src ?naming typ = + let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in + let open Context.Named.Declaration in + let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in + let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in + let (subst, vsubst, _, nc) = Lazy.force env.extra in + let typ' = subst2 subst vsubst typ in + let instance = inst_rels @ inst_vars in + let sign = val_of_named_context nc in + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in + evdref := Sigma.to_evar_map sigma; + e + +let push_rec_types (lna,typarray,_) env = + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + Array.fold_left (fun e assum -> push_rel assum e) env ctxt + +end + +open ExtraEnv + (* An auxiliary function for searching for fixpoint guard indexes *) exception Found of int array @@ -302,9 +357,9 @@ let evar_type_fixpoint loc env evdref lna lar vdefj = let lt = Array.length vdefj in if Int.equal (Array.length lar) lt then for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type + if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref + error_ill_typed_rec_body_loc loc env.ExtraEnv.env !evdref i lna vdefj lar done @@ -312,7 +367,7 @@ let evar_type_fixpoint loc env evdref lna lar vdefj = let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -361,7 +416,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env sigma c + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ @@ -444,7 +499,7 @@ let pretype_global loc rigid env evd gr us = str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in - Evd.fresh_global ~loc ~rigid ?names:instance env evd gr + Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr let pretype_ref loc evdref env ref us = match ref with @@ -459,7 +514,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env evd c in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty let judge_of_Type loc evd s = @@ -477,7 +532,7 @@ let pretype_sort loc evdref = function let new_type_evar env evdref loc = let sigma = Sigma.Unsafe.of_evar_map !evdref in let Sigma ((e, _), sigma, _) = - Evarutil.new_type_evar env sigma + Evarutil.new_type_evar env.ExtraEnv.env sigma univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in evdref := Sigma.to_evar_map sigma; @@ -489,7 +544,7 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in @@ -515,7 +570,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env !evdref c) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> @@ -544,7 +599,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in - let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in + let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } @@ -578,7 +633,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env evdref ftys.(fixi) t + in e_conv env.ExtraEnv.env evdref ftys.(fixi) t | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -617,12 +672,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env possible_indexes fixdecls + loc env.ExtraEnv.env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env.ExtraEnv.env cofix with reraise -> let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in @@ -652,7 +707,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env !evdref ty in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars else (* Let the usual code throw an error *) [] @@ -661,9 +716,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ in let app_f = match kind_of_term fj.uj_val with - | Const (p, u) when Environ.is_projection p env -> + | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in - let pb = Environ.lookup_projection p env in + let pb = Environ.lookup_projection p env.ExtraEnv.env in let npars = pb.Declarations.proj_npars in fun n -> if n == npars + 1 then fun _ v -> mkProj (p, v) @@ -674,8 +729,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_all env !evdref resj.uj_type in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in + let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -684,7 +739,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env evdref (j_val hj) arg then + if e_conv env.ExtraEnv.env evdref (j_val hj) arg then args, nf_evar !evdref (j_val hj) else [], j_val hj in @@ -695,7 +750,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env !evdref + (Loc.merge floc argloc) env.ExtraEnv.env !evdref resj [hj] in let resj = apply_rec env 1 fj candargs args in @@ -703,13 +758,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env f then + if is_template_polymorphic env.ExtraEnv.env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in - let t = Retyping.get_type_of env !evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -722,11 +777,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So @@ -735,7 +790,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - let resj = judge_of_abstraction env (orelse_name name name') j j' in + let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon | GProd(loc,name,bk,c1,c2) -> @@ -749,13 +804,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ { j with utj_val = lift 1 j.utj_val } | Name _ -> let var = (name,j.utj_val) in - let env' = push_rel_assum var env in + let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = try - judge_of_product env name j j' + judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> let (e, info) = CErrors.push e in let info = Loc.add_loc info loc in @@ -771,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are @@ -786,12 +841,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in - let cstrs = get_constructors env indf in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ str " with one constructor."); @@ -800,7 +855,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = - match get_projections env indf with + match get_projections env.ExtraEnv.env indf with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> @@ -821,36 +876,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let nal = List.rev nal in let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info env (fst ind) LetStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in (* Make dependencies from arity signature impossible *) let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then List.map (set_name Anonymous) arsgn else arsgn in - let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let nar = List.length arsgn in (match po with | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env true indf in (* with names *) + let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env !evdref lp inst in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -863,37 +918,37 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env !evdref + error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj in - let cstrs = get_constructors env indf in + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then user_err_loc (loc,"", str "If is only for inductive types with two constructors."); let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then (* Make dependencies from arity signature impossible *) List.map (set_name Anonymous) arsgn else arsgn in let nar = List.length arsgn in - let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -931,9 +986,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info env (fst ind) IfStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in @@ -941,43 +996,46 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) - tycon env (* loc *) (po,tml,eqns) + ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) + tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> let cj = match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in - let tval = nf_evar !evdref tj.utj_val in - let cj = match k with + let tval = evd_comb1 (Evarsolve.refresh_universes + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) + evdref tj.utj_val in + let tval = nf_evar !evdref tval in + let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential cty || occur_existential tval) then - let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in + if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in + if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c + pretype (mk_tycon tval) env evdref lvar c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } @@ -995,11 +1053,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = lookup_named id env |> get_type in - if is_conv env !evdref t t' then mkVar id, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1010,17 +1068,17 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon env evdref lvar = function +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_all env sigma t) with + let t = Retyping.get_type_of env.ExtraEnv.env sigma v in + match kind_of_term (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort env) evdref ev + evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in { utj_val = v; @@ -1033,16 +1091,17 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function | c -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> - if e_cumul env evdref v tj.utj_val then tj + if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_glob_constr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = + let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let c' = match kind with @@ -1053,7 +1112,7 @@ let ise_pretype_gen flags env sigma lvar kind c = | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') let default_inference_flags fail = { use_typeclasses = true; @@ -1085,19 +1144,21 @@ let on_judgment f j = {uj_val = c; uj_type = t} let understand_judgment env sigma c = + let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in + let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = + let env = make_env env in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in + let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in evdref := evd; c) j let ise_pretype_gen_ctx flags env sigma lvar kind c = @@ -1146,3 +1207,9 @@ let type_uconstr ?(flags = constr_flags) let (sigma, c) = understand_ltac flags env sigma vars expected_type term in Sigma.Unsafe.of_pair (c, sigma) end } + +let pretype k0 resolve_tc typcon env evdref lvar t = + pretype k0 resolve_tc typcon (make_env env) evdref lvar t + +let pretype_type k0 resolve_tc valcon env evdref lvar t = + pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 682a883338..284af0cb15 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -195,7 +195,7 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections (con,ind) = +let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in let u = Univ.UContext.instance ctx in @@ -222,7 +222,7 @@ let compute_canonical_projections (con,ind) = with Not_found -> let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); l end | _ -> l) @@ -246,9 +246,8 @@ let warn_redundant_canonical_projection = ++ strbrk " by " ++ prj ++ strbrk " in " ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) -let open_canonical_structure i (_,o) = - if Int.equal i 1 then - let lo = compute_canonical_projections o in +let add_canonical_structure warn o = + let lo = compute_canonical_projections warn o in List.iter (fun ((proj,(cs_pat,_ as pat)),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in let ocs = try Some (assoc_pat cs_pat l) @@ -260,11 +259,14 @@ let open_canonical_structure i (_,o) = and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) + if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) lo -let cache_canonical_structure o = - open_canonical_structure 1 o +let open_canonical_structure i (_, o) = + if Int.equal i 1 then add_canonical_structure false o + +let cache_canonical_structure (_, o) = + add_canonical_structure true o let subst_canonical_structure (subst,(cst,ind as obj)) = (* invariant: cst is an evaluable reference. Thus we can take *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0e4885bead..696d419afe 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -110,18 +110,18 @@ let e_type_case_branches env evdref (ind,largs) pj c = let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let univ = e_is_correct_arity env evdref c pj ind specif params in + let () = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in - (lc, ty, univ) + (lc, ty) let e_judge_of_case env evdref ci pj cj lfj = let indspec = try find_mrectype env !evdref cj.uj_type with Not_found -> error_case_not_inductive env cj in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty,univ) = e_type_case_branches env evdref indspec pj cj.uj_val in + let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in e_check_branch_types env evdref (fst indspec) cj (lfj,bty); { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 252b0967dc..935e2d076e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -349,8 +349,13 @@ end) = struct | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) - | LocalPattern _ -> - assert false + | LocalPattern (loc,p,tyo) -> + let p = pr_patt lsimplepatt p in + match tyo with + | None -> + str "'" ++ p + | Some ty -> + str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty) let pr_undelimited_binders sep pr_c = prlist_with_sep sep (pr_binder_among_many pr_c) @@ -360,10 +365,8 @@ end) = struct match bl with | [LocalRawAssum (nal,k,t)] -> pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) - | LocalRawAssum _ :: _ as bdl -> + | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl - | LocalPattern (loc,p,tyo) :: _ -> - str "'" ++ pr_patt ltop p | _ -> assert false let pr_binders_gen pr_c sep is_open = @@ -376,6 +379,11 @@ end) = struct if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) | CProdN (loc,[],c) -> extract_prod_binders c + | CProdN (loc,[[_,Name id],bk,t], + CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) + when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> + let bl,c = extract_prod_binders b in + LocalPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in LocalRawAssum (nal,bk,t) :: bl, c @@ -387,6 +395,11 @@ end) = struct if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) | CLambdaN (loc,[],c) -> extract_lam_binders c + | CLambdaN (loc,[[_,Name id],bk,t], + CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) + when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> + let bl,c = extract_lam_binders b in + LocalPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in LocalRawAssum (nal,bk,t) :: bl, c @@ -538,21 +551,6 @@ end) = struct (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), lfix ) - | CProdN - (_, - [([(_,Name n)],_,_)], - CCases - (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)], - [(_,[(_,[p])],a)])) - when - Id.equal m n && - not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) -> - return ( - hov 0 ( - keyword "forall" ++ spc () ++ str "'" ++ pr_patt ltop p ++ - str "," ++ pr spc ltop a), - llambda - ) | CProdN _ -> let (bl,a) = extract_prod_binders a in return ( @@ -562,21 +560,6 @@ end) = struct str "," ++ pr spc ltop a), lprod ) - | CLambdaN - (_, - [([(_,Name n)],_,_)], - CCases - (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)], - [(_,[(_,[p])],a)])) - when - Id.equal m n && - not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) -> - return ( - hov 0 ( - keyword "fun" ++ spc () ++ str "'" ++ pr_patt ltop p ++ - pr_fun_sep ++ pr spc ltop a), - llambda - ) | CLambdaN _ -> let (bl,a) = extract_lam_binders a in return ( diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f6e99c7e7..f71719cb9a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -224,12 +224,12 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () - | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" + | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] + [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] - + let print_primitive ref = match ref with | IndRef ind -> diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 58b8811741..5f0cc73d2c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -56,6 +56,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc (loc,"", str "Instance is not well-typed in the environment of " ++ - str (string_of_existential evk)) + pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index de28189023..93073fdc7e 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,19 +52,21 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in - let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + let sigma = Evd.merge_universe_context sigma ectx in + let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in + let sigma = Evd.from_env env in let ctx = let mib,mip = Inductive.lookup_mind_specif env ind in Declareops.inductive_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let ectx = Evd.evar_universe_context_of ctxset in - let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in + let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = @@ -95,6 +97,10 @@ let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) + let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index c36797059e..77f927f2df 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -13,9 +13,11 @@ open Ind_tables val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind +val rect_scheme_kind_from_type : individual scheme_kind val rect_dep_scheme_kind_from_type : individual scheme_kind val ind_scheme_kind_from_type : individual scheme_kind val ind_dep_scheme_kind_from_type : individual scheme_kind +val rec_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind diff --git a/tactics/equality.ml b/tactics/equality.ml index f18de92c03..4aa7ffa7bd 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -860,7 +860,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - mkCase (ci, p, head, Array.of_list brl))) + Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e489013143..38af9a0caa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2665,10 +2665,15 @@ let letin_tac with_eq id c ty occs = let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let abs = AbstractExact (id,c,ty,occs,true) in - let (id,_,depdecls,lastlhyp,ccl,_) = make_abstraction env sigma ccl abs in - (* We keep the original term to match *) + let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in + (* We keep the original term to match but record the potential side-effects + of unifying universes. *) + let Sigma (c, sigma, p) = match res with + | None -> Sigma.here c sigma + | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p) + in let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in - Sigma.here tac sigma + Sigma (tac, sigma, p) end } let letin_pat_tac with_eq id c occs = diff --git a/test-suite/bugs/closed/2839.v b/test-suite/bugs/closed/2839.v index e396fe06e5..e727e26061 100644 --- a/test-suite/bugs/closed/2839.v +++ b/test-suite/bugs/closed/2839.v @@ -5,6 +5,6 @@ intro. Fail let H := match goal with - | [ H : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' + | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' end in pose H. diff --git a/test-suite/bugs/closed/3383.v b/test-suite/bugs/closed/3383.v new file mode 100644 index 0000000000..25257644a6 --- /dev/null +++ b/test-suite/bugs/closed/3383.v @@ -0,0 +1,6 @@ +Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. +intro. +lazymatch goal with +| [ |- context[match ?b as b' in bool return @?P b' with true => ?t | false => ?f end] ] + => change (match b as b' in bool return P b' with true => t | false => f end) with (@bool_rect P t f b) +end. diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v index 679721667a..961563ed4a 100644 --- a/test-suite/bugs/closed/3563.v +++ b/test-suite/bugs/closed/3563.v @@ -16,11 +16,11 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0) transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] => set(foo:=h); idtac end. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ] + | [ |- context ctx [transport (fun y => (?g (fst (y H2))))] ] => idtac end. Abort. @@ -30,7 +30,7 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0) transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] => set(foo:=X) end. (* Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index c24173abf1..fd9640b890 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -47,7 +47,7 @@ Type@{Top.21} -> Type@{Top.23} Top.23 < Top.22 *) *) Fail Check @qux@{Set Set}. -Fail Check @qux@{Set Set Set}. +Check @qux@{Type Type Type Type}. (* [qux] should only need two universes *) -Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *) +Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *) Fail Check @qux@{i j}. diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v new file mode 100644 index 0000000000..2ac4abe54f --- /dev/null +++ b/test-suite/bugs/closed/3886.v @@ -0,0 +1,23 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). + +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) + := _ +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) + := _. +Obligations. +Axiom cheat : forall {A}, A. +Obligation 1 of doubleE. +apply cheat. +Qed. + +Obligation 1 of doubleO. +apply cheat. +Qed. + +Check doubleE.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 21b03ce541..61527764e2 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -49,3 +49,56 @@ Lemma bar {A} n m (x : A) : skipn n (replicate m x) = replicate (m - n) x. Proof. intros. f_equal. (* 8.5: one goal, n = m - n *) +Abort. + +Variable F : nat -> Set. +Variable X : forall n, F (n + 1). + +Definition sequator{X Y: Set}{eq:X=Y}(x:X) : Y := eq_rec _ _ x _ eq. +Definition tequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq. +Polymorphic Definition pequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq. + +Goal {n:nat & F (S n)}. +eexists. +unshelve eapply (sequator (X _)). +f_equal. (*behaves*) +Undo 2. +unshelve eapply (pequator (X _)). +f_equal. (*behaves*) +Undo 2. +unshelve eapply (tequator (X _)). +f_equal. (*behaves now *) +Focus 2. exact 0. +simpl. +reflexivity. +Defined. + +(* Part 2: modulo casts introduced by refine due to reductions in goals *) + +Goal {n:nat & F (S n)}. +eexists. +(*misbehaves, although same goal as above*) +Set Printing All. +unshelve refine (sequator (X _)); revgoals. +2:exact 0. reflexivity. +Undo 3. +unshelve refine (pequator (X _)); revgoals. +f_equal. +Undo 2. +unshelve refine (tequator (X _)); revgoals. +f_equal. +Admitted. + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index f85a60264d..eb37141bcf 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -11,7 +11,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), simpl. intros. match goal with - | [ |- appcontext G[@hd] ] => idtac + | [ |- context G[@hd] ] => idtac end. (* This second example comes from CFGV where inspecting subterms of a diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v new file mode 100644 index 0000000000..ffa478cb87 --- /dev/null +++ b/test-suite/bugs/closed/4622.v @@ -0,0 +1,24 @@ +Set Primitive Projections. + +Record foo : Type := bar { x : unit }. + +Goal forall t u, bar t = bar u -> t = u. +Proof. + intros. + injection H. + trivial. +Qed. +(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *) + +(** Dependent pattern-matching is ok on this one as it has eta *) +Definition baz (x : foo) := + match x as x' return x' = x' with + | bar u => eq_refl + end. + +Inductive foo' : Type := bar' {x' : unit; y: foo'}. +(** Dependent pattern-matching is not ok on this one *) +Fail Definition baz' (x : foo') := + match x as x' return x' = x' with + | bar' u y => eq_refl + end. diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v new file mode 100644 index 0000000000..1ae5081851 --- /dev/null +++ b/test-suite/bugs/closed/4673.v @@ -0,0 +1,57 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 + coqtop version 8.5 (February 2016) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Lists.List. +Import Coq.Lists.List. +Import Coq.Classes.Morphisms. + +Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) + ls + : P ls + := match ls with + | nil => N + | x::xs => C x xs + end. + +Global Instance list_caset_Proper' {A P} + : Proper (eq + ==> pointwise_relation _ (pointwise_relation _ eq) + ==> eq + ==> eq) + (@list_caset A (fun _ => P)). +admit. +Defined. + +Global Instance list_caset_Proper'' {A P} + : (Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> forall_relation (fun _ => eq)) + (list_caset A (fun _ => P))). +Admitted. + +Goal forall (Char : Type) (P : forall _ : list bool, Prop) (l : list bool) (l0 : forall _ : forall _ : Char, bool, list bool) + + (T : Type) (T0 : forall _ : T, Type) (t : T), + + let predata := t in + + forall (splitdata : T0 predata) (l5 : forall _ : T0 t, list nat) (T1 : Type) (b : forall (_ : T1) (_ : Char), bool) + + (T2 : Type) (a11 : T2) (xs : list T2) (T3 : Type) (i0 : T3) (P0 : Set) (b1 : forall (_ : nat) (_ : P0), bool) + + (l2 : forall (_ : forall _ : T1, list bool) (_ : forall _ : P0, list bool) (_ : T2), list bool) + + (l1 : forall (_ : forall _ : forall _ : Char, bool, list bool) (_ : forall _ : P0, list bool) (_ : T3), list bool) + + (_ : forall NT : forall _ : P0, list bool, @eq (list bool) (l1 l0 NT i0) (l2 (fun f : T1 => l0 (b f)) NT a11)), + + P + (@list_caset T2 (fun _ : list T2 => list bool) l + (fun (_ : T2) (_ : list T2) => l1 l0 (fun a9 : P0 => @map nat bool (fun x0 : nat => b1 x0 a9) (l5 splitdata)) i0 +) xs). + intros. + subst predata; + let H := match goal with H : forall _, _ = _ |- _ => H end in + setoid_rewrite H || fail 0 "too early". + Undo. + setoid_rewrite H. diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v new file mode 100644 index 0000000000..c94fa31a9d --- /dev/null +++ b/test-suite/bugs/closed/4679.v @@ -0,0 +1,18 @@ +Require Import Coq.Setoids.Setoid. +Goal forall (T : nat -> Set -> Set) (U : Set) + (H : forall n : nat, T n (match n with + | 0 => fun x => x + | S _ => fun x => x + end (nat = nat)) = U), + T 0 (nat = nat) = U. +Proof. + intros. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + rewrite H || fail 0 "too early". + Undo. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + setoid_rewrite (H 0) || fail 0 "too early". + Undo. + setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *) + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v new file mode 100644 index 0000000000..9c0bed42c4 --- /dev/null +++ b/test-suite/bugs/closed/4684.v @@ -0,0 +1,32 @@ +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. + +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v new file mode 100644 index 0000000000..ac0653492a --- /dev/null +++ b/test-suite/bugs/closed/4733.v @@ -0,0 +1,52 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) + +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v new file mode 100644 index 0000000000..5bb3cd1be7 --- /dev/null +++ b/test-suite/bugs/closed/4754.v @@ -0,0 +1,35 @@ + +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. +Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + setoid_rewrite (FG _ _); [ | reflexivity.. ]. + Undo. + setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v new file mode 100644 index 0000000000..d87906f313 --- /dev/null +++ b/test-suite/bugs/closed/4769.v @@ -0,0 +1,94 @@ + +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) +(* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3 + coqtop version trunk (June 2016) *) + +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Reserved Notation "x * y" (at level 40, left associativity). +Delimit Scope type_scope with type. +Open Scope type_scope. +Global Set Universe Polymorphism. +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Set Implicit Arguments. +Global Set Nonrecursive Elimination Schemes. +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Notation "x * y" := (prod x y) : type_scope. +Axiom admit : forall {T}, T. +Delimit Scope function_scope with function. +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope. +Record PreCategory := + Build_PreCategory { + object :> Type; + morphism : object -> object -> Type; + identity : forall x, morphism x x }. +Bind Scope category_scope with PreCategory. +Record Functor (C D : PreCategory) := { object_of :> C -> D }. +Bind Scope functor_scope with Functor. +Class Isomorphic {C : PreCategory} (s d : C) := {}. +Definition oppositeC (C : PreCategory) : PreCategory + := @Build_PreCategory C (fun s d => morphism C d s) admit. +Notation "C ^op" := (oppositeC C) (at level 3, format "C '^op'") : category_scope. +Definition oppositeF C D (F : Functor C D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) (object_of F). +Definition set_cat : PreCategory := @Build_PreCategory Type (fun x y => x -> y) admit. +Definition prodC (C D : PreCategory) : PreCategory + := @Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + admit. +Infix "*" := prodC : category_scope. +Section composition. + Variables B C D E : PreCategory. + Definition composeF (G : Functor D E) (F : Functor C D) : Functor C E := Build_Functor C E (fun c => G (F c)). +End composition. +Infix "o" := composeF : functor_scope. +Definition fstF {C D} : Functor (C * D) C := admit. +Definition sndF {C D} : Functor (C * D) D := admit. +Definition prodF C D D' (F : Functor C D) (F' : Functor C D') : Functor C (D * D') := admit. +Local Infix "*" := prodF : functor_scope. +Definition pairF C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D') + := (F o fstF) * (F' o sndF). +Section hom_functor. + Variable C : PreCategory. + Local Notation obj_of c'c := + ((morphism + C + (fst (c'c : object (C^op * C))) + (snd (c'c : object (C^op * C))))). + Definition hom_functor : Functor (C^op * C) set_cat + := Build_Functor (C^op * C) set_cat (fun c'c => obj_of c'c). +End hom_functor. +Definition identityF C : Functor C C := admit. +Definition functor_category (C D : PreCategory) : PreCategory + := @Build_PreCategory (Functor C D) admit admit. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic (C -> D) F G. + +Section Adjunction. + Variables C D : PreCategory. + Variable F : Functor C D. + Variable G : Functor D C. + + Record AdjunctionHom := + { + mate_of : @NaturalIsomorphism + (prodC (oppositeC C) D) + (@set_cat) + (@composeF + (prodC (oppositeC C) D) + (prodC (oppositeC D) D) + (@set_cat) (@hom_functor D) + (@pairF (oppositeC C) + (oppositeC D) D D + (@oppositeF C D F) (identityF D))) + (@composeF + (prodC (oppositeC C) D) + (prodC (oppositeC C) C) + (@set_cat) (@hom_functor C) + (@pairF (oppositeC C) + (oppositeC C) D C + (identityF (oppositeC C)) G)) + }. +End Adjunction.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v new file mode 100644 index 0000000000..4cec43184c --- /dev/null +++ b/test-suite/bugs/closed/4780.v @@ -0,0 +1,106 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *) +(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 + coqtop version 8.5pl1 (April 2016) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Global Set Universe Polymorphism. +Global Set Asymmetric Patterns. +Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..)) + (at level 200, x binder, right associativity, + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") + : type_scope. +Definition relation (A : Type) := A -> A -> Type. +Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z. +Tactic Notation "etransitivity" open_constr(y) := + let R := match goal with |- ?R ?x ?z => constr:(R) end in + let x := match goal with |- ?R ?x ?z => constr:(x) end in + let z := match goal with |- ?R ?x ?z => constr:(z) end in + refine (@transitivity _ R _ x y z _ _). +Tactic Notation "etransitivity" := etransitivity _. +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation pr1 := projT1. +Notation pr2 := projT2. +Notation "x .1" := (projT1 x) (at level 3) : fibration_scope. +Notation "x .2" := (projT2 x) (at level 3) : fibration_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Arguments paths_rect [A] a P f y p. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Delimit Scope path_scope with path. +Local Open Scope path_scope. +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Instance transitive_paths {A} : Transitive (@paths A) | 0 := @concat A. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Notation "1" := idpath : path_scope. +Notation "p @ q" := (concat p q) (at level 20) : path_scope. +Notation "p ^" := (inverse p) (at level 3) : path_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): + p # (f x) = f y + := match p with idpath => idpath end. +Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B) + (p : x = y) (z : P (f x)) + : transport (fun x => P (f x)) p z = transport P (ap f p) z. +admit. +Defined. +Local Open Scope path_scope. +Generalizable Variables X A B C f g n. +Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (pq : {p : u.1 = v.1 & p # u.2 = v.2}) + : u = v + := match pq with + | existT p q => + match u, v return (forall p0 : (u.1 = v.1), (p0 # u.2 = v.2) -> (u=v)) with + | (x;y), (x';y') => fun p1 q1 => + match p1 in (_ = x'') return (forall y'', (p1 # y = y'') -> (x;y)=(x'';y'')) with + | idpath => fun y' q2 => + match q2 in (_ = y'') return (x;y) = (x;y'') with + | idpath => 1 + end + end y' q1 + end p q + end. +Definition path_sigma {A : Type} (P : A -> Type) (u v : sigT P) + (p : u.1 = v.1) (q : p # u.2 = v.2) + : u = v + := path_sigma_uncurried P u v (p;q). +Definition projT1_path `{P : A -> Type} {u v : sigT P} (p : u = v) + : u.1 = v.1 + := + ap (@projT1 _ _) p. +Notation "p ..1" := (projT1_path p) (at level 3) : fibration_scope. +Definition projT2_path `{P : A -> Type} {u v : sigT P} (p : u = v) + : p..1 # u.2 = v.2 + := (transport_compose P (@projT1 _ _) p u.2)^ + @ (@apD {x:A & P x} _ (@projT2 _ _) _ _ p). +Notation "p ..2" := (projT2_path p) (at level 3) : fibration_scope. +Definition eta_path_sigma_uncurried `{P : A -> Type} {u v : sigT P} + (p : u = v) + : path_sigma_uncurried _ _ _ (p..1; p..2) = p. +admit. +Defined. +Definition eta_path_sigma `{P : A -> Type} {u v : sigT P} (p : u = v) + : path_sigma _ _ _ (p..1) (p..2) = p + := eta_path_sigma_uncurried p. + +Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (p q : u = v) + (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2}) + : p = q. +Proof. + destruct rs, p, u. + etransitivity; [ | apply eta_path_sigma ]. + simpl in *. + induction p0. + admit. +Defined. + diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v new file mode 100644 index 0000000000..a2fa93832a --- /dev/null +++ b/test-suite/bugs/closed/4858.v @@ -0,0 +1,7 @@ +Require Import Nsatz. +Goal True. +try nsatz_compute + (PEc 0%Z :: PEc (-1)%Z + :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 + :: PEsub (PEX Z 1) (PEX Z 1) :: nil). +Abort. diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v new file mode 100644 index 0000000000..f2f917b4e7 --- /dev/null +++ b/test-suite/bugs/closed/4873.v @@ -0,0 +1,72 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Coq.Compat.Coq85. + +Fixpoint tuple' T n : Type := + match n with + | O => T + | S n' => (tuple' T n' * T)%type + end. + +Definition tuple T n : Type := + match n with + | O => unit + | S n' => tuple' T n' + end. + +Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T := + match n with + | 0 => fun x => (x::nil)%list + | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list + end. + +Definition to_list {T} (n:nat) : tuple T n -> list T := + match n with + | 0 => fun _ => nil + | S n' => fun xs : tuple T (S n') => to_list' n' xs + end. + +Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n := + match n return _ with + | 0 => + match xs return (length xs = 0 -> tuple' T 0) with + | nil => fun _ => y + | _ => _ (* impossible *) + end + | S n' => + match xs return (length xs = S n' -> tuple' T (S n')) with + | cons x xs' => fun _ => (from_list' x n' xs' _, y) + | _ => _ (* impossible *) + end + end. +Goal True. + pose from_list'_obligation_3 as e. + repeat (let e' := fresh in + rename e into e'; + (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e); + subst e'). + progress hnf in e. + pose (eq_refl : e = eq_refl). + exact I. +Qed. + +Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n := +match n return _ with +| 0 => + match xs return (length xs = 0 -> tuple T 0) with + | nil => fun _ : 0 = 0 => tt + | _ => _ (* impossible *) + end +| S n' => + match xs return (length xs = S n' -> tuple T (S n')) with + | cons x xs' => fun _ => from_list' x n' xs' _ + | _ => _ (* impossible *) + end +end. + +Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs. +Proof. + destruct xs; simpl; intros; subst; auto. + generalize dependent t. simpl in *. + induction xs; simpl in *; intros; congruence. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v new file mode 100644 index 0000000000..5569798d54 --- /dev/null +++ b/test-suite/bugs/closed/4880.v @@ -0,0 +1,11 @@ +Require Import Coq.Reals.Reals Coq.nsatz.Nsatz. +Local Open Scope R. + +Goal forall x y : R, + x*x = y * y -> + x*x = -y * -y -> + x*(x*x) = 0 -> (* The associativity does not actually matter, *) + (x*x)*x = 0. (* just otherwise [assumption] would solve the goal. *) +Proof. + nsatz. +Qed. diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v new file mode 100644 index 0000000000..219d532ac6 --- /dev/null +++ b/test-suite/bugs/closed/4932.v @@ -0,0 +1,44 @@ +(* Testing recursive notations with binders seen as terms *) + +Inductive ftele : Type := +| fb {T:Type} : T -> ftele +| fr {T} : (T -> ftele) -> ftele. + +Fixpoint args ftele : Type := + match ftele with + | fb _ => unit + | fr f => sigT (fun t => args (f t)) + end. + +Definition fpack := sigT args. +Definition pack fp fa : fpack := existT _ fp fa. + +Notation "'tele' x .. z := b" := + ( + (fun x => .. + (fun z => + pack + (fr (fun x => .. ( fr (fun z => fb b) ) .. ) ) + (existT _ x .. (existT _ z tt) .. ) + ) .. + ) + ) (at level 85, x binder, z binder). + +Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt)) + (existT _ (y,z) tt). + +Example test := tele (t : Type) := tt. +Example test' := test nat. +Print test. + +Example test2 := tele (t : Type) (x:t) := tt. +Example test2' := test2 nat 0. +Print test2. + +Example test3 := tele (t : Type) (y:=0) (x:t) := tt. +Example test3' := test3 nat 0. +Print test3. + +Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt. +Example test4' := test4 nat (1,2) 3. +Print test4. diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 008fb72c4e..73da464bbe 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -22,8 +22,8 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o Ltac present_obj from to := match goal with - | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * - | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * + | [ _ : context[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * + | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. Section NaturalTransformationComposition. diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v index 5e5d5ab3e7..3d16e7ac0d 100644 --- a/test-suite/bugs/closed/HoTT_coq_058.v +++ b/test-suite/bugs/closed/HoTT_coq_058.v @@ -95,10 +95,10 @@ Goal forall (T : Type) (T0 : T -> T -> Type) | tt => idpath end)) (x1; p) = (x1; p). intros. -let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in -let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in -let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in -let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in +let F := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in +let H := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in +let X := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in +let T := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in let t0 := fresh "t0" in let t1 := fresh "t1" in let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in @@ -116,7 +116,7 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in let GL1' := fresh in set (GL0' := GL0); - let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in + let arg := match GL0 with context[x0 ?arg] => constr:(arg) end in assert (t1 = arg) by (subst t1; reflexivity); subst t1; pattern (x0 arg) in GL0'; match goal with diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v deleted file mode 100644 index 9a14641a57..0000000000 --- a/test-suite/bugs/opened/3383.v +++ /dev/null @@ -1,7 +0,0 @@ -Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. -intro. -Fail lazymatch goal with -| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ] - => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f) -end. (* Toplevel input, characters 153-154: -Error: The reference P was not found in the current environment. *) diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v new file mode 100644 index 0000000000..3ca5c095f5 --- /dev/null +++ b/test-suite/bugs/opened/4803.v @@ -0,0 +1,34 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *) +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache Binary files differindex 297ac255d3..8e5708cf02 100644 --- a/test-suite/csdp.cache +++ b/test-suite/csdp.cache diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 6354ad469e..62e9ef4b20 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -5,3 +5,6 @@ Unable to unify "nat" with "True". The command has indeed failed with message: In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". +The command has indeed failed with message: +Ltac call to "instantiate" failed. +Error: Instance is not well-typed in the environment of ?x. diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 352c87385f..424d24801c 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -16,3 +16,12 @@ Goal True. Fail simpl; apply 0. Fail simpl; f 0. Abort. + +(* Test instantiate error messages *) + +Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1. +intros T1 P1 H1. +eexists ?[x]. +destruct H1 as [x1 H1]. +Fail instantiate (x:=projT1 x1). +Abort. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index d9ce42c606..20101f48e5 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a : nat exists myx y : bool, myx = y : Prop -fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 +fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 : Prop diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out new file mode 100644 index 0000000000..360f379676 --- /dev/null +++ b/test-suite/output/Notations3.out @@ -0,0 +1,100 @@ +[<0, 2 >] + : nat * nat * (nat * nat) +[<0, 2 >] + : nat * nat * (nat * nat) +(0, 2, (2, 2)) + : nat * nat * (nat * nat) +pair (pair O (S (S O))) (pair (S (S O)) O) + : prod (prod nat nat) (prod nat nat) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (2, (2, 0))) + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (0, (2, 4))) + : nat * nat * nat * (nat * (nat * nat)) +pair (pair (pair O (S (S O))) (S (S (S (S O))))) + (pair (S (S (S (S O)))) (pair (S (S O)) O)) + : prod (prod (prod nat nat) nat) (prod nat (prod nat nat)) +ETA x y : nat, Nat.add + : nat -> nat -> nat +ETA x y : nat, Nat.add + : nat -> nat -> nat +ETA x y : nat, Nat.add + : nat -> nat -> nat +fun x y : nat => Nat.add x y + : forall (_ : nat) (_ : nat), nat +ETA x y : nat, le_S + : forall x y : nat, x <= y -> x <= S y +fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f + : (forall x : nat * (bool * unit), ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} +where +?T : [x : nat * (bool * unit) |- Type] +fun f : forall x : bool * (nat * unit), ?T => +CURRYINV (x : nat) (y : bool), f + : (forall x : bool * (nat * unit), ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} +where +?T : [x : bool * (nat * unit) |- Type] +fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f + : (forall x : unit * nat * bool, ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} +where +?T : [x : unit * nat * bool |- Type] +fun f : forall x : unit * bool * nat, ?T => +CURRYINVLEFT (x : nat) (y : bool), f + : (forall x : unit * bool * nat, ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} +where +?T : [x : unit * bool * nat |- Type] +forall n : nat, {#n | 1 > n} + : Prop +forall x : nat, {|x | x > 0|} + : Prop +exists2 x : nat, x = 1 & x = 2 + : Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x) + : nat -> Prop +fun n : nat => +foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a) + : nat -> Prop +fun n : nat => +foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0) + : nat -> Prop +fun n : nat => +foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x) + : nat -> Prop +fun n : nat => +foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x) + : nat -> Prop +fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2 + : nat -> Prop +fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2 + : nat -> Prop +fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2 + : nat -> Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x) + : nat -> Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x) + : nat -> Prop +fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3 + : nat -> Prop +fun n : nat => {|n, fun _ : nat => n = 0 |}_3 + : nat -> Prop +fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0)) + : nat -> Prop +fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4 + : nat -> Prop +fun n : nat => {|n, fun _ : nat => n = 0 |}_4 + : nat -> Prop +fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0)) + : nat -> Prop +fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) + : nat -> Prop +tele (t : Type) '(y, z) (x : t0) := tt + : forall t : Type, nat * nat -> t -> fpack diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v new file mode 100644 index 0000000000..4b8bfe3124 --- /dev/null +++ b/test-suite/output/Notations3.v @@ -0,0 +1,141 @@ +(**********************************************************************) +(* Check printing of notations with several instances of a recursive pattern *) +(* Was wrong but I could not trigger a problem due to the collision between *) +(* different instances of ".." *) + +Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)). +Check [<0,2>]. +Check ((0,2),(2,0)). +Check ((0,2),(2,2)). +Unset Printing Notations. +Check [<0,2>]. +Set Printing Notations. + +Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)). +Check <<0,2,4>>. +Check (((0,2),4),(4,(2,0))). +Check (((0,2),4),(2,(2,0))). +Check (((0,2),4),(0,(2,4))). +Unset Printing Notations. +Check <<0,2,4>>. +Set Printing Notations. + +(**********************************************************************) +(* Check notations with recursive notations both in binders and terms *) + +Notation "'ETA' x .. y , f" := + (fun x => .. (fun y => (.. (f x) ..) y ) ..) + (at level 200, x binder, y binder). +Check ETA (x:nat) (y:nat), Nat.add. +Check ETA (x y:nat), Nat.add. +Check ETA x y, Nat.add. +Unset Printing Notations. +Check ETA (x:nat) (y:nat), Nat.add. +Set Printing Notations. +Check ETA x y, le_S. + +Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRY (x:nat) (y:bool), f. + +Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYINV (x:nat) (y:bool), f. + +Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYLEFT (x:nat) (y:bool), f. + +Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. + +(**********************************************************************) +(* Notations with variables bound both as a term and as a binder *) +(* This is #4592 *) + +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). +Check forall n:nat, {# n | 1 > n}. + +Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. +Notation "{| x | P |}" := (foo x (fun x => P)). +Check forall x:nat, {| x | x > 0 |}. + +Check ex2 (fun x => x=1) (fun x0 => x0=2). + +(* Other tests about alpha-conversions: the following notation + contains all three kinds of bindings: + + - x is bound in the lhs as a term and a binder: its name is forced + by its position as a term; it can bind variables in P + - y is bound in the lhs as a binder only: its name is given by its + name as a binder in the term to display; it can bind variables in P + - z is a binder local to the rhs; it cannot bind a variable in P +*) + +Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop. +Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)). + +(* Not printable: z (resp c, n) occurs in P *) +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x). +Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a). +Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n). +Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x). +Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x). + +(* Printable *) +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x). +Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n). +Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x). + +(* Not printable: renaming x into n would bind the 2nd occurrence of n *) +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x). +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x). + +(* Other tests *) +Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop. +Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)). + +(* Printable *) +Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z). +Check fun n => foo3 n (fun x y z => (fun _ => z=0) z). + +(* Not printable: renaming z in n would hide the renaming of x into n *) +Check fun n => foo3 n (fun x y z => (fun _ => x=0) z). + +(* Other tests *) +Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop. +Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)). + +(* Printable *) +Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z). +Check fun n => foo4 n (fun x y z => (fun _ => x=0) z). + +(* Not printable: y, z not allowed to occur in P *) +Check fun n => foo4 n (fun x y z => (fun _ => z=0) z). +Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). + +(**********************************************************************) +(* Test printing of #4932 *) + +Inductive ftele : Type := +| fb {T:Type} : T -> ftele +| fr {T} : (T -> ftele) -> ftele. + +Fixpoint args ftele : Type := + match ftele with + | fb _ => unit + | fr f => sigT (fun t => args (f t)) + end. + +Definition fpack := sigT args. +Definition pack fp fa : fpack := existT _ fp fa. + +Notation "'tele' x .. z := b" := + (fun x => .. (fun z => + pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) ) + (existT _ x .. (existT _ z tt) .. ) + ) ..) + (at level 85, x binder, z binder). + +Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 6a28475d7b..c012a86b01 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -4,28 +4,36 @@ fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -proj_informative = fun 'exist _ x _ => x : A +proj_informative = fun '(exist _ x _) => x : A : {x : A | P x} -> A -foo = fun 'Bar n b tt p => if b then n + p else n - p +foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat baz = -fun 'Bar n1 _ tt p1 => fun 'Bar _ _ tt _ => n1 + p1 +fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 : Foo -> Foo -> nat -λ '(x, y), (y, x) - : A * B → B * A -∀ '(x, y), swap (x, y) = (y, x) - : Prop swap = -fun (A B : Type) (pat : A * B) => let '(x, y) := pat in (y, x) +fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A Arguments A, B are implicit and maximally inserted Argument scopes are [type_scope type_scope _] -forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x) +fun (A B : Type) '(x, y) => swap (x, y) = (y, x) + : forall A B : Type, A * B -> Prop +forall (A B : Type) '(x, y), swap (x, y) = (y, x) + : Prop +exists '(x, y), swap (x, y) = (y, x) : Prop -exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x) +exists '(x, y) '(z, w), swap (x, y) = (z, w) + : Prop +λ '(x, y), (y, x) + : A * B → B * A +∀ '(x, y), swap (x, y) = (y, x) : Prop both_z = fun pat : nat * nat => let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat +fun '(x, y) '(z, t) => swap (x, y) = (z, t) + : A * B -> B * A -> Prop +forall '(x, y) '(z, t), swap (x, y) = (z, t) + : Prop diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 8911909abc..b5c91e347b 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -21,7 +21,20 @@ Print foo. Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1. Print baz. -(** Some test involving unicode noations. *) +Module WithParameters. + +Definition swap {A B} '((x,y) : A*B) := (y,x). +Print swap. + +Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x). +Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x). + +Check exists '((x,y):A*A), swap (x,y) = (y,x). +Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w). + +End WithParameters. + +(** Some test involving unicode notations. *) Module WithUnicode. Require Import Coq.Unicode.Utf8. @@ -31,24 +44,21 @@ Module WithUnicode. End WithUnicode. - (** * Suboptimal printing *) -(** These tests show examples which expose the [let] introduced by - the pattern notation in binders. *) - Module Suboptimal. -Definition swap {A B} '((x,y) : A*B) := (y,x). -Print swap. - -Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x). - -Check exists '((x,y):A*A), swap (x,y) = (y,x). +(** This test shows an example which exposes the [let] introduced by + the pattern notation in binders. *) Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. +(** These tests show examples which do not factorize binders *) + +Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t). +Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t). + End Suboptimal. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index b72a067407..2f7c62972a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l). Notation "'intros' x" := (S x) (at level 0). Goal True -> True. intros H. exact H. Qed. + +(* Check absence of collision on ".." in nested notations with ".." *) +Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index dc0527d826..bbfe5ec420 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -136,3 +136,18 @@ Inductive I : nat -> Type := C : I 0 | D : I 0. Goal ~C=D. congruence. Qed. + +(* Example by Jonathan Leivant, congruence up to universes *) +Section JLeivant. + Variables S1 S2 : Set. + + Definition T1 : Type := S1. + Definition T2 : Type := S2. + + Goal T1 = T1. + congruence. + Undo. + unfold T1. + congruence. + Qed. +End JLeivant. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index b5e6ccd618..2fa7704941 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -47,7 +47,9 @@ Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). Proof. Fail reflexivity. Abort. +Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }. +Fail Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 39bc59a653..21b78b5337 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -70,3 +70,9 @@ Coercion sigT_of_sig : sig >-> sigT. Coercion sig_of_sigT : sigT >-> sig. Coercion sigT2_of_sig2 : sig2 >-> sigT2. Coercion sig2_of_sigT2 : sigT2 >-> sig2. + +(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *) +Require Coq.Lists.List. +Require Coq.Vectors.VectorDef. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 1e30ab9197..54621cc1cd 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -8,6 +8,10 @@ (** Compatibility file for making Coq act similar to Coq v8.5 *) +(** Any compatibility changes to make future versions of Coq behave like Coq 8.6 + are likely needed to make them behave like Coq 8.5. *) +Require Export Coq.Compat.Coq86. + (* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not behave as "intros [H|H]" but leave instead hypotheses quantified in the goal, here producing subgoals A->C and B->C. *) diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v new file mode 100644 index 0000000000..6952fdf199 --- /dev/null +++ b/theories/Compat/Coq86.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.6 *)
\ No newline at end of file diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget index 43b197004f..7ffb86ebbd 100644 --- a/theories/Compat/vo.itarget +++ b/theories/Compat/vo.itarget @@ -1,3 +1,4 @@ AdmitAxiom.vo Coq84.vo Coq85.vo +Coq86.vo diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 9a227ad130..3c5690a724 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => constructor; congruence. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). +Notation option_map := option_map (compat "8.4"). + Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index a3eb91ec65..5d1e87ae0c 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -55,12 +55,6 @@ Ltac contradict H := | _ => (elim H;fail) || pos H end. -(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*) - -Ltac swap H := - idtac "swap is OBSOLETE: use contradict instead."; - intro; apply H; clear H. - (* To contradict an hypothesis without copying its type. *) Ltac absurd_hyp H := diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 985ecaf279..b5b17e5e8d 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -34,7 +34,7 @@ Section Well_founded. destruct 1; trivial. Defined. - Global Implicit Arguments Acc_inv [x y] [x]. + Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. (** A relation is well-founded if every element is accessible *) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c67..bd59159bb5 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 7384790dae..dfd6b0eae0 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -264,7 +264,7 @@ Ltac bang := match goal with | |- ?x => match x with - | appcontext [False_rect _ ?p] => elim p + | context [False_rect _ ?p] => elim p end end. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index a2fd05cd96..c490ea5166 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -211,7 +211,7 @@ Ltac fold_sub f := match goal with | [ |- ?T ] => match T with - appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] => + context C [ @Fix_sub _ _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index f116c5580d..b86df7c80e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -293,8 +293,9 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function let cmxss = List.rev_append cmos mllibs in let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles); - ("NATIVEFILES",vfiles);("CMIFILES",cmis)] + [("VOFILES",vfiles);("VFILES",vfiles); + ("GLOBFILES",vfiles);("NATIVEFILES",vfiles); + ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in if is_install = Project_file.UnspecInstall then begin @@ -306,12 +307,6 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function print "\n"; end; if not_empty cmxss then begin - print "install-byte:\n"; - install_include_by_root "0755" - (vars_to_put_by_root [("CMOFILES",cmos);("CMAFILES",mllibs)] inc); - print "\n"; - end; - if not_empty cmxss then begin print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n"; printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; @@ -470,10 +465,10 @@ let implicit () = in let v_rules () = print "$(VOFILES): %.vo: %.v\n"; - print "\t$(SHOW)COQC $*\n"; - print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "\t$(SHOW)COQC $<\n"; + print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; + print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; + print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n"; print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; @@ -482,7 +477,7 @@ let implicit () = print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; print "\t$(SHOW)'COQDEP $<'\n"; print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" + print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n" in if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); @@ -511,7 +506,7 @@ let variables is_install opt (args,defs) = end; (* Coq executables and relative variables *) if !some_vfile || !some_mlpackfile || !some_mllibfile then - print "COQDEP?=\"$(COQBIN)coqdep\" -c -dyndep var\n"; + print "COQDEP?=\"$(COQBIN)coqdep\" -c\n"; if !some_vfile then begin print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQCHKFLAGS?=-silent -o\n"; @@ -542,16 +537,7 @@ else CAMLP4EXTEND= endif\n"; print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ - $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n"; - print "ifeq '$(OPT)' '-byte'\n"; - print "USEBYTE:=true\n"; - print "DYNOBJ:=.cmo\n"; - print "DYNLIB:=.cma\n"; - print "else\n"; - print "USEBYTE:=\n"; - print "DYNOBJ:=.cmxs\n"; - print "DYNLIB:=.cmxs\n"; - print "endif\n\n"; + $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () @@ -770,19 +756,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "HASNATDYNLINK_OR_EMPTY :=\n"; print "endif\n\n"; section "Definition of the toplevel targets."; - let has_cmo = !some_mlfile || !some_ml4file || !some_mlpackfile in - let has_ml = has_cmo || !some_mllibfile in - print "all:"; - if !some_vfile then print " $(VOFILES)"; - if has_ml then print " $(if $(USEBYTE),bytefiles,optfiles)"; + print "all: "; + if !some_vfile then print "$(VOFILES) "; + if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; + if !some_mllibfile then print "$(CMAFILES) "; + if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile + then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; print_list "\\\n " other_targets; print "\n\n"; - print "bytefiles:"; - if has_cmo then print " $(CMOFILES)"; - if !some_mllibfile then print " $(CMAFILES)"; - print "\n\n"; - print "optfiles:"; - if has_ml then print " $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES))"; - print "\n\n"; if !some_mlifile then begin print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; @@ -828,11 +808,9 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = print ".PHONY: "; print_list " " - ("all" :: "archclean" :: "beautify" :: "byte" :: "bytefiles" - :: "clean" :: "cleanall" - :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-byte" - :: "install-doc" :: "install-natdynlink" :: "install-toploop" - :: "opt" :: "optfiles" :: "printenv" + ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall" + :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc" + :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv" :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo" :: (sds@(CList.map_filter (fun (n,_,is_phony,_) -> diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 991a3221f4..a7c32e1d65 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -320,25 +320,19 @@ let treat_coq_file chan = List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> [] - | Byte -> [base,suff] - | Opt -> [base,".cmxs"] - | Both -> [base,suff; base,".cmxs"] - | Variable -> - if suff=".cmo" then [base,"$(DYNOBJ)"] - else [base,"$(DYNLIB)"] + let base = file_name s dir in + let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in + (escape base, suff ^ opt) in let decl acc str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) @ acc + | Some mldir -> (declare ".cma" mldir s) :: acc | None -> match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) @ acc + | Some mldir -> (declare ".cmo" mldir s) :: acc | None -> acc else acc in @@ -455,7 +449,6 @@ let usage () = 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"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -483,22 +476,17 @@ let rec parse = function | "-slash" :: ll -> Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; parse ll - | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll - | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll - | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll - | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll - | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep () = if Array.length Sys.argv < 2 then usage (); - if not Coq_config.has_natdynlink then option_dynlink := No; parse (List.tl (Array.to_list Sys.argv)); (* Add current dir with empty logical path if not set by options above. *) (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) with Not_found -> add_norec_dir_import add_known "." []); + if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) if !option_boot then begin add_rec_dir_import add_known "theories" ["Coq"]; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 25f62d2bec..6fc826833e 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -16,11 +16,7 @@ open Coqdep_common *) let rec parse = function - | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll - | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll - | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll - | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll - | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll + | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) | "-mldep" :: ocamldep :: ll -> diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 8bf7fee4bd..cc63c13d7b 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -15,7 +15,7 @@ open Minisys behavior is the one of [coqdep -boot]. Its only dependencies are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via - options (see for instance [option_dynlink] below). + options (see for instance [option_natdynlk] below). *) module StrSet = Set.Make(String) @@ -26,11 +26,9 @@ module StrListMap = Map.Make(StrList) let stderr = Pervasives.stderr let stdout = Pervasives.stdout -type dynlink = Opt | Byte | Both | No | Variable - let option_c = ref false let option_noglob = ref false -let option_dynlink = ref Both +let option_natdynlk = ref true let option_boot = ref false let option_mldep = ref None @@ -382,16 +380,10 @@ let rec traite_fichier_Coq suffixe verbose f = end) strl | Declare sl -> let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> () - | Byte -> printf " %s%s" base suff - | Opt -> printf " %s.cmxs" base - | Both -> printf " %s%s %s.cmxs" base suff base - | Variable -> - printf " %s%s" base - (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") - in + let base = file_name s dir in + let opt = if !option_natdynlk then " "^base^".cmxs" else "" in + printf " %s%s%s" (escape base) suff opt + in let decl str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then begin diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 205e99176c..633c474ada 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -19,10 +19,7 @@ val find_dir_logpath: string -> string list val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref - -type dynlink = Opt | Byte | Both | No | Variable - -val option_dynlink : dynlink ref +val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : StrSet.t ref val suffixe : string ref diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli deleted file mode 100644 index 2c9b3fb8e8..0000000000 --- a/tools/coqdoc/cdglobals.mli +++ /dev/null @@ -1,49 +0,0 @@ -type target_language = LaTeX | HTML | TeXmacs | Raw -val target_language : target_language ref -type output_t = StdOut | MultFiles | File of string -val output_dir : string ref -val out_to : output_t ref -val out_channel : out_channel ref -val ( / ) : string -> string -> string -val coqdoc_out : string -> string -val open_out_file : string -> unit -val close_out_file : unit -> unit -type glob_source_t = NoGlob | DotGlob | GlobFile of string -val glob_source : glob_source_t ref -val normalize_path : string -> string -val normalize_filename : string -> string * string -val guess_coqlib : unit -> string -val header_trailer : bool ref -val header_file : string ref -val header_file_spec : bool ref -val footer_file : string ref -val footer_file_spec : bool ref -val quiet : bool ref -val light : bool ref -val gallina : bool ref -val short : bool ref -val index : bool ref -val multi_index : bool ref -val index_name : string ref -val toc : bool ref -val page_title : string ref -val title : string ref -val externals : bool ref -val coqlib : string ref -val coqlib_path : string ref -val raw_comments : bool ref -val parse_comments : bool ref -val plain_comments : bool ref -val toc_depth : int option ref -val lib_name : string ref -val lib_subtitles : bool ref -val interpolate : bool ref -val inline_notmono : bool ref -val charset : string ref -val inputenc : string ref -val latin1 : bool ref -val utf8 : bool ref -val set_latin1 : unit -> unit -val set_utf8 : unit -> unit -type coq_module = string -type file = Vernac_file of string * coq_module | Latex_file of string diff --git a/toplevel/command.ml b/toplevel/command.ml index f92ea027dd..097865648e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1251,6 +1251,11 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." +let collect_evars_of_term evd c ty = + let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) + evars (Evd.from_ctx (Evd.evar_universe_context evd)) + let do_program_recursive local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = @@ -1268,8 +1273,9 @@ let do_program_recursive local p fixkind fixl ntns = and typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in + let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - Obligations.eterm_obligations env id evd + Obligations.eterm_obligations env id evm (List.length rec_sign) def typ in (id, def, typ, imps, evars) in diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5438b163a3..d9cd574a04 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -130,7 +130,8 @@ let init_ocaml_path () = [ "grammar" ]; [ "ide" ]; [ "ltac" ]; ] let get_compat_version = function - | "8.5" -> Flags.Current + | "8.6" -> Flags.Current + | "8.5" -> Flags.V8_5 | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7c0b9bec21..c49a97cadb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -54,7 +54,7 @@ let init_color () = Terminal.has_style Unix.stderr && (* emacs compilation buffer does not support colors by default, its TERM variable is set to "dumb". *) - Unix.getenv "TERM" <> "dumb" + try Sys.getenv "TERM" <> "dumb" with Not_found -> false in if has_color then begin let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in @@ -200,6 +200,7 @@ let require () = let add_compat_require v = match v with | Flags.V8_4 -> add_require "Coq.Compat.Coq84" + | Flags.V8_5 -> add_require "Coq.Compat.Coq85" | _ -> () let compile_list = ref ([] : (bool * string) list) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1e4c3c8f11..b3eae3765b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1147,6 +1147,11 @@ let error_not_allowed_case_analysis isrec kind i = strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) (fst i) ++ str "." +let error_not_allowed_dependent_analysis isrec i = + str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + strbrk " is not allowed for inductive definition " ++ + pr_inductive (Global.env()) i ++ str "." + let error_not_mutual_in_scheme ind ind' = if eq_ind ind ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ @@ -1178,6 +1183,8 @@ let explain_recursion_scheme_error = function | NotAllowedCaseAnalysis (isrec,k,i) -> error_not_allowed_case_analysis isrec k i | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' + | NotAllowedDependentAnalysis (isrec, i) -> + error_not_allowed_dependent_analysis isrec i (* Pattern-matching errors *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 32e0eb53b0..f9e6c207c3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -217,7 +217,11 @@ let declare_beq_scheme = declare_beq_scheme_with [] let declare_one_case_analysis_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in - let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in + let dep = + if kind == InProp then case_scheme_kind_from_prop + else if not (Inductiveops.has_dependent_elim mib) then + case_scheme_kind_from_type + else case_dep_scheme_kind_from_type in let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the @@ -237,15 +241,23 @@ let kinds_from_type = InProp,ind_dep_scheme_kind_from_type; InSet,rec_dep_scheme_kind_from_type] +let nondep_kinds_from_type = + [InType,rect_scheme_kind_from_type; + InProp,ind_scheme_kind_from_type; + InSet,rec_scheme_kind_from_type] + let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let from_prop = kind == InProp in + let depelim = Inductiveops.has_dependent_elim mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> if Sorts.List.mem sort kelim then Some kind else None) - (if from_prop then kinds_from_prop else kinds_from_type) in + (if from_prop then kinds_from_prop + else if depelim then kinds_from_type + else nondep_kinds_from_type) in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims @@ -392,7 +404,6 @@ let do_mutual_induction_scheme lnamedepindsort = let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in - (* let decltype = refresh_universes decltype in *) let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref @@ -502,7 +513,8 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in - if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then + if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) + && mib.mind_typing_flags.check_guarded then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1f1be243e8..29d7457321 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -858,18 +858,17 @@ let obligation_terminator name num guard hook auto pf = in let obl = { obl with obl_status = false, status } in let uctx = Evd.evar_context_universe_context ctx in - let (def, obl) = declare_obligation prg obl body ty uctx in + let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in try ignore (update_obls prg obls (pred rem)); - if def then - if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then + if pred rem > 0 then + begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then ignore (auto (Some name) None deps) - end + end with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 0559934ec7..f83ada466b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -179,7 +179,7 @@ let display_cmd_header loc com = str " [" ++ str cmd ++ str "] ") -let rec vernac_com verbose checknav (loc,com) = +let rec vernac_com checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in @@ -193,7 +193,7 @@ let rec vernac_com verbose checknav (loc,com) = end; begin try - read_vernac_file verbosely f; + Flags.silently (read_vernac_file verbosely) f; restore_translator_coqdoc st; with reraise -> let reraise = CErrors.push reraise in @@ -203,7 +203,7 @@ let rec vernac_com verbose checknav (loc,com) = | v when !just_parsing -> () - | v -> Stm.interp verbose (loc,v) + | v -> Stm.interp (Flags.is_verbose()) (loc,v) in try checknav loc com; @@ -232,7 +232,7 @@ and read_vernac_file verbosely s = while true do let loc_ast = parse_sentence input in CWarnings.set_current_loc (fst loc_ast); - vernac_com verbosely checknav loc_ast + vernac_com checknav loc_ast; done with any -> (* whatever the exception *) let (e, info) = CErrors.push any in @@ -256,7 +256,7 @@ let checknav loc ast = if is_deep_navigation_vernac ast then user_error loc "Navigation commands forbidden in nested commands" -let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast +let eval_expr loc_ast = vernac_com checknav loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () |