diff options
| -rw-r--r-- | .circleci/config.yml | 40 | ||||
| -rw-r--r-- | .github/CODEOWNERS | 13 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | Makefile.doc | 6 | ||||
| -rw-r--r-- | README.md | 1 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh | 6 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 5 | ||||
| -rwxr-xr-x | dev/tools/check-owners-pr.sh | 32 | ||||
| -rwxr-xr-x | dev/tools/check-owners.sh | 138 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 92 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 10 | ||||
| -rw-r--r-- | engine/evd.ml | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/universes.ml | 34 | ||||
| -rw-r--r-- | engine/universes.mli | 9 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 1 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 2 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 4 | ||||
| -rw-r--r-- | pretyping/constr_matching.mli | 2 |
20 files changed, 287 insertions, 121 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 14c102cede..79f83d4720 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -160,22 +160,22 @@ workflows: requires: - build - bignums - - compcert: *req-main - - coq-dpdgraph: *req-main - - coquelicot: *req-main - - cross-crypto: *req-main - - elpi: *req-main - - equations: *req-main - - geocoq: *req-main - - fcsl-pcm: *req-main - - fiat-crypto: *req-main - - fiat-parsers: *req-main - - flocq: *req-main + # - compcert: *req-main + # - coq-dpdgraph: *req-main + # - coquelicot: *req-main + # - cross-crypto: *req-main + # - elpi: *req-main + # - equations: *req-main + # - geocoq: *req-main + # - fcsl-pcm: *req-main + # - fiat-crypto: *req-main + # - fiat-parsers: *req-main + # - flocq: *req-main - math-classes: requires: - build - bignums - - mtac2: *req-main + # - mtac2: *req-main - corn: requires: - build @@ -184,11 +184,11 @@ workflows: requires: - build - corn - - hott: *req-main - - iris-lambda-rust: *req-main - - ltac2: *req-main - - math-comp: *req-main - - pidetop: *req-main - - sf: *req-main - - unimath: *req-main - - vst: *req-main + # - hott: *req-main + # - iris-lambda-rust: *req-main + # - ltac2: *req-main + # - math-comp: *req-main + # - pidetop: *req-main + # - sf: *req-main + # - unimath: *req-main + # - vst: *req-main diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index ab9725c967..2ca8274929 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -8,9 +8,13 @@ ########## CI infrastructure ########## -/dev/ci/*.sh @ejgallego +/dev/ci/ @ejgallego # Secondary maintainer @SkySkimmer +/dev/ci/user-overlays/*.sh @ghost +# Trick to avoid getting review requests +# each time someone adds an overlay + /.circleci/ @SkySkimmer # Secondary maintainer @ejgallego @@ -20,7 +24,9 @@ /.gitlab-ci.yml @SkySkimmer # Secondary maintainer @ejgallego -/appveyor.yml @maximedenes +/appveyor.yml @maximedenes +/dev/ci/appveyor.* @maximedenes +/dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer /default.nix @Zimmi48 @@ -338,3 +344,6 @@ /dev/tools/pre-commit @SkySkimmer /dev/tools/sudo-apt-get-update @JasonGross + +/dev/tools/check-owners*.sh @SkySkimmer +# Secondary maintainer @maximedenes diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3d4cee8fbc..c010da4cfc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -94,7 +94,7 @@ before_script: - set +e variables: &warnings-variables - COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -217,6 +217,7 @@ warnings:base: warnings:edge: <<: *warnings-template variables: + <<: *warnings-variables OPAM_SWITCH: edge test-suite:base: diff --git a/Makefile.doc b/Makefile.doc index d13d0c09e3..41ae11b869 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -49,7 +49,11 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex doc: sphinx stdlib -sphinx: coq +ifndef QUICK +SPHINX_DEPS := coq +endif + +sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html @echo @@ -1,5 +1,6 @@ # Coq +[](https://gitlab.com/coq/coq/commits/master) [](https://travis-ci.org/coq/coq/builds) [](https://ci.appveyor.com/project/coq/coq/branch/master) [](https://circleci.com/gh/coq/workflows/coq/tree/master) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 189734a0bc..2a14ed352a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ]; then export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi else if [ -n "${TRAVIS}" ]; then diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 0000000000..517088a247 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 84ff94c66a..a466124c1c 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -109,9 +109,8 @@ There are two cases to consider: The merge script passes option `-S` to `git merge` to ensure merge commits are signed. Consequently, it depends on the GnuPG command utility being -installed and a GPG key being available. Here is a short tutorial to -creating your own GPG key: -<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. The script depends on a few other utilities. If you are a Nix user, the simplest way of getting them is to run `nix-shell` first. diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh new file mode 100755 index 0000000000..d2910279b5 --- /dev/null +++ b/dev/tools/check-owners-pr.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env sh + +usage() { + { echo "usage: $0 PR [ARGS]..." + echo "A wrapper around check-owners.sh to check owners for a PR." + echo "Assumes upstream is the canonical Coq repository." + echo "Assumes the PR is against master." + echo + echo " PR: PR number" + echo " ARGS: passed through to check-owners.sh" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi;; + "") + usage + exit 1;; +esac + +PR="$1" +shift + +# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first +git fetch upstream "+refs/pull/$PR/head" master + +head=$(git rev-parse FETCH_HEAD) +base=$(git merge-base upstream/master "$head") + +git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@" diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh new file mode 100755 index 0000000000..1a97508abb --- /dev/null +++ b/dev/tools/check-owners.sh @@ -0,0 +1,138 @@ +#!/usr/bin/env bash + +# Determine CODEOWNERS of the files given in argument +# For a given commit range: +# git diff --name-only -z COMMIT1 COMMIT2 | xargs -0 dev/tools/check-owners.sh [opts] + +# NB: gitignore files will be messed up if you interrupt the script. +# You should be able to just move the .gitignore.bak files back manually. + +usage() { + { echo "usage: $0 [--show-patterns] [--owner OWNER] [FILE]..." + echo " --show-patterns: instead of printing file names print the matching patterns (more compact)" + echo " --owner: show only files/patterns owned by OWNER (use Nobody to see only non-owned files)" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi +esac + +if ! [ -e .github/CODEOWNERS ]; then + >&2 echo "No CODEOWNERS set up or calling from wrong directory." + exit 1 +fi + +files=() +show_patterns=false + +target_owner="" + +while [[ "$#" -gt 0 ]]; do + case "$1" in + "--show-patterns") + show_patterns=true + shift;; + "--owner") + if [[ "$#" = 1 ]]; then + >&2 echo "Missing argument to --owner" + usage + exit 1 + elif [[ "$target_owner" != "" ]]; then + >&2 echo "Only one --owner allowed" + usage + exit 1 + fi + target_owner="$2" + shift 2;; + *) + files+=("$@") + break;; + esac +done + +# CODEOWNERS uses .gitignore patterns so we want to use git to parse it +# The only available tool for that is git check-ignore +# However it provides no way to use alternate .gitignore files +# so we rename them temporarily + +find . -name .gitignore -print0 | while IFS= read -r -d '' f; do + if [ -e "$f.bak" ]; then + >&2 echo "$f.bak exists!" + exit 1 + else + mv "$f" "$f.bak" + fi +done + +# CODEOWNERS is not quite .gitignore patterns: +# after the pattern is the owner (space separated) +# git would interpret that as a big pattern containing spaces +# so we create a valid .gitignore by removing all but the first field + +while read -r pat _; do + printf '%s\n' "$pat" >> .gitignore +done < .github/CODEOWNERS + +# associative array [file => owner] +declare -A owners + +for f in "${files[@]}"; do + data=$(git check-ignore --verbose --no-index "./$f") + code=$? + + if [[ "$code" = 1 ]] || ! [[ "$data" =~ .gitignore:.* ]] ; then + # no match, or match from non tracked gitignore (eg global gitignore) + if [ "$target_owner" != "" ] && [ "$target_owner" != Nobody ] ; then + owner="" + else + owner="Nobody" + pat="$f" # no patterns for unowned files + fi + else + # data looks like [.gitignore:$line:$pattern $file] + # extract the line to look it up in CODEOWNERS + data=${data#'.gitignore:'} + line=${data%%:*} + + # NB: supports multiple owners + # Does not support secondary owners declared in comment + read -r pat fowners < <(sed "${line}q;d" .github/CODEOWNERS) + + owner="" + if [ "$target_owner" != "" ]; then + for o in $fowners; do # do not quote: multiple owners possible + if [ "$o" = "$target_owner" ]; then + owner="$o" + fi + done + else + owner="$fowners" + fi + fi + + if [ "$owner" != "" ]; then + if $show_patterns; then + owners[$pat]="$owner" + else + owners[$f]="$owner" + fi + fi +done + +for f in "${!owners[@]}"; do + printf '%s: %s\n' "$f" "${owners[$f]}" +done | sort -k 2 -k 1 # group by owner + +# restore gitignore files +rm .gitignore +find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do + base=${f%.bak} + if [ -e "$base" ]; then + >&2 echo "$base exists!" + else + mv "$f" "$base" + fi +done diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 39735a6eda..aa41f8058d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1245,37 +1245,37 @@ inhabitant of the type) is interactively built using tactics. The interactive proof mode is described in Chapter :ref:`proofhandling` and the tactics in Chapter :ref:`Tactics`. The basic assertion command is: -.. cmd:: Theorem @ident : @type +.. cmd:: Theorem @ident {? @binders } : @type -After the statement is asserted, Coq needs a proof. Once a proof of -:token:`type` under the assumptions represented by :token:`binders` is given and -validated, the proof is generalized into a proof of forall , :token:`type` and -the theorem is bound to the name :token:`ident` in the environment. + After the statement is asserted, Coq needs a proof. Once a proof of + :token:`type` under the assumptions represented by :token:`binders` is given and + validated, the proof is generalized into a proof of :n:`forall @binders, @type` and + the theorem is bound to the name :token:`ident` in the environment. -.. exn:: The term @term has type @type which should be Set, Prop or Type. + .. exn:: The term @term has type @type which should be Set, Prop or Type. -.. exn:: @ident already exists. - :name: @ident already exists. (Theorem) + .. exn:: @ident already exists. + :name: @ident already exists. (Theorem) - The name you provided is already defined. You have then to choose - another name. + The name you provided is already defined. You have then to choose + another name. -.. cmdv:: Lemma @ident : @type - :name: Lemma + The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: -.. cmdv:: Remark @ident : @type - :name: Remark + .. cmdv:: Lemma @ident {? @binders } : @type + :name: Lemma -.. cmdv:: Fact @ident : @type - :name: Fact + .. cmdv:: Remark @ident {? @binders } : @type + :name: Remark -.. cmdv:: Corollary @ident : @type - :name: Corollary + .. cmdv:: Fact @ident {? @binders } : @type + :name: Fact -.. cmdv:: Proposition @ident : @type - :name: Proposition + .. cmdv:: Corollary @ident {? @binders } : @type + :name: Corollary - These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`. + .. cmdv:: Proposition @ident {? @binders } : @type + :name: Proposition .. cmdv:: Theorem @ident : @type {* with @ident : @type} @@ -1302,13 +1302,13 @@ the theorem is bound to the name :token:`ident` in the environment. .. cmdv:: Definition @ident : @type This allows defining a term of type :token:`type` using the proof editing - mode. It behaves as Theorem but is intended to be used in conjunction with + mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with :cmd:`Defined` in order to define a constant of which the computational behavior is relevant. The command can be used also with :cmd:`Example` instead of :cmd:`Definition`. - See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. cmdv:: Let @ident : @type @@ -1328,21 +1328,14 @@ the theorem is bound to the name :token:`ident` in the environment. This generalizes the syntax of CoFixpoint so that one or more bodies can be defined interactively using the proof editing mode. -.. cmd:: Proof - - A proof starts by the keyword Proof. Then Coq enters the proof editing mode - until the proof is completed. The proof editing mode essentially contains - tactics that are described in chapter :ref:`Tactics`. Besides tactics, there - are commands to manage the proof editing mode. They are described in Chapter - :ref:`proofhandling`. - -.. cmd:: Qed - - When the proof is completed it should be validated and put in the environment - using the keyword Qed. +A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +until the proof is completed. The proof editing mode essentially contains +tactics that are described in chapter :ref:`Tactics`. Besides tactics, there +are commands to manage the proof editing mode. They are described in Chapter +:ref:`proofhandling`. -.. exn:: @ident already exists. - :name: @ident already exists. (Qed) +When the proof is completed it should be validated and put in the environment +using the keyword :cmd:`Qed`. .. note:: @@ -1351,28 +1344,19 @@ the theorem is bound to the name :token:`ident` in the environment. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the - statements still to be proved. - - #. Proof is recommended but can currently be omitted. On the opposite - side, Qed (or Defined, see below) is mandatory to validate a proof. + statements still to be proved. Nonetheless, this practice is discouraged + and may stop working in future versions. - #. Proofs ended by Qed are declared opaque. Their content cannot be + #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be unfolded (see :ref:`performingcomputations`), thus realizing some form of *proof-irrelevance*. To be able to unfold a - proof, the proof should be ended by Defined (see below). - -.. cmdv:: Defined - :name: Defined - - Same as :cmd:`Qed` but the proof is then declared transparent, which means - that its content can be explicitly used for type-checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). + proof, the proof should be ended by :cmd:`Defined`. -.. cmdv:: Admitted - :name: Admitted + #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite + side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. - Turns the current asserted statement into an axiom and exits the proof mode. + #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the + current asserted statement into an axiom and exit the proof editing mode. .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 069cf8a6dc..892ddbc165 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -60,7 +60,6 @@ list of assertion commands is given in :ref:`Assertions`. The command used for another statement). .. cmd:: Qed - :name: Qed (interactive proof) This command is available in interactive editing proof mode when the proof is completed. Then :cmd:`Qed` extracts a proof term from the proof @@ -82,9 +81,12 @@ list of assertion commands is given in :ref:`Assertions`. The command even incur a memory overflow. .. cmdv:: Defined - :name: Defined (interactive proof) + :name: Defined - Defines the proved term as a transparent constant. + Same as :cmd:`Qed` but the proof is then declared transparent, which means + that its content can be explicitly used for type-checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). .. cmdv:: Save @ident :name: Save @@ -94,7 +96,6 @@ list of assertion commands is given in :ref:`Assertions`. The command has been opened using the :cmd:`Goal` command. .. cmd:: Admitted - :name: Admitted (interactive proof) This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom. @@ -125,7 +126,6 @@ list of assertion commands is given in :ref:`Assertions`. The command proof term (see Section :ref:`applyingtheorems`). .. cmd:: Proof - :name: Proof (interactive proof) Is a no-op which is useful to delimit the sequence of tactic commands which start a proof, after a :cmd:`Theorem` command. It is a good practice to diff --git a/engine/evd.ml b/engine/evd.ml index af22de5cd4..20a7c80ea0 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -842,12 +842,12 @@ let universe_rigidity evd l = else UnivRigid let normalize_universe evd = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l diff --git a/engine/uState.ml b/engine/uState.ml index 6c8dbe3f44..df50bae86e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs = let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in - let normalize = normalize_univ_variable_opt_subst vars in + let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) diff --git a/engine/universes.ml b/engine/universes.ml index 938f5ad9cb..a13663cbad 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -605,31 +605,25 @@ let fresh_universe_context_set_instance ctx = let cst' = subst_univs_level_constraints subst cst in subst, (univs', cst') -let normalize_univ_variable ~find ~update = +let normalize_univ_variable ~find = let rec aux cur = let b = find cur in let b' = subst_univs_universe aux b in if Universe.equal b' b then b - else update cur b' + else b' in aux let normalize_univ_variable_opt_subst ectx = let find l = - match Univ.LMap.find l !ectx with + match Univ.LMap.find l ectx with | Some b -> b | None -> raise Not_found in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false - in normalize_univ_variable ~find ~update + normalize_univ_variable ~find let normalize_univ_variable_subst subst = - let find l = Univ.LMap.find l !subst in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in - normalize_univ_variable ~find ~update + let find l = Univ.LMap.find l subst in + normalize_univ_variable ~find let normalize_universe_opt_subst subst = let normlevel = normalize_univ_variable_opt_subst subst in @@ -640,13 +634,10 @@ let normalize_universe_subst subst = subst_univs_universe normlevel let normalize_opt_subst ctx = - let ectx = ref ctx in - let normalize = normalize_univ_variable_opt_subst ectx in - let () = - Univ.LMap.iter (fun u v -> - if Option.is_empty v then () - else try ignore(normalize u) with Not_found -> assert(false)) ctx - in !ectx + let normalize = normalize_universe_opt_subst ctx in + Univ.LMap.mapi (fun u -> function + | None -> None + | Some v -> Some (normalize v)) ctx type universe_opt_subst = Universe.t option universe_map @@ -655,7 +646,7 @@ let subst_univs_fn_puniverses f (c, u as cu) = if u' == u then cu else (c, u') let nf_evars_and_universes_opt_subst f subst = - let subst = normalize_univ_variable_opt_subst (ref subst) in + let subst = normalize_univ_variable_opt_subst subst in let lsubst = level_subst_of subst in let rec aux c = match kind c with @@ -975,7 +966,7 @@ let normalize_context_set g ctx us algs weak = (* Process weak constraints: when one side is flexible and the 2 universes are unrelated unify them. *) let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> - let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in let u = norm u and v = norm v in let set_to a b = (LSet.remove a ctx, @@ -994,7 +985,6 @@ let normalize_context_set g ctx us algs weak = (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = - let us = ref us in let norm = level_subst_of (normalize_univ_variable_opt_subst us) in Constraint.fold (fun (u,d,v) noneqs -> let u = norm u and v = norm v in diff --git a/engine/universes.mli b/engine/universes.mli index e6bee42bb3..df2e961d60 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -184,19 +184,18 @@ val normalize_univ_variables : universe_opt_subst -> val normalize_univ_variable : find:(Level.t -> Universe.t) -> - update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> +val normalize_univ_variable_opt_subst : universe_opt_subst -> (Level.t -> Universe.t) -val normalize_univ_variable_subst : universe_subst ref -> +val normalize_univ_variable_subst : universe_subst -> (Level.t -> Universe.t) -val normalize_universe_opt_subst : universe_opt_subst ref -> +val normalize_universe_opt_subst : universe_opt_subst -> (Universe.t -> Universe.t) -val normalize_universe_subst : universe_subst ref -> +val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) (** Create a fresh global in the global environment, without side effects. diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index c66d69c036..d8fdfdb1bd 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -352,7 +352,6 @@ let about () = { } let handle_exn (e, info) = - let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index b6462c8106..c949589e22 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) let id_map_try_add id x m = match id with - | Some id -> Id.Map.add id x m + | Some id -> Id.Map.add id (Lazy.force x) m | None -> m (** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a410..b4e1a1b102 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -427,7 +427,7 @@ let special_meta = (-1) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : constr; } + m_ctx : constr Lazy.t; } let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) @@ -451,7 +451,7 @@ let authorized_occ env sigma closed pat c mk_ctx = let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) - else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next) with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 3c2c73915f..d19789ef42 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : EConstr.t } + m_ctx : EConstr.t Lazy.t } (** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], |