diff options
57 files changed, 531 insertions, 372 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7ec3ba1bd7..744fe1c743 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -74,18 +74,3 @@ jobs: make -j "$NJOBS" test-suite PRINT_LOGS=1 env: NJOBS: "2" - - - name: Create the dmg bundle - run: | - eval $(opam env) - export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig - export OUTDIR="$(pwd)/_install_ci" - ./dev/build/osx/make-macos-dmg.sh - env: - MACOSX_DEPLOYMENT_TARGET: "10.11" - NJOBS: "2" - - - uses: actions/upload-artifact@v2 - with: - name: coq-macOS-installer - path: _build/*.dmg diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ce6be777f3..52b03e455b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -20,7 +20,7 @@ variables: # Format: $IMAGE-V$DATE-$hash # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g. # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10) - CACHEKEY: "bionic_coq-V2021-02-11-b601de5a7b" + CACHEKEY: "bionic_coq-V2021-04-14-802aebab96" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/Makefile.build b/Makefile.build index d619fd3c85..cbd4f4efbe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -893,7 +893,7 @@ PLUGININCLUDES=$(addprefix -I plugins/, $(PLUGINDIRS)) $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) ########################################################################### diff --git a/checker/values.ml b/checker/values.ml index f7a367b986..1353435181 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -87,7 +87,7 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|] (** kernel/univ *) -let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|] +let v_level_global = v_tuple "Level.Global.t" [|v_dp;String;Int|] let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *) [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh deleted file mode 100755 index 2550cbb31c..0000000000 --- a/dev/build/osx/make-macos-dmg.sh +++ /dev/null @@ -1,37 +0,0 @@ -#!/bin/bash - -# Fail on first error -set -e - -# Configuration setup -DMGDIR=$PWD/_dmg -VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) -APP=bin/CoqIDE_${VERSION}.app - -# Install Coq into the .app file -make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources" install-coq install-ide-toploop - -# Fill .app file with metadata and other .app specific stuff (like non-system .so) -make PRIVATEBINARIES="$APP" -j 1 -l2 "$APP" VERBOSE=1 - -# Create the dmg bundle -mkdir -p "$DMGDIR" -ln -sf /Applications "$DMGDIR/Applications" -cp -r "$APP" "$DMGDIR" - -mkdir -p _build - -# Temporary countermeasure to hdiutil error 5341 -# head -c9703424 /dev/urandom > $DMGDIR/.padding - -hdi_opts=(-volname "coq-$VERSION-installer-macos" - -srcfolder "$DMGDIR" - -ov # overwrite existing file - -format UDZO - -imagekey "zlib-level=9" - - # needed for backward compat since macOS 10.14 which uses APFS by default - # see discussion in #11803 - -fs hfs+ - ) -hdiutil create "${hdi_opts[@]}" "_build/coq-$VERSION-installer-macos.dmg" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8f14625c63..00729cd168 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc, pytest for coqtail -RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ +RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \ pytest==5.4.3 @@ -44,7 +44,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.13.0" + BASE_ONLY_OPAM="elpi.1.13.1" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh new file mode 100644 index 0000000000..d1606711dc --- /dev/null +++ b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh @@ -0,0 +1 @@ +overlay metacoq https://github.com/SkySkimmer/metacoq no-remote-counter-alt 14050 diff --git a/dev/ci/user-overlays/14111-gares-update-elpi.sh b/dev/ci/user-overlays/14111-gares-update-elpi.sh new file mode 100644 index 0000000000..8827127a38 --- /dev/null +++ b/dev/ci/user-overlays/14111-gares-update-elpi.sh @@ -0,0 +1,2 @@ +overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.5 14111 +overlay hierarchy_builder https://github.com/math-comp/hierarchy-builder coq-master+1.1.0 14111 diff --git a/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst new file mode 100644 index 0000000000..9753ce915b --- /dev/null +++ b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow scope delimiters in Ltac2 open_constr:(...) quotation + (`#13939 <https://github.com/coq/coq/pull/13939>`_, + fixes `#12806 <https://github.com/coq/coq/issues/12806>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-cli-tools/14024-coqdep-errors.rst b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst new file mode 100644 index 0000000000..355c0bd7b7 --- /dev/null +++ b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst @@ -0,0 +1,8 @@ +- **Changed:** + ``coqdep`` now reports an error if files specified on the + command line don't exist or if it encounters unreadable files. + Unknown options now generate a warning. Previously these + conditions were ignored. + (`#14024 <https://github.com/coq/coq/pull/14024>`_, + fixes `#14023 <https://github.com/coq/coq/issues/14023>`_, + by Hendrik Tews). diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index abb08d98cc..e262a9305d 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -267,6 +267,11 @@ code span.error { color: inherit !important; } + +.coqdoc-comment { + color: #808080 !important +} + /* make the error message index readable */ .indextable code { white-space: inherit; /* break long lines */ diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 06b6c61ea9..e53e6ea1cb 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -4,10 +4,80 @@ Conversion rules ---------------- Coq has conversion rules that can be used to determine if two -terms are equal by definition, or :term:`convertible`. +terms are equal by definition in |CiC|, or :term:`convertible`. Conversion rules consist of reduction rules and expansion rules. -See :ref:`applyingconversionrules`, -which describes tactics that apply these conversion rules. +Equality is determined by +converting both terms to a normal form, then verifying they are syntactically +equal (ignoring differences in the names of bound variables by +:term:`alpha-conversion <alpha-convertible>`). + +.. seealso:: :ref:`applyingconversionrules`, which describes tactics that apply these conversion rules. + +:gdef:`Reductions <reduction>` convert terms to something that is incrementally +closer to its normal form. For example, :term:`zeta-reduction` removes +:n:`let @ident := @term__1 in @term__2` constructs from a term by replacing +:n:`@ident` with :n:`@term__1` wherever :n:`@ident` appears in :n:`@term__2`. +The resulting term may be longer or shorter than the original. + +.. coqtop:: all + + Eval cbv zeta in let i := 1 in i + i. + +:gdef:`Expansions <expansion>` are reductions applied in the opposite direction, +for example expanding `2 + 2` to `let i := 2 in i + i`. While applying +reductions gives a unique result, the associated +expansion may not be unique. For example, `2 + 2` could also be +expanded to `let i := 2 in i + 2`. Reductions that have a unique inverse +expansion are also referred to as :gdef:`contractions <contraction>`. + +The normal form is defined as the result of applying a particular +set of conversion rules (beta-, delta-, iota- and zeta-reduction and eta-expansion) +repeatedly until it's no longer possible to apply any of them. + +Sometimes the result of a reduction tactic will be a simple value, for example reducing +`2*3+4` with `cbv beta delta iota` to `10`, which requires applying several +reduction rules repeatedly. In other cases, it may yield an expression containing +variables, axioms or opaque contants that can't be reduced. + +The useful conversion rules are shown below. All of them except for eta-expansion +can be applied with conversion tactics such as :tacn:`cbv`: + + .. list-table:: + :header-rows: 1 + + * - Conversion name + - Description + + * - beta-reduction + - eliminates `fun` + + * - delta-reduction + - replaces a defined variable or constant with its definition + + * - zeta-reduction + - eliminates `let` + + * - eta-expansion + - replaces a term `f` of type `forall a : A, B` with `fun x : A => f x` + + * - match-reduction + - eliminates `match` + + * - fix-reduction + - replaces a `fix` with a :term:`beta-redex`; + recursive calls to the symbol are replaced with the `fix` term + + * - cofix-reduction + - replaces a `cofix` with a :term:`beta-redex`; + recursive calls to the symbol are replaced with the `cofix` term + + * - iota-reduction + - match-, fix- and cofix-reduction together + +:ref:`applyingconversionrules` +describes tactics that only apply conversion rules. +(Other tactics may use conversion rules in addition +to other changes to the proof state.) α-conversion ~~~~~~~~~~~~ @@ -123,7 +193,7 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. .. math:: λ x:T.~(t~x)~\not\triangleright_η~t - This is because, in general, the type of :math:`t` need not to be convertible + This is because, in general, the type of :math:`t` need not be convertible to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that: .. math:: @@ -142,6 +212,30 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. +Examples +~~~~~~~~ + + .. example:: Simple delta, fix, beta and match reductions + + ``+`` is a :ref:`notation <Notations>` for ``Nat.add``, which is defined + with a :cmd:`Fixpoint`. + + .. coqtop:: all abort + + Print Nat.add. + Goal 1 + 1 = 2. + cbv delta. + cbv fix. + cbv beta. + cbv match. + + The term can be fully reduced with `cbv`: + + .. coqtop:: all abort + + Goal 1 + 1 = 2. + cbv. + .. _proof-irrelevance: Proof Irrelevance diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 294c56ef06..25ac72069b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1375,8 +1375,9 @@ table further down lists the classes that that are handled plainly. the term (as described in :ref:`LocalInterpretationRulesForNotations`). The last :token:`scope_key` is the top of the scope stack that's applied to the :token:`term`. - :n:`open_constr` - Parses an open :token:`term`. + :n:`open_constr {? ( {+, @scope_key } ) }` + Parses an open :token:`term`. Like :n:`constr` above, this class + accepts a list of notation scopes with the same effects. :n:`ident` Parses :token:`ident` or :n:`$@ident`. The first form returns :n:`ident:(@ident)`, diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bab9d35099..d4749f781a 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -609,7 +609,7 @@ Abbreviations |SSR| extends the :tacn:`set` tactic by supplying: - + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic; + + an open syntax, similarly to the :tacn:`pose <pose (ssreflect)>` tactic; + a more aggressive matching algorithm; + an improved interpretation of wildcards, taking advantage of the matching algorithm; @@ -899,7 +899,7 @@ context of a goal thanks to the ``in`` tactical. .. tacv:: set @ident := @term in {+ @ident} - This variant of :tacn:`set (ssreflect)` introduces a defined constant + This variant of :tacn:`set <set (ssreflect)>` introduces a defined constant called :token:`ident` in the context, and folds it in the context entries mentioned on the right hand side of ``in``. The body of :token:`ident` is the first subterm matching these context @@ -1202,7 +1202,7 @@ The move tactic. Goal not False. move. - More precisely, the :tacn:`move` tactic inspects the goal and does nothing + More precisely, the :tacn:`move <move (ssreflect)>` tactic inspects the goal and does nothing (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a product or a ``let … in``, and performs :tacn:`hnf` otherwise. @@ -1301,7 +1301,7 @@ The apply tactic this use of the :tacn:`refine` tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms. -:tacn:`apply (ssreflect)` has a special behavior on goals containing +:tacn:`apply <apply (ssreflect)>` has a special behavior on goals containing existential metavariables of sort :g:`Prop`. .. example:: @@ -2461,7 +2461,7 @@ The have tactic. redex, and introduces the lemma under a fresh name, automatically chosen. -Like in the case of the :n:`pose (ssreflect)` tactic (see section :ref:`definitions_ssr`), the types of +Like in the case of the :n:`pose <pose (ssreflect)>` tactic (see section :ref:`definitions_ssr`), the types of the holes are abstracted in term. .. example:: @@ -3775,7 +3775,7 @@ involves the following steps: ``forall n, F1 n = F2 n`` for ``eq_map``). 3. If so :tacn:`under` puts these n goals in head normal form (using - the defective form of the tactic :tacn:`move`), then executes + the defective form of the tactic :tacn:`move <move (ssreflect)>`), then executes the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals @@ -5665,6 +5665,7 @@ Tactics respectively. .. tacn:: move + :name: move (ssreflect) :tacn:`idtac` or :tacn:`hnf` (see :ref:`bookkeeping_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fad02b2645..7bc009fcfe 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1148,7 +1148,7 @@ Managing the local context or at the bottom of the local context. All hypotheses on which the new hypothesis depends are moved too so as to respect the order of dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` - followed by the appropriate call to :tacn:`move … after …`, + followed by the appropriate call to :tacn:`move`, :tacn:`move … before …`, :tacn:`move … at top`, or :tacn:`move … at bottom`. @@ -1235,7 +1235,6 @@ Managing the local context hypotheses that depend on it. .. tacn:: move @ident__1 after @ident__2 - :name: move … after … This moves the hypothesis named :n:`@ident__1` in the local context after the hypothesis named :n:`@ident__2`, where “after” is in reference to the @@ -1256,7 +1255,7 @@ Managing the local context :name: move … before … This moves :n:`@ident__1` towards and just before the hypothesis - named :n:`@ident__2`. As for :tacn:`move … after …`, dependencies + named :n:`@ident__2`. As for :tacn:`move`, dependencies over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies) or in the type of :n:`@ident__1` (when :n:`@ident__1` comes after :n:`@ident__2` in the order of @@ -2502,7 +2501,7 @@ and an explanation of the underlying technique. :name: inversion ... using ... .. todo using … instead of ... in the name above gives a Sphinx error, even though - this works just find for :tacn:`move … after …` + this works just find for :tacn:`move` Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index 32d3e87e68..dd1d6051b5 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -15,7 +15,7 @@ .. |c_i| replace:: `c`\ :math:`_{i}` .. |c_n| replace:: `c`\ :math:`_{n}` .. |Cic| replace:: CIC -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{βδιζ}` .. |Latex| replace:: :smallcaps:`LaTeX` .. |Ltac| replace:: `L`:sub:`tac` .. |p_1| replace:: `p`\ :math:`_{1}` diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 522b9900a5..51e26a9082 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -28,7 +28,7 @@ from bs4 import BeautifulSoup from bs4.element import NavigableString COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', - '-s', '--html', '--stdout', '--utf8'] + '-s', '--html', '--stdout', '--utf8', '--parse-comments'] COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) @@ -68,8 +68,19 @@ def lex(source): if isinstance(elem, NavigableString): yield [], elem elif elem.name == "span": - cls = "coqdoc-{}".format(elem['title']) - yield [cls], elem.string + if elem.string: + cls = "coqdoc-{}".format(elem.get("title", "comment")) + yield [cls], elem.string + else: + # handle multi-line comments + children = list(elem.children) + mlc = children[0].startswith("(*") and children[-1].endswith ("*)") + for elem2 in children: + if isinstance(elem2, NavigableString): + cls = ["coqdoc-comment"] if mlc else [] + yield cls, elem2 + elif elem2.name == 'br': + pass elif elem.name == 'br': pass else: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1428dae7ef..468b6b648d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -938,10 +938,11 @@ class CoqtopBlocksTransform(Transform): @staticmethod def split_lines(source): - r"""Split Coq input in chunks + r"""Split Coq input into chunks, which may include single- or + multi-line comments. Nested comments are not supported. A chunk is a minimal sequence of consecutive lines of the input that - ends with a '.' + ends with a '.' or '*)' >>> split_lines('A.\nB.''') ['A.', 'B.'] @@ -962,8 +963,14 @@ class CoqtopBlocksTransform(Transform): >>> split_lines('SearchHead le.\nSearchHead (@eq bool).') ['SearchHead le.', 'SearchHead (@eq bool).'] + + >>> split_lines("(* *) x. (* *)\ny.\n") + ['(* *) x. (* *)', 'y.'] + + >>> split_lines("(* *) x (* \n *)\ny.\n") + ['(* *) x (* \n *)', 'y.'] """ - return re.split(r"(?<=(?<!\.)\.)\n", source.strip()) + return re.split(r"(?:(?<=(?<!\.)\.)|(?<=\*\)))\n", source.strip()) @staticmethod def parse_options(node): @@ -1039,7 +1046,11 @@ class CoqtopBlocksTransform(Transform): if options['warn']: repl.sendone('Set Warnings "default".') for sentence in self.split_lines(node.rawsource): - pairs.append((sentence, repl.sendone(sentence))) + comment = re.compile(r"\s*\(\*.*?\*\)\s*", re.DOTALL) + wo_comments = re.sub(comment, "", sentence) + has_tac = wo_comments != "" and not wo_comments.isspace() + output = repl.sendone(sentence) if has_tac else "" + pairs.append((sentence, output)) if options['abort']: repl.sendone('Abort All.') if options['fail']: @@ -1052,9 +1063,10 @@ class CoqtopBlocksTransform(Transform): # Use Coqdoc to highlight input in_chunks = highlight_using_coqdoc(sentence) dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input'])) - # Parse ANSI sequences to highlight output - out_chunks = AnsiColorsParser().colorize_str(output) - dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) + if output: + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) node.clear() node.rawsource = self.make_rawsource(pairs, options['input'], options['output']) node['classes'].extend(self.block_classes(options['input'] or options['output'])) @@ -1180,8 +1192,7 @@ class StdGlossaryIndex(Index): if type == 'term': entries = content[itemname[0].lower()] entries.append([itemname, 0, docname, anchor, '', '', '']) - content = sorted(content.items()) - return content, False + return content.items(), False def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): """A grammar production not included in a ``prodn`` directive. diff --git a/engine/univGen.ml b/engine/univGen.ml index 278ca6bf34..b917d91512 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,14 +13,14 @@ open Names open Constr open Univ -type univ_unique_id = int (* Generator of levels *) -let new_univ_id, set_remote_new_univ_id = - RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> n) +let new_univ_id = + let cnt = ref 0 in + fun () -> incr cnt; !cnt let new_univ_global () = - Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ()) + let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in + Univ.Level.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ()) let fresh_level () = Univ.Level.make (new_univ_global ()) diff --git a/engine/univGen.mli b/engine/univGen.mli index 05737411f5..743d819747 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -13,12 +13,6 @@ open Constr open Environ open Univ - -(** The global universe counter *) -type univ_unique_id -val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer -val new_univ_id : unit -> univ_unique_id (** for the stm *) - (** Side-effecting functions creating new universe levels. *) val new_univ_global : unit -> Level.UGlobal.t diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6cb61174d3..ddbd5fa0a7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -717,7 +717,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false -let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) +let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) "" 0)) let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = let anon = Context.make_annot Anonymous Sorts.Relevant in diff --git a/kernel/univ.ml b/kernel/univ.ml index a2fd14025e..c2496f10b0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -38,20 +38,22 @@ struct open Names module UGlobal = struct - type t = DirPath.t * int + type t = DirPath.t * string * int - let make dp i = (DirPath.hcons dp,i) + let make dp s i = (DirPath.hcons dp,s,i) let repr x : t = x - let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' + let equal (d, s, i) (d', s', i') = Int.equal i i' && DirPath.equal d d' && String.equal s s' - let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d) + let hash (d,s,i) = Hashset.Combine.combine3 i (String.hash s) (DirPath.hash d) - let compare (d, i) (d', i') = - let c = Int.compare i i' in - if Int.equal c 0 then DirPath.compare d d' - else c + let compare (d, s, i) (d', s', i') = + if i < i' then -1 + else if i' < i then 1 + else let c = DirPath.compare d d' in + if not (Int.equal c 0) then c + else String.compare s s' end type t = @@ -84,10 +86,7 @@ struct | Set, Set -> 0 | Set, _ -> -1 | _, Set -> 1 - | Level (dp1, i1), Level (dp2, i2) -> - if i1 < i2 then -1 - else if i1 > i2 then 1 - else DirPath.compare dp1 dp2 + | Level l1, Level l2 -> UGlobal.compare l1 l2 | Level _, _ -> -1 | _, Level _ -> 1 | Var n, Var m -> Int.compare n m @@ -98,8 +97,8 @@ struct | SProp, SProp -> true | Prop, Prop -> true | Set, Set -> true - | Level (n,d), Level (n',d') -> - n == n' && d == d' + | Level (d,s,n), Level (d',s',n') -> + n == n' && s==s' && d == d' | Var n, Var n' -> n == n' | _ -> false @@ -107,9 +106,10 @@ struct | SProp as x -> x | Prop as x -> x | Set as x -> x - | Level (d,n) as x -> + | Level (d,s,n) as x -> + let s' = CString.hcons s in let d' = Names.DirPath.hcons d in - if d' == d then x else Level (d',n) + if s' == s && d' == d then x else Level (d',s',n) | Var _n as x -> x open Hashset.Combine @@ -119,7 +119,7 @@ struct | Prop -> combinesmall 1 1 | Set -> combinesmall 1 2 | Var n -> combinesmall 2 n - | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d)) + | Level l -> combinesmall 3 (UGlobal.hash l) end @@ -200,7 +200,10 @@ module Level = struct | SProp -> "SProp" | Prop -> "Prop" | Set -> "Set" - | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n + | Level (d,s,n) -> + Names.DirPath.to_string d ^ + (if CString.is_empty s then "" else "." ^ s) ^ + "." ^ string_of_int n | Var n -> "Var(" ^ string_of_int n ^ ")" let pr u = str (to_string u) @@ -218,7 +221,7 @@ module Level = struct let name u = match data u with - | Level (d, n) -> Some (d, n) + | Level l -> Some l | _ -> None end diff --git a/kernel/univ.mli b/kernel/univ.mli index 7286fc84cb..eeaa1ad62d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -15,8 +15,8 @@ sig module UGlobal : sig type t - val make : Names.DirPath.t -> int -> t - val repr : t -> Names.DirPath.t * int + val make : Names.DirPath.t -> string -> int -> t + val repr : t -> Names.DirPath.t * string * int val equal : t -> t -> bool val hash : t -> int val compare : t -> t -> int diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml deleted file mode 100644 index 9ea751eef9..0000000000 --- a/lib/remoteCounter.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type 'a getter = unit -> 'a -type 'a installer = ('a getter) -> unit - -type remote_counters_status = (string * Obj.t) list - -let counters : remote_counters_status ref = ref [] - -let (!!) x = !(!x) - -let new_counter ~name a ~incr ~build = - assert(not (List.mem_assoc name !counters)); - let data = ref (ref a) in - counters := (name, Obj.repr data) :: !counters; - let m = Mutex.create () in - let mk_thsafe_local_getter f () = - (* - slaves must use a remote counter getter, not this one! *) - (* - in the main process there is a race condition between slave - managers (that are threads) and the main thread, hence the mutex *) - if Flags.async_proofs_is_worker () then - CErrors.anomaly(Pp.str"Slave processes must install remote counters."); - let x = CThread.with_lock m ~scope:f in - build x in - let mk_thsafe_remote_getter f () = - CThread.with_lock m ~scope:f in - let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in - let installer f = - if not (Flags.async_proofs_is_worker ()) then - CErrors.anomaly(Pp.str"Only slave processes can install a remote counter."); - getter := mk_thsafe_remote_getter f in - (fun () -> !getter ()), installer - -let backup () = !counters - -let snapshot () = - List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters - -let restore l = - List.iter (fun (name, data) -> - assert(List.mem_assoc name !counters); - let dataref = Obj.obj (List.assoc name !counters) in - !dataref := !!(Obj.obj data)) - l diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli deleted file mode 100644 index 42d1f8a8d1..0000000000 --- a/lib/remoteCounter.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Remote counters are *global* counters for fresh ids. In the master/slave - * scenario, the slave installs a getter that asks the master for a fresh - * value. In the scenario of a slave that runs after the death of the master - * on some marshalled data, a backup of all counters status should be taken and - * restored to avoid reusing ids. - * Counters cannot be created by threads, they must be created once and forall - * as toplevel module declarations. *) - - -type 'a getter = unit -> 'a -type 'a installer = ('a getter) -> unit - -val new_counter : name:string -> - 'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer - -type remote_counters_status -val backup : unit -> remote_counters_status -(* like backup but makes a copy so that further increment does not alter - * the snapshot *) -val snapshot : unit -> remote_counters_status -val restore : remote_counters_status -> unit diff --git a/man/coqdep.1 b/man/coqdep.1 index bb6b20c0bb..5ca558b7c5 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -70,6 +70,21 @@ Output dependencies for .vos files (this is not the default as it breaks dune's .B \-boot For coq developers, prints dependencies over coq library files (omitted by default). +.TP +.B \-noinit +Currently no effect. + + +.SH EXIT STATUS +.IP "1" +A file given on the command line cannot be found or some file +cannot be opened. +.IP "0" +In all other cases. In particular, when a dependency cannot be +found or an invalid option is encountered, +.B coqdep +prints a warning and exits with status +.B 0\fR. .SH SEE ALSO diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 53aa619d10..1018271751 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -449,6 +449,8 @@ let bound_monomials (sys : WithProof.t list) = in List.map snd (List.filter has_mon bounds) @ snd l +let bound_monomials = tr_sys "bound_monomials" bound_monomials + let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); max_nb_cstr := compute_max_nb_cstr sys prfdepth; @@ -1181,10 +1183,12 @@ let nlia enum prfdepth sys = It would only be safe if the variable is linear... *) let sys1 = - elim_simple_linear_equality (WithProof.subst_constant true sys) + normalise + (elim_simple_linear_equality (WithProof.subst_constant true sys)) in + let bnd1 = bound_monomials sys1 in let sys2 = saturate_by_linear_equalities sys1 in - let sys3 = nlinear_preprocess (sys1 @ sys2) in + let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in let sys4 = make_cstr_system (*sys2@*) sys3 in (* [reduction_equations] is too brutal - there should be some non-linear reasoning *) xlia (List.map fst sys) enum reduction_equations sys4 diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index cc75c63e16..3ea7408067 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -60,6 +60,7 @@ let op_iff_morph = lazy (zify "iff_morph") let op_not = lazy (zify "not") let op_not_morph = lazy (zify "not_morph") let op_True = lazy (zify "True") +let op_I = lazy (zify "I") (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map. This is useful for calling Constr.hash *) @@ -1553,41 +1554,51 @@ let spec_of_hyps = let iter_specs = spec_of_hyps let find_hyp evd t l = - try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)) + try + Some + (EConstr.mkVar + (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))) with Not_found -> None -let sat_constr c d = - Proofview.Goal.enter (fun gl -> - let evd = Tacmach.New.project gl in - let env = Tacmach.New.pf_env gl in - let hyps = Tacmach.New.pf_hyps_types gl in - match EConstr.kind evd c with - | App (c, args) -> - if Array.length args = 2 then - let h1 = - Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) - in - let h2 = - Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) - in - match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with - | Some h1, Some h2 -> - let n = - Tactics.fresh_id_in_env Id.Set.empty - (Names.Id.of_string "__sat") - env - in - let trm = - EConstr.mkApp - ( d.ESatT.satOK - , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] ) - in - Tactics.pose_proof (Names.Name n) trm - | _, _ -> Tacticals.New.tclIDTAC - else Tacticals.New.tclIDTAC - | _ -> Tacticals.New.tclIDTAC) +let find_proof evd t l = + if EConstr.eq_constr evd t (Lazy.force op_True) then Some (Lazy.force op_I) + else find_hyp evd t l + +(** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where + - sub' is a fresh subscript obtained from sub + - taclist' is obtained from taclist by posing the lemma 'd' applied to 'c' + - hyps' is obtained from hyps' + taclist and hyps are threaded to avoid adding duplicates + *) +let sat_constr env evd (sub,taclist, hyps) c d = + match EConstr.kind evd c with + | App (c, args) -> + if Array.length args = 2 then + let h1 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) + in + let h2 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) + in + let n = Nameops.add_subscript (Names.Id.of_string "__sat") sub in + let trm = + match (find_proof evd h1 hyps, find_proof evd h2 hyps) with + | Some h1, Some h2 -> + (EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1; h2|])) + | Some h1, _ -> + EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1|]) + | _, _ -> EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1)|]) + in + let rtrm = Tacred.cbv_beta env evd trm in + let typ = Retyping.get_type_of env evd rtrm in + match find_hyp evd typ hyps with + | None -> (Nameops.Subscript.succ sub, (Tactics.pose_proof (Names.Name n) rtrm :: taclist) , (n,typ)::hyps) + | Some _ -> (sub, taclist, hyps) + else (sub,taclist,hyps) + | _ -> (sub,taclist,hyps) + let get_all_sat env evd c = List.fold_left @@ -1611,8 +1622,10 @@ let saturate = Array.iter sat args; if Array.length args = 2 then let ds = get_all_sat env evd c in - if ds = [] then () - else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds + if ds = [] || CstrTable.HConstr.mem table t + then () + else List.iter (fun x -> + CstrTable.HConstr.add table t x.deriv) ds else () | Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous -> sat t1; sat t2 @@ -1621,5 +1634,6 @@ let saturate = (* Collect all the potential saturation lemma *) sat concl; List.iter (fun (_, t) -> sat t) hyps; - Tacticals.New.tclTHENLIST - (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table [])) + let s0 = fresh_subscript env in + let (_,tacs,_) = CstrTable.HConstr.fold (fun c d acc -> sat_constr env evd acc c d) table (s0,[],hyps) in + Tacticals.New.tclTHENLIST tacs) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index dd80ff21aa..a9f203014f 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -56,12 +56,8 @@ module Make(T : Task) () = struct type response = | Response of T.response | RespFeedback of Feedback.feedback - | RespGetCounterNewUnivLevel type request = Request of T.request - type more_data = - | MoreDataUnivLevel of UnivGen.univ_unique_id list - let slave_respond (Request r) = let res = T.perform r in Response res @@ -94,16 +90,6 @@ module Make(T : Task) () = struct with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("unmarshal_response: "^s) - let marshal_more_data oc (res : more_data) = - try marshal_to_channel oc res - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("marshal_more_data: "^s) - - let unmarshal_more_data ic = - try (CThread.thread_friendly_input_value ic : more_data) - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("unmarshal_more_data: "^s) - let report_status ?(id = !Flags.async_proofs_worker_id) s = let open Feedback in feedback ~id:Stateid.initial (WorkerStatus(id, s)) @@ -198,8 +184,6 @@ module Make(T : Task) () = struct | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in - let more_univs n = - CList.init n (fun _ -> UnivGen.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -231,9 +215,6 @@ module Make(T : Task) () = struct marshal_request oc (Request req); let rec continue () = match unmarshal_response ic with - | RespGetCounterNewUnivLevel -> - marshal_more_data oc (MoreDataUnivLevel (more_univs 10)); - continue () | RespFeedback fbk -> T.forward_feedback fbk; continue () | Response resp -> match T.use_response !worker_age task resp with @@ -315,13 +296,6 @@ module Make(T : Task) () = struct let ic, oc = Spawned.get_channels () in slave_oc := Some oc; slave_ic := Some ic - let bufferize f = - let l = ref [] in - fun () -> - match !l with - | [] -> let data = f () in l := List.tl data; List.hd data - | x::tl -> l := tl; x - let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) @@ -339,11 +313,6 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc) () in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); - (* We ask master to allocate universe identifiers *) - UnivGen.set_remote_new_univ_id (bufferize @@ Control.protect_sigalrm (fun () -> - marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; - match unmarshal_more_data (Option.get !slave_ic) with - | MoreDataUnivLevel l -> l)); let working = ref false in slave_handshake (); while true do diff --git a/stm/stm.ml b/stm/stm.ml index f5768726c3..6287943cee 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2447,24 +2447,21 @@ let join ~doc = VCS.print (); doc -let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot () - -type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status -let check_task name (tasks,rcbackup) i = - RemoteCounter.restore rcbackup; +type tasks = int Slaves.tasks +let check_task name tasks i = let vcs = VCS.backup () in try let rc = State.purify (Slaves.check_task name tasks) i in VCS.restore vcs; rc with e when CErrors.noncritical e -> VCS.restore vcs; false -let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u p (t,rcbackup as tasks) = - RemoteCounter.restore rcbackup; +let info_tasks = Slaves.info_tasks + +let finish_tasks name u p tasks = let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u p t) i in + let u = State.purify (Slaves.finish_task name u p tasks) i in VCS.restore vcs; u in try @@ -2515,13 +2512,13 @@ let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, below, [snapshot] gets computed even if [create_vos] is true. *) - let (tasks,counters) = dump_snapshot() in + let tasks = Slaves.dump_snapshot() in let except = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in let todo_proofs = if create_vos then Library.ProofsTodoSomeEmpty except - else Library.ProofsTodoSome (except,tasks,counters) + else Library.ProofsTodoSome (except,tasks) in Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); doc diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5338e0eef5..783a317b3a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -293,31 +293,34 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if Coqlib.check_ind_ref "core.eq.type" ind then - Some (build_coq_eq_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if Coqlib.check_ind_ref "core.identity.type" ind then - Some (build_coq_identity_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if Coqlib.check_ind_ref "core.JMeq.type" ind then - Some (build_coq_jmeq_data()),hdapp, - HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else - let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let nconstr = Array.length mip.mind_consnames in - if Int.equal nconstr 1 then - let (ctx, cty) = constr_types.(0) in - let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - if is_matching env sigma coq_refl_leibniz1_pattern cty then - None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching env sigma coq_refl_leibniz2_pattern cty then - None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching env sigma coq_refl_jm_pattern cty then - None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else raise NoEquationFound - else raise NoEquationFound - | _ -> raise NoEquationFound + (try + if Coqlib.check_ind_ref "core.eq.type" ind then + Some (build_coq_eq_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.identity.type" ind then + Some (build_coq_identity_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.JMeq.type" ind then + Some (build_coq_jmeq_data()),hdapp, + HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else + let (mib,mip) = Global.lookup_inductive ind in + let constr_types = mip.mind_nf_lc in + let nconstr = Array.length mip.mind_consnames in + if Int.equal nconstr 1 then + let (ctx, cty) = constr_types.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + if is_matching env sigma coq_refl_leibniz1_pattern cty then + None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) + else if is_matching env sigma coq_refl_leibniz2_pattern cty then + None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if is_matching env sigma coq_refl_jm_pattern cty then + None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else raise NoEquationFound + else raise NoEquationFound + with UserError _ -> + raise NoEquationFound) + | _ -> raise NoEquationFound (* Note: An "equality type" is any type with a single argument-free constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also diff --git a/test-suite/bugs/closed/bug_12806.v b/test-suite/bugs/closed/bug_12806.v new file mode 100644 index 0000000000..ee221d33a6 --- /dev/null +++ b/test-suite/bugs/closed/bug_12806.v @@ -0,0 +1,9 @@ +Require Import Ltac2.Ltac2. + +Declare Scope my_scope. +Delimit Scope my_scope with my_scope. + +Notation "###" := tt : my_scope. + +Ltac2 Notation "bar" c(open_constr(my_scope)) := c. +Ltac2 Eval bar ###. diff --git a/test-suite/micromega/bug_11656.v b/test-suite/micromega/bug_11656.v new file mode 100644 index 0000000000..19846ad50a --- /dev/null +++ b/test-suite/micromega/bug_11656.v @@ -0,0 +1,11 @@ +Require Import Lia. +Require Import NArith. +Open Scope N_scope. + +Goal forall (a b c: N), + a <> 0 -> + c <> 0 -> + a * ((b + 1) * c) <> 0. +Proof. + intros. nia. +Qed. diff --git a/test-suite/micromega/bug_12184.v b/test-suite/micromega/bug_12184.v new file mode 100644 index 0000000000..d329a3fa7f --- /dev/null +++ b/test-suite/micromega/bug_12184.v @@ -0,0 +1,8 @@ +Require Import Lia. +Require Import ZArith. + +Goal forall p : positive, (0 < Z.pos (2^p)%positive)%Z. +Proof. + intros p. + lia. +Qed. diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index d70bb809c6..d22e2b7c8c 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -12,6 +12,12 @@ Open Scope Z_scope. Require Import ZMicromega. Require Import VarMap. +Lemma power_pos : forall x y, 0 <= x \/ False -> x^ y >= 0. +Proof. + intros. + lia. +Qed. + Lemma not_so_easy : forall x n : Z, 2*x + 1 <= 2 *n -> x <= n-1. Proof. diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v index 485c24f0c9..e79b76b810 100644 --- a/test-suite/micromega/example_nia.v +++ b/test-suite/micromega/example_nia.v @@ -7,10 +7,16 @@ (************************************************************************) Require Import ZArith. -Require Import Psatz. Open Scope Z_scope. -Require Import ZMicromega. +Require Import ZMicromega Lia. Require Import VarMap. +Unset Nia Cache. + +Goal forall (x y: Z), 0 < (1+y^2)^(x^2). +Proof. nia. Qed. + +Goal forall (x y: Z), 0 <= (y^2)^x. +Proof. nia. Qed. (* false in Q : x=1/2 and n=1 *) @@ -347,8 +353,8 @@ Lemma hol_light17 : forall x y, -> x * y * (x + y) <= x ^ 2 + y ^ 2. Proof. intros. - Fail nia. -Abort. + nia. +Qed. Lemma hol_light18 : forall x y, @@ -507,3 +513,24 @@ Proof. intros. lia. Qed. + +Lemma mult : forall x x0 x1 x2 n n0 n1 n2, + 0 <= x -> 0 <= x0 -> 0 <= x1 -> 0 <= x2 -> + 0 <= n -> 0 <= n0 -> 0 <= n1 -> 0 <= n2 -> + (n1 * x <= n2 * x1) -> + (n * x0 <= n0 * x2) -> + (n1 * n * (x * x0) > n2 * n0 * (x1 * x2)) -> False. +Proof. + intros. + nia. +Qed. + + +Lemma mult_nat : forall x x0 x1 x2 n n0 n1 n2, + (n1 * x <= n2 * x1)%nat -> + (n * x0 <= n0 * x2)%nat -> + (n1 * n * (x * x0) > n2 * n0 * (x1 * x2))%nat -> False. +Proof. + intros. + nia. +Qed. diff --git a/test-suite/misc/vio_checking.sh b/test-suite/misc/vio_checking.sh new file mode 100755 index 0000000000..ffa909e93b --- /dev/null +++ b/test-suite/misc/vio_checking.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +set -ex + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc + +rm -f vio_checking{,bad}.{vo,vio} + +coqc -vio vio_checking.v +coqc -vio vio_checking_bad.v + +coqc -schedule-vio-checking 2 vio_checking.vio + +if coqc -schedule-vio-checking 2 vio_checking_bad.vio; then + echo 'vio-checking on vio_checking_bad.vio should have failed!' + exit 1 +fi +if coqc -schedule-vio-checking 2 vio_checking.vio vio_checking_bad.vio; then + echo 'vio-checking on vio_checking vio_checking_bad.vio should have failed!' + exit 1 +fi + +coqc -vio2vo vio_checking.vio +coqchk -silent vio_checking.vo + +if coqc -vio2vo vio_checking_bad.vio; then + echo 'vio2vo on vio_checking_bad.vio should have failed!' + exit 1 +fi diff --git a/test-suite/misc/vio_checking.v b/test-suite/misc/vio_checking.v new file mode 100644 index 0000000000..8dd5e47383 --- /dev/null +++ b/test-suite/misc/vio_checking.v @@ -0,0 +1,9 @@ + +Lemma foo : Type. +Proof. exact Type. Qed. + +Lemma foo1 : Type. +Proof. exact Type. Qed. + +Lemma foo2 : Type. +Proof. exact foo1. Qed. diff --git a/test-suite/misc/vio_checking_bad.v b/test-suite/misc/vio_checking_bad.v new file mode 100644 index 0000000000..f32d06f34a --- /dev/null +++ b/test-suite/misc/vio_checking_bad.v @@ -0,0 +1,4 @@ +(* a file to check that vio-checking is not a noop *) + +Lemma foo : Type. +Proof. match goal with |- ?G => exact G end. Qed. diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index bbdf9762a3..a530c34297 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,4 +1,3 @@ - Require Import Lia ZArith. (* Submitted by Xavier Urbain 18 Jan 2002 *) diff --git a/test-suite/success/RemoteUnivs.v b/test-suite/success/RemoteUnivs.v new file mode 100644 index 0000000000..5ab4937dda --- /dev/null +++ b/test-suite/success/RemoteUnivs.v @@ -0,0 +1,31 @@ + + +Goal Type * Type. +Proof. + split. + par: exact Type. +Qed. + +Goal Type. +Proof. + exact Type. +Qed. + +(* (* coqide test, note the delegated proofs seem to get an empty dirpath? + or I got confused because I had lemma foo in file foo + *) +Definition U := Type. + +Lemma foo : U. +Proof. + exact Type. +Qed. + + +Lemma foo1 : Type. +Proof. + exact (U:Type). +Qed. + +Print foo. +*) diff --git a/test-suite/vio/univ_constraints_statements_body.v b/test-suite/vio/univ_constraints_statements_body.v new file mode 100644 index 0000000000..6302adefc2 --- /dev/null +++ b/test-suite/vio/univ_constraints_statements_body.v @@ -0,0 +1,7 @@ +Definition T := Type. +Definition T1 : T := Type. + +Lemma x : True. +Proof. +exact (let a : T := Type in I). +Qed. diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 2a26b6b12a..4bf971668d 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -218,7 +218,6 @@ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with y;auto with zarith. rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. - assert (0 < 2^p);auto with zarith. replace (2^p) with 0. destruct x;change (0<y);auto with zarith. destruct p;trivial;discriminate. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index a3ebe67325..d3fac82d09 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1428,7 +1428,7 @@ Proof. assert (Hp3: (0 < Φ (WW ih il))). {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } + } cbv zeta. case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. @@ -1465,7 +1465,6 @@ Proof. apply Hrec; rewrite H; clear u H. assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith). case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2. - 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith. split. replace (φ j + Φ (WW ih il) / φ j)%Z with (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia. diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 01cc9ad810..3a50001b1f 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -33,5 +33,6 @@ Ltac zify := intros; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; - zify_to_euclidean_division_equations ; zify_post_hook. + zify_to_euclidean_division_equations ; + zify_post_hook; + zify_saturate. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index e86d799541..25d9fa9104 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -281,3 +281,4 @@ Register impl_morph as ZifyClasses.impl_morph. Register not as ZifyClasses.not. Register not_morph as ZifyClasses.not_morph. Register True as ZifyClasses.True. +Register I as ZifyClasses.I. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index dd31b998d4..8dee70be45 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -480,39 +480,20 @@ Add Zify UnOpSpec ZabsSpec. (** Saturate positivity constraints *) -Instance SatProd : Saturate Z.mul := - {| - PArg1 := fun x => 0 <= x; - PArg2 := fun y => 0 <= y; - PRes := fun r => 0 <= r; - SatOk := Z.mul_nonneg_nonneg - |}. -Add Zify Saturate SatProd. - -Instance SatProdPos : Saturate Z.mul := +Instance SatPowPos : Saturate Z.pow := {| PArg1 := fun x => 0 < x; - PArg2 := fun y => 0 < y; + PArg2 := fun y => 0 <= y; PRes := fun r => 0 < r; - SatOk := Z.mul_pos_pos + SatOk := Z.pow_pos_nonneg |}. -Add Zify Saturate SatProdPos. - -Lemma pow_pos_strict : - forall a b, - 0 < a -> 0 < b -> 0 < a ^ b. -Proof. - intros. - apply Z.pow_pos_nonneg; auto. - apply Z.lt_le_incl;auto. -Qed. - +Add Zify Saturate SatPowPos. -Instance SatPowPos : Saturate Z.pow := +Instance SatPowNonneg : Saturate Z.pow := {| - PArg1 := fun x => 0 < x; - PArg2 := fun y => 0 < y; - PRes := fun r => 0 < r; - SatOk := pow_pos_strict + PArg1 := fun x => 0 <= x; + PArg2 := fun y => True; + PRes := fun r => 0 <= r; + SatOk := fun a b Ha _ => @Z.pow_nonneg a b Ha |}. -Add Zify Saturate SatPowPos. +Add Zify Saturate SatPowNonneg. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index f1dbac889b..199fc4225d 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -34,7 +34,8 @@ let usage () = eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; - eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; + eprintf " -noinit : currently no effect\n"; + eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; @@ -64,6 +65,7 @@ let rec parse = function | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-noinit" :: ll -> (* do nothing *) parse ll | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () @@ -80,6 +82,8 @@ let rec parse = function | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () + | opt :: ll when String.length opt > 0 && opt.[0] = '-' -> + coqdep_warning "unknown option %s" opt; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index dca9291da3..a6634586f3 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -157,6 +157,18 @@ let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 +let error_cannot_stat s unix_error = + (* Print an arbitrary line number, such that the message matches + common error message pattern. *) + Printf.eprintf "File \"%s\", line 1: %s\n" s (error_message unix_error); + exit 1 + +let error_cannot_open s msg = + (* Print an arbitrary line number, such that the message matches + common error message pattern. *) + Printf.eprintf "File \"%s\", line 1: %s\n" s msg; + exit 1 + let warning_module_notfound f s = coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!" f (String.concat "." s) @@ -368,7 +380,7 @@ let rec find_dependencies basename = | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j) - with Sys_error _ -> [] (* TODO: report an error? *) + with Sys_error msg -> error_cannot_open (basename ^ ".v") msg let write_vos = ref false @@ -472,7 +484,12 @@ let rec treat_file old_dirname old_name = | (Some d1,d2) -> Some (d1//d2) in let complete_name = file_name name dirname in - match try (stat complete_name).st_kind with _ -> S_BLK with + let stat_res = + try stat complete_name + with Unix_error(error, _, _) -> error_cannot_stat complete_name error + in + match stat_res.st_kind + with | S_DIR -> (if name.[0] <> '.' then let newdirname = diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 041097d2d3..df6f04792e 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -194,7 +194,7 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = if mode = BuildVio then dump_empty_vos() | Vio2Vo -> - + Flags.async_proofs_worker_id := "Vio2Vo"; let sum, lib, univs, tasks, proofs = Library.load_library_todo long_f_dot_in in let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in @@ -223,6 +223,7 @@ let compile_file opts stm_opts copts injections = (* VIO Dispatching *) (******************************************************************************) let check_vio_tasks copts = + Flags.async_proofs_worker_id := "VioChecking"; let rc = List.fold_left (fun acc (n,f) -> let f_in = ensure ".vio" f f in diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 457b8e1acf..4758ecf5bd 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1754,6 +1754,16 @@ let () = add_scope "constr" (fun arg -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) ) +let () = add_scope "open_constr" (fun arg -> + let delimiters = List.map (function + | SexprRec (_, { v = Some s }, []) -> s + | _ -> scope_fail "open_constr" arg) + arg + in + let act e = Tac2quote.of_open_constr ~delimiters e in + Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) + ) + let add_expr_scope name entry f = add_scope name begin function | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f) @@ -1782,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_ let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format -let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern (** seq scope, a bit hairy *) diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index d1a72fcfd1..2d65f9ec3e 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -102,18 +102,22 @@ let of_anti f = function let of_ident {loc;v=id} = inj_wit ?loc wit_ident id +let quote_constr ?delimiters c = + let loc = Constrexpr_ops.constr_loc c in + Option.cata + (List.fold_left (fun c d -> + CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c)) + c) + c delimiters + let of_constr ?delimiters c = let loc = Constrexpr_ops.constr_loc c in - let c = Option.cata - (List.fold_left (fun c d -> - CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c)) - c) - c delimiters - in + let c = quote_constr ?delimiters c in inj_wit ?loc wit_constr c -let of_open_constr c = +let of_open_constr ?delimiters c = let loc = Constrexpr_ops.constr_loc c in + let c = quote_constr ?delimiters c in inj_wit ?loc wit_open_constr c let of_bool ?loc b = diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli index fcd1339cd7..6e2f548319 100644 --- a/user-contrib/Ltac2/tac2quote.mli +++ b/user-contrib/Ltac2/tac2quote.mli @@ -36,7 +36,7 @@ val of_ident : Id.t CAst.t -> raw_tacexpr val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr -val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr +val of_open_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr val of_list : ?loc:Loc.t -> ('a -> raw_tacexpr) -> 'a list -> raw_tacexpr diff --git a/vernac/library.ml b/vernac/library.ml index cc9e3c3c44..eedf8aa670 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -448,10 +448,10 @@ let save_library_base f sum lib univs tasks proofs = Sys.remove f; Exninfo.iraise reraise -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) let save_library_to todo_proofs ~output_native_objects dir f otab = assert( @@ -464,7 +464,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let except = match todo_proofs with | ProofsTodoNone -> Future.UUIDSet.empty | ProofsTodoSomeEmpty except -> except - | ProofsTodoSome (except,l,_) -> except + | ProofsTodoSome (except,l) -> except in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, f2t_map = Opaqueproof.dump ~except otab in @@ -473,13 +473,13 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = | ProofsTodoNone -> None, None | ProofsTodoSomeEmpty _except -> None, Some (Univ.ContextSet.empty,false) - | ProofsTodoSome (_except, tasks, rcbackup) -> + | ProofsTodoSome (_except, tasks) -> let tasks = List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b with Not_found -> assert b; { r with uuid = -1 }, b) tasks in - Some (tasks,rcbackup), + Some tasks, Some (Univ.ContextSet.empty,false) in let sd = { diff --git a/vernac/library.mli b/vernac/library.mli index d0e9f84691..4c6c654c58 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -41,13 +41,13 @@ type seg_proofs = Opaqueproof.opaque_proofterm array argument. [output_native_objects]: when producing vo objects, also compile the native-code version. *) -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) val save_library_to : - ('document,'counters) todo_proofs -> + 'document todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit diff --git a/vernac/record.ml b/vernac/record.ml index fccc3e4fbd..53f3508806 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -766,11 +766,9 @@ let add_inductive_class env sigma ind = let k = let ctx = oneind.mind_arity_ctxt in let univs = Declareops.inductive_polymorphic_context mind in - let env = push_context ~strict:false (Univ.AUContext.repr univs) env in - let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in let ty = Inductive.type_of_inductive ((mind, oneind), inst) in - let r = Inductive.relevance_of_inductive env ind in + let r = oneind.mind_relevance in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; cl_context = ctx; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index af40292f18..54f034c74e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -413,7 +413,7 @@ let sort_universes g = let levels = traverse LMap.empty [normalize Level.set, 0] in let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in + let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in let ulevels = Array.cons Level.set ulevels in (* Add the normal universes *) let fold (cur, ans) u = |