diff options
| -rw-r--r-- | .merlin | 14 | ||||
| -rw-r--r-- | API/API.mli | 18 | ||||
| -rw-r--r-- | META.coq | 18 | ||||
| -rw-r--r-- | Makefile.build | 55 | ||||
| -rw-r--r-- | Makefile.checker | 2 | ||||
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | Makefile.ide | 2 | ||||
| -rw-r--r-- | appveyor.yml | 20 | ||||
| -rw-r--r-- | clib/backtrace.ml (renamed from lib/backtrace.ml) | 0 | ||||
| -rw-r--r-- | clib/backtrace.mli (renamed from lib/backtrace.mli) | 0 | ||||
| -rw-r--r-- | clib/bigint.ml (renamed from lib/bigint.ml) | 0 | ||||
| -rw-r--r-- | clib/bigint.mli (renamed from lib/bigint.mli) | 0 | ||||
| -rw-r--r-- | clib/cArray.ml (renamed from lib/cArray.ml) | 0 | ||||
| -rw-r--r-- | clib/cArray.mli (renamed from lib/cArray.mli) | 0 | ||||
| -rw-r--r-- | clib/cEphemeron.ml (renamed from lib/cEphemeron.ml) | 0 | ||||
| -rw-r--r-- | clib/cEphemeron.mli (renamed from lib/cEphemeron.mli) | 0 | ||||
| -rw-r--r-- | clib/cList.ml (renamed from lib/cList.ml) | 0 | ||||
| -rw-r--r-- | clib/cList.mli (renamed from lib/cList.mli) | 0 | ||||
| -rw-r--r-- | clib/cMap.ml (renamed from lib/cMap.ml) | 0 | ||||
| -rw-r--r-- | clib/cMap.mli (renamed from lib/cMap.mli) | 0 | ||||
| -rw-r--r-- | clib/cObj.ml (renamed from lib/cObj.ml) | 0 | ||||
| -rw-r--r-- | clib/cObj.mli (renamed from lib/cObj.mli) | 0 | ||||
| -rw-r--r-- | clib/cSet.ml (renamed from lib/cSet.ml) | 0 | ||||
| -rw-r--r-- | clib/cSet.mli (renamed from lib/cSet.mli) | 0 | ||||
| -rw-r--r-- | clib/cSig.mli (renamed from lib/cSig.mli) | 0 | ||||
| -rw-r--r-- | clib/cStack.ml (renamed from lib/cStack.ml) | 0 | ||||
| -rw-r--r-- | clib/cStack.mli (renamed from lib/cStack.mli) | 0 | ||||
| -rw-r--r-- | clib/cString.ml (renamed from lib/cString.ml) | 0 | ||||
| -rw-r--r-- | clib/cString.mli (renamed from lib/cString.mli) | 0 | ||||
| -rw-r--r-- | clib/cThread.ml (renamed from lib/cThread.ml) | 0 | ||||
| -rw-r--r-- | clib/cThread.mli (renamed from lib/cThread.mli) | 0 | ||||
| -rw-r--r-- | clib/cUnix.ml (renamed from lib/cUnix.ml) | 0 | ||||
| -rw-r--r-- | clib/cUnix.mli (renamed from lib/cUnix.mli) | 0 | ||||
| -rw-r--r-- | clib/canary.ml (renamed from lib/canary.ml) | 0 | ||||
| -rw-r--r-- | clib/canary.mli (renamed from lib/canary.mli) | 0 | ||||
| -rw-r--r-- | clib/clib.mllib (renamed from lib/clib.mllib) | 49 | ||||
| -rw-r--r-- | clib/deque.ml (renamed from lib/deque.ml) | 0 | ||||
| -rw-r--r-- | clib/deque.mli (renamed from lib/deque.mli) | 0 | ||||
| -rw-r--r-- | clib/dyn.ml (renamed from lib/dyn.ml) | 0 | ||||
| -rw-r--r-- | clib/dyn.mli (renamed from lib/dyn.mli) | 0 | ||||
| -rw-r--r-- | clib/exninfo.ml (renamed from lib/exninfo.ml) | 0 | ||||
| -rw-r--r-- | clib/exninfo.mli (renamed from lib/exninfo.mli) | 0 | ||||
| -rw-r--r-- | clib/hMap.ml (renamed from lib/hMap.ml) | 0 | ||||
| -rw-r--r-- | clib/hMap.mli (renamed from lib/hMap.mli) | 0 | ||||
| -rw-r--r-- | clib/hashcons.ml (renamed from lib/hashcons.ml) | 0 | ||||
| -rw-r--r-- | clib/hashcons.mli (renamed from lib/hashcons.mli) | 0 | ||||
| -rw-r--r-- | clib/hashset.ml (renamed from lib/hashset.ml) | 0 | ||||
| -rw-r--r-- | clib/hashset.mli (renamed from lib/hashset.mli) | 0 | ||||
| -rw-r--r-- | clib/heap.ml (renamed from lib/heap.ml) | 0 | ||||
| -rw-r--r-- | clib/heap.mli (renamed from lib/heap.mli) | 0 | ||||
| -rw-r--r-- | clib/iStream.ml (renamed from lib/iStream.ml) | 0 | ||||
| -rw-r--r-- | clib/iStream.mli (renamed from lib/iStream.mli) | 0 | ||||
| -rw-r--r-- | clib/int.ml (renamed from lib/int.ml) | 0 | ||||
| -rw-r--r-- | clib/int.mli (renamed from lib/int.mli) | 0 | ||||
| -rw-r--r-- | clib/minisys.ml (renamed from lib/minisys.ml) | 0 | ||||
| -rw-r--r-- | clib/monad.ml (renamed from lib/monad.ml) | 0 | ||||
| -rw-r--r-- | clib/monad.mli (renamed from lib/monad.mli) | 0 | ||||
| -rw-r--r-- | clib/option.ml (renamed from lib/option.ml) | 0 | ||||
| -rw-r--r-- | clib/option.mli (renamed from lib/option.mli) | 0 | ||||
| -rw-r--r-- | clib/predicate.ml (renamed from lib/predicate.ml) | 0 | ||||
| -rw-r--r-- | clib/predicate.mli (renamed from lib/predicate.mli) | 0 | ||||
| -rw-r--r-- | clib/segmenttree.ml (renamed from lib/segmenttree.ml) | 0 | ||||
| -rw-r--r-- | clib/segmenttree.mli (renamed from lib/segmenttree.mli) | 0 | ||||
| -rw-r--r-- | clib/store.ml (renamed from lib/store.ml) | 0 | ||||
| -rw-r--r-- | clib/store.mli (renamed from lib/store.mli) | 0 | ||||
| -rw-r--r-- | clib/terminal.ml (renamed from lib/terminal.ml) | 0 | ||||
| -rw-r--r-- | clib/terminal.mli (renamed from lib/terminal.mli) | 0 | ||||
| -rw-r--r-- | clib/trie.ml (renamed from lib/trie.ml) | 0 | ||||
| -rw-r--r-- | clib/trie.mli (renamed from lib/trie.mli) | 0 | ||||
| -rw-r--r-- | clib/unicode.ml (renamed from lib/unicode.ml) | 0 | ||||
| -rw-r--r-- | clib/unicode.mli (renamed from lib/unicode.mli) | 0 | ||||
| -rw-r--r-- | clib/unicodetable.ml (renamed from lib/unicodetable.ml) | 0 | ||||
| -rw-r--r-- | clib/unionfind.ml (renamed from lib/unionfind.ml) | 0 | ||||
| -rw-r--r-- | clib/unionfind.mli (renamed from lib/unionfind.mli) | 0 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | dev/ci/appveyor.bat | 2 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 11 | ||||
| -rw-r--r-- | dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh | 9 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06217-coqdep-at-once.sh | 3 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/README.md | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 7 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 6 | ||||
| -rw-r--r-- | grammar/tacextend.mlp | 14 | ||||
| -rw-r--r-- | interp/declare.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 3 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 4 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 3 | ||||
| -rw-r--r-- | kernel/cClosure.ml | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 2 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 7 | ||||
| -rw-r--r-- | lib/lib.mllib | 39 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 18 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 3 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 13 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 8 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 5 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | printing/printmod.ml | 6 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetCompat.v | 44 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 39 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 91 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 3 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 6 |
127 files changed, 309 insertions, 316 deletions
@@ -1,17 +1,17 @@ FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50 +S clib +B clib S config B config -S ide -B ide S lib B lib -S intf -B intf S kernel B kernel S kernel/byterun B kernel/byterun +S intf +B intf S library B library S engine @@ -30,14 +30,16 @@ S parsing B parsing S stm B stm -S toplevel -B toplevel S vernac B vernac +S toplevel +B toplevel S plugins/ltac B plugins/ltac S API B API +S ide +B ide S tools B tools diff --git a/API/API.mli b/API/API.mli index 892c05b64d..1d0c32273a 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1443,9 +1443,9 @@ sig type record_body = (Id.t * Constant.t array * projection_body array) option type recursivity_kind = - | Finite - | CoFinite - | BiFinite + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) type mutual_inductive_body = { mind_packets : one_inductive_body array; @@ -2160,10 +2160,14 @@ module Decl_kinds : sig type polymorphic = bool type cumulative_inductive_flag = bool + type recursivity_kind = Declarations.recursivity_kind = - | Finite - | CoFinite - | BiFinite + | Finite (** = inductive *) + [@ocaml.deprecated "Please use [Declarations.Finite"] + | CoFinite (** = coinductive *) + [@ocaml.deprecated "Please use [Declarations.CoFinite"] + | BiFinite (** = non-recursive, like in "Record" definitions *) + [@ocaml.deprecated "Please use [Declarations.BiFinite"] [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] type discharge = @@ -4308,7 +4312,7 @@ sig type typeclass = { cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; - cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; + cl_context : Globnames.global_reference option list * Context.Rel.t; cl_props : Context.Rel.t; cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option * Names.Constant.t option) list; @@ -23,19 +23,27 @@ package "config" ( ) +package "clib" ( + description = "Base General Coq Library" + version = "8.7" + + directory = "clib" + requires = "str, unix, threads" + + archive(byte) = "clib.cma" + archive(native) = "clib.cmxa" +) + package "lib" ( - description = "Base Coq Library" + description = "Base Coq-Specific Library" version = "8.7" directory = "lib" - requires = "str, unix, threads, coq.config" + requires = "coq.clib, coq.config" - archive(byte) = "clib.cma" archive(byte) += "lib.cma" - - archive(native) = "clib.cmxa" archive(native) += "lib.cmxa" ) diff --git a/Makefile.build b/Makefile.build index 2f7ce6ef35..33ab72e689 100644 --- a/Makefile.build +++ b/Makefile.build @@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile -LOCALINCLUDES=$(if $(filter plugins/%,$@),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) +LOCALINCLUDES=$(if $(filter plugins/%,$@),-I clib -I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) @@ -417,7 +417,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) # coqc -COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo +COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -438,21 +438,21 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # Remember to update the dependencies below when you add files! COQDEPBOOTSRC := \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ + clib/segmenttree.cmo clib/unicodetable.cmo clib/unicode.cmo clib/minisys.cmo \ tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo -lib/segmenttree.cmo : lib/segmenttree.cmi -lib/segmenttree.cmx : lib/segmenttree.cmi -lib/unicodetable.cmo : lib/segmenttree.cmo -lib/unicodetable.cmx : lib/segmenttree.cmx -lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi -lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi -lib/minisys.cmo : lib/unicode.cmo -lib/minisys.cmx : lib/unicode.cmx -tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi -tools/coqdep_lexer.cmx : lib/unicode.cmx tools/coqdep_lexer.cmi -tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi -tools/coqdep_common.cmx : lib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi +clib/segmenttree.cmo : clib/segmenttree.cmi +clib/segmenttree.cmx : clib/segmenttree.cmi +clib/unicodetable.cmo : clib/segmenttree.cmo +clib/unicodetable.cmx : clib/segmenttree.cmx +clib/unicode.cmo : clib/unicodetable.cmo clib/unicode.cmi +clib/unicode.cmx : clib/unicodetable.cmx clib/unicode.cmi +clib/minisys.cmo : clib/unicode.cmo +clib/minisys.cmx : clib/unicode.cmx +tools/coqdep_lexer.cmo : clib/unicode.cmi tools/coqdep_lexer.cmi +tools/coqdep_lexer.cmx : clib/unicode.cmx tools/coqdep_lexer.cmi +tools/coqdep_common.cmo : clib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi +tools/coqdep_common.cmx : clib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi tools/coqdep_boot.cmo : tools/coqdep_common.cmi tools/coqdep_boot.cmx : tools/coqdep_common.cmx @@ -466,10 +466,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ - lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ - tools/coqdep.cmo +COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo \ + tools/coqdep_common.cmo tools/coqdep.cmo $(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -479,7 +477,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,) -COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo +COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' @@ -493,23 +491,24 @@ $(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -package str) -COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ +COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) $(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -package str,unix) -$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) +$(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ - ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ - ide/richpp.cmo ide/xmlprotocol.cmo tools/fake_ide.cmo +FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo \ + ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo \ + ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo \ + tools/fake_ide.cmo $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' @@ -517,7 +516,7 @@ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) # votour: a small vo explorer (based on the checker) -bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo) +bin/votour: $(call bestobj, clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker) @@ -525,7 +524,7 @@ bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo # Csdp to micromega special targets ########################################################################### -CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ +CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ mutils.cmo micromega.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) @@ -581,7 +580,7 @@ kernel/kernel.cma: kernel/kernel.mllib # Make sure that API/API.mli cannot leak types from the Coq codebase. API/API.cmi : API/API.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -I lib -I $(MYCAMLP4LIB) -c $< + $(HIDE)$(OCAMLC) -I clib -I lib -I $(MYCAMLP4LIB) -c $< %.cma: %.mllib $(SHOW)'OCAMLC -a -o $@' diff --git a/Makefile.checker b/Makefile.checker index 7e0f588759..5b5855782f 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -20,7 +20,7 @@ CHICKEN:=bin/coqchk$(EXE) # The sources -CHKLIBS:= -I config -I lib -I checker +CHKLIBS:= -I config -I clib -I lib -I checker ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread diff --git a/Makefile.common b/Makefile.common index f436d3e8f1..7e8f3e3e74 100644 --- a/Makefile.common +++ b/Makefile.common @@ -73,7 +73,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ - config lib kernel intf kernel/byterun library \ + config clib lib kernel intf kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel API @@ -100,7 +100,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ +CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma API/API.cma diff --git a/Makefile.ide b/Makefile.ide index 7d809f67a5..08829b5544 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -41,7 +41,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -IDEDEPS:=lib/clib.cma lib/cErrors.cmo lib/spawn.cmo +IDEDEPS:=clib/clib.cma lib/lib.cma IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma diff --git a/appveyor.yml b/appveyor.yml index 92fc629b30..64c1bedb54 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -12,22 +12,20 @@ environment: matrix: - USEOPAM: true ARCH: 64 -# Comment out until issue #5998 is fixed. -# - USEOPAM: false -# ARCH: 32 -# - USEOPAM: false -# ARCH: 64 + - USEOPAM: false + ARCH: 32 + - USEOPAM: false + ARCH: 64 build_script: - cmd: 'call %APPVEYOR_BUILD_FOLDER%\dev\ci\appveyor.bat' test: off -# Comment out until issue #5998 is fixed. -#artifacts: -# - path: 'dev\nsis\*.exe' -# name: installer +artifacts: + - path: 'dev\nsis\*.exe' + name: installer -# - path: 'coq-opensource-archive-*.zip' -# name: opensource-archive + - path: 'coq-opensource-archive-*.zip' + name: opensource-archive diff --git a/lib/backtrace.ml b/clib/backtrace.ml index be9f40c1fb..be9f40c1fb 100644 --- a/lib/backtrace.ml +++ b/clib/backtrace.ml diff --git a/lib/backtrace.mli b/clib/backtrace.mli index dd82165b6d..dd82165b6d 100644 --- a/lib/backtrace.mli +++ b/clib/backtrace.mli diff --git a/lib/bigint.ml b/clib/bigint.ml index 4f8b95d592..4f8b95d592 100644 --- a/lib/bigint.ml +++ b/clib/bigint.ml diff --git a/lib/bigint.mli b/clib/bigint.mli index 2a5a5f122d..2a5a5f122d 100644 --- a/lib/bigint.mli +++ b/clib/bigint.mli diff --git a/lib/cArray.ml b/clib/cArray.ml index 013585735c..013585735c 100644 --- a/lib/cArray.ml +++ b/clib/cArray.ml diff --git a/lib/cArray.mli b/clib/cArray.mli index 325ff8edcc..325ff8edcc 100644 --- a/lib/cArray.mli +++ b/clib/cArray.mli diff --git a/lib/cEphemeron.ml b/clib/cEphemeron.ml index 8b253a7901..8b253a7901 100644 --- a/lib/cEphemeron.ml +++ b/clib/cEphemeron.ml diff --git a/lib/cEphemeron.mli b/clib/cEphemeron.mli index d8a1f27573..d8a1f27573 100644 --- a/lib/cEphemeron.mli +++ b/clib/cEphemeron.mli diff --git a/lib/cList.ml b/clib/cList.ml index 0ef7c3d8ba..0ef7c3d8ba 100644 --- a/lib/cList.ml +++ b/clib/cList.ml diff --git a/lib/cList.mli b/clib/cList.mli index f87db04cf4..f87db04cf4 100644 --- a/lib/cList.mli +++ b/clib/cList.mli diff --git a/lib/cMap.ml b/clib/cMap.ml index b4c4aedd0e..b4c4aedd0e 100644 --- a/lib/cMap.ml +++ b/clib/cMap.ml diff --git a/lib/cMap.mli b/clib/cMap.mli index 5e65bd200a..5e65bd200a 100644 --- a/lib/cMap.mli +++ b/clib/cMap.mli diff --git a/lib/cObj.ml b/clib/cObj.ml index 7f3ee18553..7f3ee18553 100644 --- a/lib/cObj.ml +++ b/clib/cObj.ml diff --git a/lib/cObj.mli b/clib/cObj.mli index 16933a4aa4..16933a4aa4 100644 --- a/lib/cObj.mli +++ b/clib/cObj.mli diff --git a/lib/cSet.ml b/clib/cSet.ml index ed65edf16e..ed65edf16e 100644 --- a/lib/cSet.ml +++ b/clib/cSet.ml diff --git a/lib/cSet.mli b/clib/cSet.mli index 2eb9bce869..2eb9bce869 100644 --- a/lib/cSet.mli +++ b/clib/cSet.mli diff --git a/lib/cSig.mli b/clib/cSig.mli index 32e9d2af0c..32e9d2af0c 100644 --- a/lib/cSig.mli +++ b/clib/cSig.mli diff --git a/lib/cStack.ml b/clib/cStack.ml index 4acb2930c5..4acb2930c5 100644 --- a/lib/cStack.ml +++ b/clib/cStack.ml diff --git a/lib/cStack.mli b/clib/cStack.mli index 8dde1d1a1a..8dde1d1a1a 100644 --- a/lib/cStack.mli +++ b/clib/cStack.mli diff --git a/lib/cString.ml b/clib/cString.ml index f2242460e8..f2242460e8 100644 --- a/lib/cString.ml +++ b/clib/cString.ml diff --git a/lib/cString.mli b/clib/cString.mli index 29d3a44995..29d3a44995 100644 --- a/lib/cString.mli +++ b/clib/cString.mli diff --git a/lib/cThread.ml b/clib/cThread.ml index 0221e690e8..0221e690e8 100644 --- a/lib/cThread.ml +++ b/clib/cThread.ml diff --git a/lib/cThread.mli b/clib/cThread.mli index 66f039bb52..66f039bb52 100644 --- a/lib/cThread.mli +++ b/clib/cThread.mli diff --git a/lib/cUnix.ml b/clib/cUnix.ml index 34fb660db4..34fb660db4 100644 --- a/lib/cUnix.ml +++ b/clib/cUnix.ml diff --git a/lib/cUnix.mli b/clib/cUnix.mli index d08dc4c403..d08dc4c403 100644 --- a/lib/cUnix.mli +++ b/clib/cUnix.mli diff --git a/lib/canary.ml b/clib/canary.ml index 0ed1d28f37..0ed1d28f37 100644 --- a/lib/canary.ml +++ b/clib/canary.ml diff --git a/lib/canary.mli b/clib/canary.mli index 904b88213c..904b88213c 100644 --- a/lib/canary.mli +++ b/clib/canary.mli diff --git a/lib/clib.mllib b/clib/clib.mllib index 5c1f7d9af8..bd5ddb1525 100644 --- a/lib/clib.mllib +++ b/clib/clib.mllib @@ -1,37 +1,38 @@ -Coq_config - -Terminal Canary -Hook +CObj +CEphemeron + Hashset Hashcons + CSet CMap +CList +CString +CStack + Int -Dyn HMap +Bigint + +CArray Option +CUnix + +Segmenttree +Unicodetable +Unicode +Minisys +CThread +Trie +Predicate +Heap +Unionfind + +Dyn Store Exninfo Backtrace IStream -Flags -Control -Loc -CAst -DAst -CList -CString -Deque -CObj -CArray -CStack -Util -Stateid -Pp -Feedback -CUnix -Envars -Aux_file +Terminal Monad -CoqProject_file diff --git a/lib/deque.ml b/clib/deque.ml index 373269b4f5..373269b4f5 100644 --- a/lib/deque.ml +++ b/clib/deque.ml diff --git a/lib/deque.mli b/clib/deque.mli index 23cb1e4919..23cb1e4919 100644 --- a/lib/deque.mli +++ b/clib/deque.mli diff --git a/lib/dyn.ml b/clib/dyn.ml index 64535d35f6..64535d35f6 100644 --- a/lib/dyn.ml +++ b/clib/dyn.ml diff --git a/lib/dyn.mli b/clib/dyn.mli index 2206394e2d..2206394e2d 100644 --- a/lib/dyn.mli +++ b/clib/dyn.mli diff --git a/lib/exninfo.ml b/clib/exninfo.ml index 167d3d6dc8..167d3d6dc8 100644 --- a/lib/exninfo.ml +++ b/clib/exninfo.ml diff --git a/lib/exninfo.mli b/clib/exninfo.mli index c960ac7c08..c960ac7c08 100644 --- a/lib/exninfo.mli +++ b/clib/exninfo.mli diff --git a/lib/hMap.ml b/clib/hMap.ml index 37079af783..37079af783 100644 --- a/lib/hMap.ml +++ b/clib/hMap.ml diff --git a/lib/hMap.mli b/clib/hMap.mli index c77bfced88..c77bfced88 100644 --- a/lib/hMap.mli +++ b/clib/hMap.mli diff --git a/lib/hashcons.ml b/clib/hashcons.ml index ee22325811..ee22325811 100644 --- a/lib/hashcons.ml +++ b/clib/hashcons.ml diff --git a/lib/hashcons.mli b/clib/hashcons.mli index fbd2ebcf9a..fbd2ebcf9a 100644 --- a/lib/hashcons.mli +++ b/clib/hashcons.mli diff --git a/lib/hashset.ml b/clib/hashset.ml index 7f96627a68..7f96627a68 100644 --- a/lib/hashset.ml +++ b/clib/hashset.ml diff --git a/lib/hashset.mli b/clib/hashset.mli index ec79205a5c..ec79205a5c 100644 --- a/lib/hashset.mli +++ b/clib/hashset.mli diff --git a/lib/heap.ml b/clib/heap.ml index a6109972d7..a6109972d7 100644 --- a/lib/heap.ml +++ b/clib/heap.ml diff --git a/lib/heap.mli b/clib/heap.mli index 93d504c5ac..93d504c5ac 100644 --- a/lib/heap.mli +++ b/clib/heap.mli diff --git a/lib/iStream.ml b/clib/iStream.ml index d3a54332a1..d3a54332a1 100644 --- a/lib/iStream.ml +++ b/clib/iStream.ml diff --git a/lib/iStream.mli b/clib/iStream.mli index cd7940e8d3..cd7940e8d3 100644 --- a/lib/iStream.mli +++ b/clib/iStream.mli diff --git a/lib/int.ml b/clib/int.ml index 63f62154d8..63f62154d8 100644 --- a/lib/int.ml +++ b/clib/int.ml diff --git a/lib/int.mli b/clib/int.mli index b65367f7d4..b65367f7d4 100644 --- a/lib/int.mli +++ b/clib/int.mli diff --git a/lib/minisys.ml b/clib/minisys.ml index 389b18ad4e..389b18ad4e 100644 --- a/lib/minisys.ml +++ b/clib/minisys.ml diff --git a/lib/monad.ml b/clib/monad.ml index 2e55e9698c..2e55e9698c 100644 --- a/lib/monad.ml +++ b/clib/monad.ml diff --git a/lib/monad.mli b/clib/monad.mli index 7b0a3e600f..7b0a3e600f 100644 --- a/lib/monad.mli +++ b/clib/monad.mli diff --git a/lib/option.ml b/clib/option.ml index 98b1680354..98b1680354 100644 --- a/lib/option.ml +++ b/clib/option.ml diff --git a/lib/option.mli b/clib/option.mli index 66f05023f7..66f05023f7 100644 --- a/lib/option.mli +++ b/clib/option.mli diff --git a/lib/predicate.ml b/clib/predicate.ml index 1aa7db6af1..1aa7db6af1 100644 --- a/lib/predicate.ml +++ b/clib/predicate.ml diff --git a/lib/predicate.mli b/clib/predicate.mli index cee3b0bd39..cee3b0bd39 100644 --- a/lib/predicate.mli +++ b/clib/predicate.mli diff --git a/lib/segmenttree.ml b/clib/segmenttree.ml index d0ded4cb59..d0ded4cb59 100644 --- a/lib/segmenttree.ml +++ b/clib/segmenttree.ml diff --git a/lib/segmenttree.mli b/clib/segmenttree.mli index e274a6fdc8..e274a6fdc8 100644 --- a/lib/segmenttree.mli +++ b/clib/segmenttree.mli diff --git a/lib/store.ml b/clib/store.ml index 97a8fea085..97a8fea085 100644 --- a/lib/store.ml +++ b/clib/store.ml diff --git a/lib/store.mli b/clib/store.mli index 5cc5bb8593..5cc5bb8593 100644 --- a/lib/store.mli +++ b/clib/store.mli diff --git a/lib/terminal.ml b/clib/terminal.ml index 34efddfbca..34efddfbca 100644 --- a/lib/terminal.ml +++ b/clib/terminal.ml diff --git a/lib/terminal.mli b/clib/terminal.mli index b1b76e6e2a..b1b76e6e2a 100644 --- a/lib/terminal.mli +++ b/clib/terminal.mli diff --git a/lib/trie.ml b/clib/trie.ml index 0b0ba27613..0b0ba27613 100644 --- a/lib/trie.ml +++ b/clib/trie.ml diff --git a/lib/trie.mli b/clib/trie.mli index a87acc8a69..a87acc8a69 100644 --- a/lib/trie.mli +++ b/clib/trie.mli diff --git a/lib/unicode.ml b/clib/unicode.ml index f193c4e0f8..f193c4e0f8 100644 --- a/lib/unicode.ml +++ b/clib/unicode.ml diff --git a/lib/unicode.mli b/clib/unicode.mli index 32ffbb8e94..32ffbb8e94 100644 --- a/lib/unicode.mli +++ b/clib/unicode.mli diff --git a/lib/unicodetable.ml b/clib/unicodetable.ml index b607058c64..b607058c64 100644 --- a/lib/unicodetable.ml +++ b/clib/unicodetable.ml diff --git a/lib/unionfind.ml b/clib/unionfind.ml index f9c92d6a8e..f9c92d6a8e 100644 --- a/lib/unionfind.ml +++ b/clib/unionfind.ml diff --git a/lib/unionfind.mli b/clib/unionfind.mli index b242232edb..b242232edb 100644 --- a/lib/unionfind.mli +++ b/clib/unionfind.mli diff --git a/configure.ml b/configure.ml index 06aa5e7666..0698d93e26 100644 --- a/configure.ml +++ b/configure.ml @@ -1143,7 +1143,7 @@ let write_configml f = core_src_dirs in pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; - pr "\nlet api_dirs = [\"API\"; \"lib\"]\n"; + pr "\nlet api_dirs = [\"API\"; \"clib\"; \"lib\"]\n"; pr "\nlet plugins_dirs = [\n"; let plugins = Sys.readdir "plugins" in diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f12cbe0a78..c467678215 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1087,7 +1087,7 @@ function copy_coq_license { install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true - install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" + install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt" @@ -1174,7 +1174,7 @@ function make_mingw_make { if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then # The config.h.win32 file is fine - don't edit it # We need to copy the mingw gcc here as "gcc" - then the batch file will use it - cp /usr/bin/${ARCH}-w64-mingw32-gcc-5.4.0.exe ./gcc.exe + cp /usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe ./gcc.exe # By some magic cygwin bash can run batch files logn build ./build_w32.bat gcc # Copy make to Coq folder diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index e2fbf1f6d1..72ee89962c 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -37,5 +37,5 @@ if %USEOPAM% == true ( GOTO :EOF :ErrorExit - ECHO ERROR MakeCoq_MinGW.bat failed + ECHO ERROR %0 failed EXIT /b 1 diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 23131c94c6..58c90ff11d 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -5,8 +5,17 @@ set -xe if [ -n "${GITLAB_CI}" ]; then export COQBIN=`pwd`/_install_ci/bin - export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" + export CI_BRANCH="$CI_COMMIT_REF_NAME" else + if [ -n "${TRAVIS}" ]; + then + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" + elif [ -n "${CIRCLECI}" ]; + then + export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" + export CI_BRANCH="$CIRCLE_BRANCH" + fi export COQBIN=`pwd`/bin fi export PATH="$COQBIN:$PATH" diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index af4a96f4ae..7716bcb59a 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,4 +1,4 @@ -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh deleted file mode 100644 index 5c4dd1324f..0000000000 --- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then - formal_topology_CI_BRANCH=ci - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git - - HoTT_CI_BRANCH=coq-pr-1033 - HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git - - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh deleted file mode 100644 index cdca8e525a..0000000000 --- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then - ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer - ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git -fi diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh deleted file mode 100644 index 6741cf26fb..0000000000 --- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then - ltac2_CI_BRANCH=master - ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2 -fi diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh deleted file mode 100644 index c9f1272bed..0000000000 --- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then - ltac2_CI_BRANCH=localityfixyou - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git -fi diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh deleted file mode 100644 index 68e1901f7f..0000000000 --- a/dev/ci/user-overlays/06217-coqdep-at-once.sh +++ /dev/null @@ -1,3 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then - UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git -fi diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh deleted file mode 100644 index 7e9b5febdd..0000000000 --- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then - Equations_CI_BRANCH=fix-coq-6324 - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh deleted file mode 100644 index c0dcf79e1d..0000000000 --- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then - Equations_CI_BRANCH=econstr+fix_class - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh deleted file mode 100644 index 8aea7dee3a..0000000000 --- a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then - Equations_CI_BRANCH=interp+less_impstyle_p2 - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9146d3d521..9f0377ceea 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub Example: `00669-maximedenes-ssr-merge.sh` containing ``` -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi ``` + +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 01aa6b599b..f6fbb69424 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -68,6 +68,13 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +### XML IDE Protocol + +- Before 8.8, `Query` only executed the first command present in the + `query` string; starting with 8.8, the caller may include several + statements. This is useful for instance for temporarily setting an + option and then executing a command. + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 18f6288f6f..b35571e9ca 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -330,6 +330,12 @@ the STM API, `force` triggers a `Join`. <string>${message}</string> </value> ``` + +Before 8.8, `Query` only executed the first command present in the +`query` string; starting with 8.8, the caller may include several +statements. This is useful for instance for temporarily setting an +option and then executing a command. + ------------------------------- diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 0b33dab051..c52a0040bf 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -45,7 +45,7 @@ let rec make_let raw e = function <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l -let make_clause (pt,_,e) = +let make_clause (pt,e) = (make_patt pt, ploc_vala None, make_let false e pt) @@ -76,7 +76,7 @@ let make_prod_item = function <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >> let mlexpr_of_clause cl = - mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl + mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl (** Special treatment of constr entries *) let is_constr_gram = function @@ -88,8 +88,8 @@ let make_var = function | ExtNonTerminal (_, p) -> p | _ -> assert false -let declare_tactic loc tacname ~level classification clause = match clause with -| [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> +let declare_tactic loc tacname ~level clause = match clause with +| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in @@ -141,16 +141,14 @@ EXTEND str_item: [ [ "TACTIC"; "EXTEND"; s = tac_name; level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ]; - c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ]; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> let level = match level with Some i -> int_of_string i | None -> 0 in - declare_tactic loc s ~level c l ] ] + declare_tactic loc s ~level l ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; - c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ]; - "->"; "["; e = Pcaml.expr; "]" -> (l,c,e) + "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] ; tacargs: diff --git a/interp/declare.ml b/interp/declare.ml index 5be07e09ec..d1b79ffcdd 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -349,7 +349,7 @@ let dummy_one_inductive_entry mie = { let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = None; - mind_entry_finite = Decl_kinds.BiFinite; + mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 0197cf9ae2..d7962e29a6 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -68,6 +68,7 @@ let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state open Decl_kinds +open Declarations let type_of_logical_kind = function | IsDefinition def -> @@ -111,14 +112,12 @@ let type_of_global_ref gr = | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> None then - let open Decl_kinds in begin match mib.Declarations.mind_finite with | Finite -> "indrec" | BiFinite -> "rec" | CoFinite -> "corec" end else - let open Decl_kinds in begin match mib.Declarations.mind_finite with | Finite -> "ind" | BiFinite -> "variant" diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index f7c36c4e5f..bfe73160bb 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + (Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index b0c1f66613..b9a3f0c212 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -77,6 +77,9 @@ type logical_kind = type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) + [@ocaml.deprecated "Please use [Declarations.Finite"] | CoFinite (** = coinductive *) + [@ocaml.deprecated "Please use [Declarations.CoFinite"] | BiFinite (** = non-recursive, like in "Record" definitions *) + [@ocaml.deprecated "Please use [Declarations.BiFinite"] [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 31ded9129a..11616da7b3 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -810,7 +810,7 @@ let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (_,projs,pbs)) when - mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + mib.Declarations.mind_finite == Declarations.BiFinite -> (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8e9b606a58..1f2ae0b6cc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( best-effort fashion. *) let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in - let recursive = finite != Decl_kinds.BiFinite in + let recursive = finite != BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let ra_env_ar = Array.rev_to_list rc in let nparamsctxt = Context.Rel.length paramsctxt in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2a629f00a9..28a09b81b0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -38,14 +38,14 @@ let find_inductive env c = let (t, l) = decompose_app (whd_all env c) in match kind t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_all env c) in match kind t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index de4dc21079..160a90dc2f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -515,7 +515,7 @@ let rec lambda_of_constr env sigma c = { asw_ind = ind; asw_ci = ci; asw_reloc = tbl; - asw_finite = mib.mind_finite <> Decl_kinds.CoFinite; + asw_finite = mib.mind_finite <> CoFinite; asw_prefix = prefix} in (* translation of the argument *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2913c6dfad..d0d5cb1d56 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -193,7 +193,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (arities_of_specif (mind, inst) (mib2, p2)) in let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in - check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x); + check (fun mib -> mib.mind_finite<>CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x); check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x); assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps); assert (Array.length mib1.mind_packets >= 1 diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 970666638c..34f9aed37b 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -113,6 +113,7 @@ let exists_dir dir = let process_cmd_line orig_dir proj args = + let parsing_project_file = ref (proj.project_file <> None) in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in @@ -155,16 +156,22 @@ let process_cmd_line orig_dir proj args = aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r | "-f" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file)); let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () | Some _ -> Feedback.msg_warning (Pp.str "Multiple project files are deprecated.") in + parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in + parsing_project_file := false; aux proj r | "-o" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file)); if String.contains file '/' then error "Output file must be in the current directory"; if proj.makefile <> None then diff --git a/lib/lib.mllib b/lib/lib.mllib index 66f939a910..b2260ba097 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,21 +1,30 @@ +Coq_config + +Hook +Flags +Control +Util + +Pp +Stateid +Loc +Feedback CErrors CWarnings -Bigint -Segmenttree -Unicodetable -Unicode -Minisys + +Rtree System -CThread -Spawn -Trie -CProfile Explore -Predicate -Rtree -Heap -Unionfind -Genarg -CEphemeron +RTree +CProfile Future +Spawn + +CAst +DAst +Genarg + RemoteCounter +Aux_file +Envars +CoqProject_file diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6ecc8355cb..92e60f4656 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -15,6 +15,7 @@ open Constrexpr_ops open Extend open Vernacexpr open Decl_kinds +open Declarations open Misctypes open Tok (* necessary for camlp4 *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 4ae875cd70..c169b7b50b 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -431,7 +431,7 @@ and extract_really_ind env kn mib = let ip = (kn, 0) in let r = IndRef ip in if is_custom r then raise (I Standard); - if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive); + if mib.mind_finite == CoFinite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); let p,u = packets.(0) in if p.ip_logical then raise (I Standard); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 97066e5312..b4e17c5d1c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1498,7 +1498,7 @@ let do_build_inductive try with_full_print (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) - Decl_kinds.Finite + Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9fcb35f89e..8f5d3f22f4 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -20,10 +20,10 @@ open Names open Term open Constr open Vars -open Declarations open Glob_term open Glob_termops open Decl_kinds +open Declarations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -353,8 +353,8 @@ let ind2name = Id.of_string "__ind2" be co-inductive, and for the moment they must not be mutual either. *) let verify_inds mib1 mib2 = - if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive"; - if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive"; + if mib1.mind_finite == CoFinite then error "First argument is coinductive"; + if mib2.mind_finite == CoFinite then error "Second argument is coinductive"; if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; () @@ -891,7 +891,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] - false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9ae112d371..e5933de2a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -61,12 +61,9 @@ struct type t = Val.t -let normalize v = v - let of_constr c = in_gen (topwit wit_constr) c let to_constr v = - let v = normalize v in if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in Some c @@ -78,7 +75,6 @@ let to_constr v = let of_uconstr c = in_gen (topwit wit_uconstr) c let to_uconstr v = - let v = normalize v in if has_type v (topwit wit_uconstr) then Some (out_gen (topwit wit_uconstr) v) else None @@ -86,7 +82,6 @@ let to_uconstr v = let of_int i = in_gen (topwit wit_int) i let to_int v = - let v = normalize v in if has_type v (topwit wit_int) then Some (out_gen (topwit wit_int) v) else None @@ -108,14 +103,12 @@ let constr_of_id env id = (* Gives the constr corresponding to a Constr_context tactic_arg *) let coerce_to_constr_context v = - let v = Value.normalize v in if has_type v (topwit wit_constr_context) then out_gen (topwit wit_constr_context) v else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) let coerce_var_to_ident fresh env sigma v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -140,7 +133,6 @@ let g = sigma in let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -179,7 +171,6 @@ let id_of_name = function let coerce_to_intro_pattern env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_var) then @@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v = | _ -> raise (CannotCoerceTo "a naming introduction pattern") let coerce_to_hint_base v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) -> Id.to_string id @@ -206,13 +196,11 @@ let coerce_to_hint_base v = else raise (CannotCoerceTo "a hint base name") let coerce_to_int v = - let v = Value.normalize v in if has_type v (topwit wit_int) then out_gen (topwit wit_int) v else raise (CannotCoerceTo "an integer") let coerce_to_constr env v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a term") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -230,7 +218,6 @@ let coerce_to_constr env v = else fail () let coerce_to_uconstr env v = - let v = Value.normalize v in if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -243,7 +230,6 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in - let v = Value.normalize v in let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v = let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id @@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v = (* Interprets a qualified name *) let coerce_to_reference env sigma v = - let v = Value.normalize v in match Value.to_constr v with | Some c -> begin @@ -318,7 +302,6 @@ let coerce_to_reference env sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_decl_or_quant_hyp env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d7b253a687..dce16b7333 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -31,9 +31,6 @@ module Value : sig type t = Val.t - val normalize : t -> t - (** Eliminated the leading dynamic type casts. *) - val of_constr : constr -> t val to_constr : t -> constr option val of_uconstr : Ltac_pretype.closed_glob_constr -> t diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ccded44179..f2720954d0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v (** More naming applications *) let name_vfun appl vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) @@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = - let v = Value.normalize v in let pr_with_env pr = match env with | Some (env,sigma) -> pr env sigma @@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with | Some trace -> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -298,7 +295,6 @@ let propagate_trace ist loc id v = else Proofview.tclUNIT v let append_trace trace v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) @@ -307,11 +303,9 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = - let v = Value.normalize v in let fail () = user_err ?loc (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with let extract_ids ids lfun accu = let fold id v accu = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu @@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c = (** TODO: should use dedicated printers *) let message_of_value v = - let v = Value.normalize v in let pr_with_env pr = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in @@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg = try (** FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -1248,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run args tac and force_vrec ist v : Val.t Ftactic.t = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with @@ -1324,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in - let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1377,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> @@ -1604,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in Proofview.tclLIFT begin diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f7a3789a21..788e4d268a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1044,7 +1044,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 34df7d3d72..78e6bc6f14 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -275,7 +275,7 @@ 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 + | Some (Some _) -> mib.mind_finite == BiFinite | _ -> true (* Annotation for cases *) @@ -486,7 +486,7 @@ let find_inductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found @@ -496,7 +496,7 @@ let find_coinductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bbb3a1bb2b..bc9990d026 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -65,7 +65,7 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + cl_context : global_reference option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -175,7 +175,7 @@ let subst_class (subst,cl) = and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + List.smartmap (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in @@ -213,10 +213,10 @@ let discharge_class (_,cl) = let newgrs = List.map (fun decl -> match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None - | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + List.smartmap (Option.smartmap Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8ee061330a..0cbe1c71c0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,9 +25,8 @@ type typeclass = { cl_impl : global_reference; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. - The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + The global reference gives a direct link to the class itself. *) + cl_context : global_reference option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 30674fee27..b41fb4e4dd 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -666,7 +666,7 @@ let is_eta_constructor_app env sigma ts f l1 term = | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 647111bbe1..2b7886d115 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -235,8 +235,8 @@ 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 -> str" without eta conversion" - | Decl_kinds.BiFinite -> str " with eta conversion" + | CoFinite | Finite -> str" without eta conversion" + | BiFinite -> str " with eta conversion" in [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] diff --git a/printing/printmod.ml b/printing/printmod.ml index 05292b06ba..fb9d45a793 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -125,7 +125,7 @@ let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> "Inductive" | BiFinite -> "Variant" @@ -184,7 +184,7 @@ let print_record env mind mib udecl = (Array.to_list (Univ.Instance.to_array u)) udecl in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | BiFinite -> "Record" | Finite -> "Inductive" @@ -346,7 +346,7 @@ let print_body is_impl env mp (l,body) = pr_mutual_inductive_body env (MutInd.make2 mp l) mib None with e when CErrors.noncritical e -> let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> def "Inductive" | BiFinite -> def "Variant" diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2c8ca19722..a3a3e0a9e9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -48,7 +48,7 @@ let match_with_non_recursive_type sigma t = let (hdapp,args) = decompose_app sigma t in (match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then + if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then Some (hdapp,args) else None diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 508040ec18..4ee0a8a7b2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1492,7 +1492,7 @@ let simplest_ecase c = general_case_analysis true None (c,NoBindings) exception IsNonrec -let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Decl_kinds.BiFinite +let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite let find_ind_eliminator ind s gl = let gr = lookup_eliminator ind s in diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index b1769da3d8..31bc1cc31d 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -165,13 +165,13 @@ End Backport_WSets. (** * From new Sets to new ones *) Module Backport_Sets - (E:OrderedType.OrderedType) - (M:MSetInterface.Sets with Definition E.t := E.t - with Definition E.eq := E.eq - with Definition E.lt := E.lt) - <: FSetInterface.S with Module E:=E. + (O:OrderedType.OrderedType) + (M:MSetInterface.Sets with Definition E.t := O.t + with Definition E.eq := O.eq + with Definition E.lt := O.lt) + <: FSetInterface.S with Module E:=O. - Include Backport_WSets E M. + Include Backport_WSets O M. Implicit Type s : t. Implicit Type x y : elt. @@ -182,21 +182,21 @@ Module Backport_Sets Definition min_elt_1 : forall s x, min_elt s = Some x -> In x s := M.min_elt_spec1. Definition min_elt_2 : forall s x y, - min_elt s = Some x -> In y s -> ~ E.lt y x + min_elt s = Some x -> In y s -> ~ O.lt y x := M.min_elt_spec2. Definition min_elt_3 : forall s, min_elt s = None -> Empty s := M.min_elt_spec3. Definition max_elt_1 : forall s x, max_elt s = Some x -> In x s := M.max_elt_spec1. Definition max_elt_2 : forall s x y, - max_elt s = Some x -> In y s -> ~ E.lt x y + max_elt s = Some x -> In y s -> ~ O.lt x y := M.max_elt_spec2. Definition max_elt_3 : forall s, max_elt s = None -> Empty s := M.max_elt_spec3. - Definition elements_3 : forall s, sort E.lt (elements s) + Definition elements_3 : forall s, sort O.lt (elements s) := M.elements_spec2. Definition choose_3 : forall s s' x y, - choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y := M.choose_spec3. Definition lt_trans : forall s s' s'', lt s s' -> lt s' s'' -> lt s s'' := @StrictOrder_Transitive _ _ M.lt_strorder. @@ -211,7 +211,7 @@ Module Backport_Sets [ apply EQ | apply LT | apply GT ]; auto. Defined. - Module E := E. + Module E := O. End Backport_Sets. @@ -342,13 +342,13 @@ End Update_WSets. (** * From old Sets to new ones. *) Module Update_Sets - (E:Orders.OrderedType) - (M:FSetInterface.S with Definition E.t := E.t - with Definition E.eq := E.eq - with Definition E.lt := E.lt) - <: MSetInterface.Sets with Module E:=E. + (O:Orders.OrderedType) + (M:FSetInterface.S with Definition E.t := O.t + with Definition E.eq := O.eq + with Definition E.lt := O.lt) + <: MSetInterface.Sets with Module E:=O. - Include Update_WSets E M. + Include Update_WSets O M. Implicit Type s : t. Implicit Type x y : elt. @@ -359,21 +359,21 @@ Module Update_Sets Definition min_elt_spec1 : forall s x, min_elt s = Some x -> In x s := M.min_elt_1. Definition min_elt_spec2 : forall s x y, - min_elt s = Some x -> In y s -> ~ E.lt y x + min_elt s = Some x -> In y s -> ~ O.lt y x := M.min_elt_2. Definition min_elt_spec3 : forall s, min_elt s = None -> Empty s := M.min_elt_3. Definition max_elt_spec1 : forall s x, max_elt s = Some x -> In x s := M.max_elt_1. Definition max_elt_spec2 : forall s x y, - max_elt s = Some x -> In y s -> ~ E.lt x y + max_elt s = Some x -> In y s -> ~ O.lt x y := M.max_elt_2. Definition max_elt_spec3 : forall s, max_elt s = None -> Empty s := M.max_elt_3. - Definition elements_spec2 : forall s, sort E.lt (elements s) + Definition elements_spec2 : forall s, sort O.lt (elements s) := M.elements_3. Definition choose_spec3 : forall s s' x y, - choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y := M.choose_3. Instance lt_strorder : StrictOrder lt. @@ -407,6 +407,6 @@ Module Update_Sets Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s'). Proof. intros; unfold compare; destruct M.compare; auto. Qed. - Module E := E. + Module E := O. End Update_Sets. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 2feaaa04cd..b7a62a78c0 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,16 +27,8 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage () = - output_string stderr "Usage summary:\ -\n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ -\n ... [any] ... [-extra[-phony] result dependencies command]\ -\n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ -\n [-h] [--help]\ -\n\ +let usage_common () = + output_string stderr "\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ \n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ @@ -65,10 +57,29 @@ let usage () = \n[-install opt]: where opt is \"user\" to force install into user directory,\ \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ +\n[-bypass-API]: when compiling plugins, bypass Coq API\ +\n" + +let usage_coq_project () = + output_string stderr "Available arguments:"; + usage_common (); + exit 1 + +let usage_coq_makefile () = + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n"; + usage_common (); + output_string stderr "\ \n[-f file]: take the contents of file as arguments\ -\n[-o file]: output should go in file file\ +\n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ -\n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\n"; exit 1 @@ -380,8 +391,8 @@ let share_prefix s1 s2 = | _ -> false let _ = + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in let prog, args = - if Array.length Sys.argv = 1 then usage (); let args = Array.to_list Sys.argv in let prog = List.hd args in prog, List.tl args in @@ -392,7 +403,7 @@ let _ = let project = try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage () in + with Parsing_error s -> prerr_endline s; usage_coq_project () in if only_destination <> None then begin destination_of project (Option.get only_destination); diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 51dd5cd4f5..ec6b62ee27 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -317,7 +317,7 @@ let build_beq_scheme mode kn = let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in if not (Sorts.List.mem InSet kelim) then raise (NonSingletonProp (kn,i)); - if mib.mind_finite = Decl_kinds.CoFinite then + if mib.mind_finite = CoFinite then raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), diff --git a/vernac/classes.ml b/vernac/classes.ml index c2e9a5ab44..6914f899b7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -141,7 +141,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, _) -> match clname with - | Some (cl, b) -> + | Some cl -> let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 883121479f..d376696f76 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -11,7 +11,6 @@ open Util open Constr open Environ open Entries -open Termops open Redexpr open Declare open Constrintern @@ -49,55 +48,57 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") +let check_imps ~impsty ~impsbody = + let b = + try + List.for_all (fun (key, (va:bool*bool*bool)) -> + (* Pervasives.(=) is OK for this type *) + Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va) + impsbody + with Not_found -> false + in + if not b then warn_implicits_in_term () + let interp_definition pl bl poly red_option c ctypopt = + let open EConstr in let env = Global.env() in + (* Explicitly bound universes and constraints *) let evd, decl = Univdecls.interp_univ_decl_opt env pl in + (* Build the parameters *) let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in - let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in - let nb_args = Context.Rel.nhyps ctx in - let evd,imps,ce = - match ctypopt with - None -> - let evd, subst = Evd.nf_univ_variables evd in - let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in - let env_bl = push_rel_context ctx env in - let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in - let c = EConstr.Unsafe.to_constr c in - let evd,nf = Evarutil.nf_evars_and_universes evd in - let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in - let evd = Evd.restrict_universe_context evd vars in - let uctx = Evd.check_univ_decl ~poly evd decl in - evd, imps1@(Impargs.lift_implicits nb_args imps2), - definition_entry ~univs:uctx body - | Some ctyp -> - let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in - let evd, subst = Evd.nf_univ_variables evd in - let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in - let env_bl = push_rel_context ctx env in - let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in - let c = EConstr.Unsafe.to_constr c in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let body = nf (it_mkLambda_or_LetIn c ctx) in - let ty = EConstr.Unsafe.to_constr ty in - let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in - let beq b1 b2 = if b1 then b2 else not b2 in - let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in - (* Check that all implicit arguments inferable from the term - are inferable from the type *) - let chk (key,va) = - impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) - in - if not (try List.for_all chk imps2 with Not_found -> false) - then warn_implicits_in_term (); - let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in - let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in - let vars = Univ.LSet.union bodyvars tyvars in - let evd = Evd.restrict_universe_context evd vars in - let uctx = Evd.check_univ_decl ~poly evd decl in - evd, imps1@(Impargs.lift_implicits nb_args impsty), - definition_entry ~types:typ ~univs:uctx body + (* Build the type *) + let evd, tyopt = Option.fold_left_map + (interp_type_evars_impls ~impls env_bl) + evd ctypopt + in + (* Build the body, and merge implicits from parameters and from type/body *) + let evd, c, imps, tyopt = + match tyopt with + | None -> + let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in + evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None + | Some (ty, impsty) -> + let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in + check_imps ~impsty ~impsbody; + evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty + in + (* universe minimization *) + let evd = Evd.nf_constraints evd in + (* Substitute evars and universes, and add parameters. + Note: in program mode some evars may remain. *) + let ctx = List.map (EConstr.to_rel_decl evd) ctx in + let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in + let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in + (* Keep only useful universes. *) + let uvars_fold uvars c = + Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) in + let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in + let evd = Evd.restrict_universe_context evd uvars in + (* Check we conform to declared universes *) + let uctx = Evd.check_univ_decl ~poly evd decl in + (* We're done! *) + let ce = definition_entry ?types:tyopt ~univs:uctx c in (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps) let check_definition (ce, evd, _, imps) = diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index f3f50f41dd..1c8677e9cd 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -25,7 +25,6 @@ open Nametab open Impargs open Reductionops open Indtypes -open Decl_kinds open Pretyping open Evarutil open Indschemes @@ -411,7 +410,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = (* spiwack: raises an error if the structure is supposed to be non-recursive, but isn't *) begin match mie.mind_entry_finite with - | BiFinite when is_recursive mie -> + | Declarations.BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") else diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index e4ca98749c..2f4c95affc 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -258,7 +258,7 @@ let declare_one_induction_scheme ind = let declare_induction_schemes kn = let mib = Global.lookup_mind kn in - if mib.mind_finite <> Decl_kinds.CoFinite then begin + if mib.mind_finite <> Declarations.CoFinite then begin for i = 0 to Array.length mib.mind_packets - 1 do declare_one_induction_scheme (kn,i); done; @@ -268,7 +268,7 @@ let declare_induction_schemes kn = let declare_eq_decidability_gen internal names kn = let mib = Global.lookup_mind kn in - if mib.mind_finite <> Decl_kinds.CoFinite then + if mib.mind_finite <> Declarations.CoFinite then ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) @@ -512,7 +512,7 @@ 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) + if !elim_flag && (mib.mind_finite <> Declarations.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; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 27a680b9b6..6ef310837c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -100,7 +100,7 @@ let find_mutually_recursive_statements sigma thms = match EConstr.kind sigma t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - mind.mind_finite <> Decl_kinds.CoFinite -> + mind.mind_finite <> Declarations.CoFinite -> [ind,x,i] | _ -> []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in @@ -110,7 +110,7 @@ let find_mutually_recursive_statements sigma thms = match EConstr.kind sigma whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> + Int.equal mind.mind_ntypes n && mind.mind_finite == Declarations.CoFinite -> [ind,x,0] | _ -> [] in diff --git a/vernac/record.ml b/vernac/record.ml index 114b55cb40..d9dc16d96e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -143,7 +143,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in let assums = List.filter is_local_assum newps in let params = List.map (RelDecl.get_name %> Name.get_id) assums in - let ty = Inductive (params,(finite != BiFinite)) in + let ty = Inductive (params,(finite != Declarations.BiFinite)) in let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in let env2,sigma,impls,newfs,data = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) @@ -507,7 +507,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls + let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -523,7 +523,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari let ctx_context = List.map (fun decl -> match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with - | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) + | Some (_, ((cl,_), _)) -> Some cl.cl_impl | None -> None) params, params in |