aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.circleci/config.yml7
-rw-r--r--.gitlab-ci.yml41
-rw-r--r--.travis.yml7
-rw-r--r--INSTALL.doc8
-rw-r--r--Makefile.ci2
-rw-r--r--Makefile.doc17
-rw-r--r--configure.ml44
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-mtac2.sh (renamed from dev/ci/ci-metacoq.sh)6
-rw-r--r--dev/top_printers.ml4
-rw-r--r--engine/universes.ml257
-rw-r--r--engine/universes.mli2
-rw-r--r--kernel/cbytegen.ml4
-rw-r--r--kernel/cbytegen.mli3
-rw-r--r--kernel/clambda.ml4
-rw-r--r--kernel/clambda.mli3
-rw-r--r--kernel/uGraph.ml15
-rw-r--r--kernel/uGraph.mli5
-rw-r--r--kernel/univ.ml15
-rw-r--r--kernel/univ.mli2
-rw-r--r--lib/flags.ml9
-rw-r--r--lib/flags.mli32
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--test-suite/success/evars.v5
-rw-r--r--vernac/vernacentries.ml10
26 files changed, 250 insertions, 262 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8b6b43a552..f811f26e1d 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -54,7 +54,6 @@ opam-switch: &opam-switch
- restore_cache:
keys:
- coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
- - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}- # this grabs old cache if checksum doesn't match
- run:
name: Update opam lists
command: |
@@ -127,7 +126,7 @@ jobs:
<<: *opam-boot-template
environment:
<<: *envvars
- EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
+ EXTRA_OPAM: "ocamlgraph elpi"
# Build and prepare test environment
build: *build-template
@@ -207,6 +206,9 @@ jobs:
math-comp:
<<: *ci-template
+ mtac2:
+ <<: *ci-template
+
sf:
<<: *ci-template
environment:
@@ -251,6 +253,7 @@ workflows:
requires:
- build
- bignums
+ - mtac2: *req-main
- corn:
requires:
- build
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7d6b539644..6b42ac7eb1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,12 +1,15 @@
-image: ubuntu:latest
+image: ubuntu:bionic
stages:
- opam-boot
- build
- test
+# some default values
variables:
- # some default values
+ # Format: $IMAGE-V$DATE-$HOUR-$MINUTE
+ CACHEKEY: bionic-V2018-04-29-00-50
+ DEBIAN_FRONTEND: "noninteractive"
NJOBS: "2"
COMPILER: "4.02.3"
CAMLP5_VER: "6.14"
@@ -16,26 +19,26 @@ variables:
# some useful values
COMPILER_32BIT: "4.02.3+32bit"
- COMPILER_BLEEDING_EDGE: "4.06.0"
- CAMLP5_VER_BLEEDING_EDGE: "7.03"
+ COMPILER_BLEEDING_EDGE: "4.06.1"
+ CAMLP5_VER_BLEEDING_EDGE: "7.05"
- TIMING_PACKAGES: "time python"
+ TIMING_PACKAGES: "time python3"
COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev"
#COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
- COQIDE_OPAM: "lablgtk-extras"
- COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6"
- COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa python3-pip"
- COQDOC_OPAM: "hevea"
- SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex"
- ELPI_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
-
+ COQIDE_OPAM: "lablgtk.2.18.5 conf-gtksourceview.2"
+ COQIDE_OPAM_BE: "lablgtk.2.18.6 conf-gtksourceview.2"
+ COQDOC_PACKAGES: "texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip"
+ SPHINX_PACKAGES: "antlr4-python3-runtime"
+ ELPI_OPAM: "elpi"
before_script:
+ - cat /proc/{cpu,mem}info || true
- ls -a # figure out if artifacts are around
- printenv
# - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
- apt-get update -qq && apt-get install -y -qq m4 opam ${EXTRA_PACKAGES}
+ # This should be replaced by standard debian packages once python3-antlr4 makes to the archive.
- if [ -n "${PIP_PACKAGES}" ]; then pip3 install ${PIP_PACKAGES}; fi
# if no cache running opam config fails!
- if [ -d .opamcache ]; then eval $(opam config env); fi
@@ -57,9 +60,6 @@ before_script:
- .opamcache
expire_in: 1 week
script:
- # the default repo in this docker image is a local directory
- # at the time of 4aaeb8abf it lagged behind the official
- # repository such that camlp5 7.01 was not available
- opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org
- eval $(opam config env)
- opam update
@@ -178,16 +178,16 @@ opam-boot:
cache:
paths: &cache-paths
- .opamcache
- key: main
+ key: "main-$CACHEKEY"
variables:
- EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM ocamlgraph $ELPI_OPAM"
+ EXTRA_OPAM: "$COQIDE_OPAM ocamlgraph $ELPI_OPAM"
EXTRA_PACKAGES: "$COQIDE_PACKAGES"
opam-boot:32bit:
<<: *opam-boot-template
cache:
paths: *cache-paths
- key: 32bit
+ key: "32bit-$CACHEKEY"
variables:
COMPILER: "$COMPILER_32BIT"
EXTRA_PACKAGES: "gcc-multilib"
@@ -196,7 +196,7 @@ opam-boot:bleeding-edge:
<<: *opam-boot-template
cache:
paths: *cache-paths
- key: be
+ key: "be-$CACHEKEY"
variables:
COMPILER: "$COMPILER_BLEEDING_EDGE"
CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
@@ -360,6 +360,9 @@ ci-math-classes:
ci-math-comp:
<<: *ci-template
+ci-mtac2:
+ <<: *ci-template
+
ci-sf:
<<: *ci-template
variables:
diff --git a/.travis.yml b/.travis.yml
index fe376431e3..a60d68de57 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -76,7 +76,7 @@ matrix:
- TEST_TARGET="ci-coquelicot"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
+ - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi"
# ppx_tools_versioned requires a specific version findlib
- FINDLIB_VER=""
- if: NOT (type = pull_request)
@@ -117,6 +117,9 @@ matrix:
- TEST_TARGET="ci-math-comp"
- if: NOT (type = pull_request)
env:
+ - TEST_TARGET="ci-mtac2"
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="ci-sf"
- if: NOT (type = pull_request)
env:
@@ -160,8 +163,6 @@ matrix:
- texlive-fonts-extra
- latex-xcolor
- ghostscript
- - transfig
- - imagemagick
- tipa
- python3
- python3-pip
diff --git a/INSTALL.doc b/INSTALL.doc
index 625c368693..8c578fbd61 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -22,10 +22,7 @@ To produce all the documents, the following tools are needed:
- dvips
- bibtex
- makeindex
- - fig2dev (transfig)
- - convert (ImageMagick)
- hevea
- - hacha
- Python 3
- Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/)
- sphinx_rtd_theme
@@ -38,9 +35,8 @@ Under Debian based operating systems (Debian, Ubuntu, ...) a
working set of packages for compiling the documentation for Coq is:
texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra
- texlive-humanities texlive-pictures latex-xcolor hevea transfig
- imagemagick
- python3 python-pip3
+ texlive-humanities texlive-pictures latex-xcolor hevea python3
+ python-pip3
To install the Python packages required to build the user manual, run:
pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex
diff --git a/Makefile.ci b/Makefile.ci
index 6b30f87232..37b14ed918 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,7 +28,7 @@ CI_TARGETS=ci-bignums \
ci-ltac2 \
ci-math-classes \
ci-math-comp \
- ci-metacoq \
+ ci-mtac2 \
ci-sf \
ci-tlc \
ci-unimath \
diff --git a/Makefile.doc b/Makefile.doc
index ce31c5fcbe..9b6013d8d7 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -32,10 +32,7 @@ BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10
MAKEINDEX:=makeindex
PDFLATEX:=pdflatex
DVIPS:=dvips
-FIG2DEV:=fig2dev
-CONVERT:=convert
HEVEA:=hevea
-HACHA:=hacha
HEVEAOPTS:=-fix -exec xxdate.exe
HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
HTMLSTYLE:=coqremote
@@ -110,20 +107,6 @@ endif
%.ps: %.dvi
(cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`)
-%.png: %.fig
- $(FIG2DEV) -L png -m 2 $< $@
-
-%.pdf: %.fig
- $(FIG2DEV) -L pdftex $< $@
- $(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t
-
-%.eps: %.fig
- $(FIG2DEV) -L pstex $< $@
- $(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t
-
-%.eps: %.png
- $(CONVERT) $< $@
-
######################################################################
# Macros for filtering outputs
######################################################################
diff --git a/configure.ml b/configure.ml
index 2ac705ad27..e77310eb72 100644
--- a/configure.ml
+++ b/configure.ml
@@ -21,11 +21,18 @@ let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
let verbose = ref false (* for debugging this script *)
+let red, yellow, reset =
+ if Unix.isatty Unix.stdout && Unix.isatty Unix.stderr && Sys.os_type = "Unix"
+ then "\027[31m", "\027[33m", "\027[0m"
+ else "", "", ""
+
(** * Utility functions *)
let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc
let cprintf s = cfprintf stdout s
let ceprintf s = cfprintf stderr s
-let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1
+let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1
+
+let warn s = cprintf ("%sWarning: " ^^ s ^^ "%s") yellow reset
let s2i = int_of_string
let i2s = string_of_int
@@ -109,7 +116,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args =
let cmd = String.concat " " (prog::args) in
let exn = match e with Failure s -> s | _ -> Printexc.to_string e in
let msg = sprintf "Error while running '%s' (%s)" cmd exn in
- if fatal then die msg else (cprintf "W: %s" msg; "", [])
+ if fatal then die msg else (warn "%s" msg; "", [])
let tryrun prog args = run ~fatal:false ~err:DevNull prog args
@@ -205,7 +212,7 @@ let win_aware_quote_executable str =
sprintf "%S" str
else
let _ = if contains_suspicious_characters str then
- cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in
+ warn "The string %S contains suspicious characters; ocamlfind might fail" str in
Str.global_replace (Str.regexp "\\\\") "/" str
(** * Date *)
@@ -414,8 +421,8 @@ let args_options = Arg.align [
" Do not add debugging information in the Coq executables";
"-profiling", arg_set (fun p profile -> { p with profile }),
" Add profiling information in the Coq executables";
- "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."),
- " Deprecated. Please use -annot or -bin-annot instead";
+ "-annotate", Arg.Unit (fun () -> die "-annotate has been removed. Please use -annot or -bin-annot instead."),
+ " Removed option. Please use -annot or -bin-annot instead";
"-annot", arg_set (fun p annot -> { p with annot }),
" Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)";
"-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }),
@@ -598,7 +605,7 @@ let check_caml_version () =
else
let () = cprintf "Your version of OCaml is %s." caml_version in
if !prefs.force_caml_version then
- cprintf "*Warning* Your version of OCaml is outdated."
+ warn "Your version of OCaml is outdated."
else
die "You need OCaml 4.02.1 or later."
@@ -620,7 +627,7 @@ let check_findlib_version () =
else
let () = cprintf "Your version of OCamlfind is %s." findlib_version in
if !prefs.force_findlib_version then
- cprintf "*Warning* Your version of OCamlfind is outdated."
+ warn "Your version of OCamlfind is outdated."
else
die "You need OCamlfind 1.4.1 or later."
@@ -731,17 +738,17 @@ let camlp5libdir = shorten_camllib fullcamlp5libdir
(** * Native compiler *)
-let msg_byteonly () =
- cprintf "Only the bytecode version of Coq will be available."
+let msg_byteonly =
+ "Only the bytecode version of Coq will be available."
let msg_no_ocamlopt () =
- cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly ()
+ warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly
let msg_no_camlp5_cmxa () =
- cprintf "Cannot find the native-code library of camlp5."; msg_byteonly ()
+ warn "Cannot find the native-code library of camlp5.\n%s" msg_byteonly
let msg_no_dynlink_cmxa () =
- cprintf "Cannot find native-code dynlink library."; msg_byteonly ();
+ warn "Cannot find native-code dynlink library.\n%s" msg_byteonly;
cprintf "For building a native-code Coq, you may try to first";
cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)";
cprintf "and then run ./configure -natdynlink no"
@@ -757,8 +764,7 @@ let check_native () =
else
let () =
if version <> caml_version then
- cprintf
- "Warning: Native and bytecode compilers do not have the same version!"
+ warn "Native and bytecode compilers do not have the same version!"
in cprintf "You have native-code compilation. Good!"
let best_compiler =
@@ -813,7 +819,7 @@ let get_source = function
(** Is some location a suitable LablGtk2 installation ? *)
let check_lablgtkdir ?(fatal=false) src dir =
- let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in
+ let yell msg = if fatal then die msg else (warn "%s" msg; false) in
let msg = get_source src in
if not (dir_exists dir) then
yell (sprintf "No such directory '%s' (%s)." dir msg)
@@ -849,7 +855,7 @@ let get_lablgtkdir () =
let check_lablgtk_version src dir = match src with
| Manual | Stdlib ->
- cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
+ warn "Could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
(true, "an unknown version")
| OCamlFind ->
let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
@@ -860,7 +866,11 @@ let check_lablgtk_version src dir = match src with
else if vi < [2; 18; 3] then
begin
(* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *)
- cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v;
+ warn "Your installed lablgtk reports as %s.\n\
+It is possible that the installed version is actually more recent\n\
+but reports an incorrect version. If the installed version is\n\
+actually more recent than 2.18.3, that's fine; if it is not,\n
+CoqIDE will compile but may be very unstable." v;
(true, "an unknown version")
end
else
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5566a51175..5cee72cc73 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -19,13 +19,13 @@
: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
########################################################################
: "${unicoq_CI_BRANCH:=master}"
: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
########################################################################
# Mathclasses + Corn
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-mtac2.sh
index a66dc1e762..1372acb8e5 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
# Setup UniCoq
@@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
# Setup MetaCoq
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9b4025866..8d5b5bef4a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n)
(* proof printers *)
let pr_evar ev = Pp.int (Evar.repr ev)
let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
let pr_existentialset evars =
prlist_with_sep spc pr_evar (Evar.Set.elements evars)
let ppexistentialset evars =
diff --git a/engine/universes.ml b/engine/universes.ml
index e5f9212a71..e987087242 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -524,8 +524,6 @@ let new_global_univ () =
(** Simplification *)
-module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
-
let add_list_map u t map =
try
let l = LMap.find u map in
@@ -533,8 +531,6 @@ let add_list_map u t map =
with Not_found ->
LMap.add u [t] map
-module UF = LevelUnionFind
-
(** Precondition: flexible <= ctx *)
let choose_canonical ctx flexible algs s =
let global = LSet.diff s ctx in
@@ -709,6 +705,7 @@ let pr_universe_body = function
let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
+(* Eq < Le < Lt *)
let compare_constraint_type d d' =
match d, d' with
| Eq, Eq -> 0
@@ -742,10 +739,12 @@ let lower_add l c m =
let lower_of_list l =
List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
+
exception Found of Level.t * lowermap
let find_inst insts v =
- try LMap.iter (fun k (enf,alg,v',lower) ->
- if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
+ try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
+ if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
insts; raise Not_found
with Found (f,l) -> (f,l)
@@ -765,18 +764,18 @@ let compute_lbound left =
sup (Universe.super l) lbound
else None))
None left
-
-let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) =
+
+let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
if enforce then
let inst = Universe.make u in
let cstrs' = enforce_leq lbound inst cstrs in
(ctx, us, LSet.remove u algs,
- LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
- (enforce, alg, inst, lower)
+ LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+ {enforce; alg; lbound=inst; lower}
else (* Actually instantiate *)
(Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
- LMap.add u (enforce,alg,lbound,lower) insts, cstrs),
- (enforce, alg, lbound, lower)
+ LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+ {enforce; alg; lbound; lower}
type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
@@ -790,73 +789,82 @@ let _pr_constraints_map (cmap:constraints_map) =
let remove_alg l (ctx, us, algs, insts, cstrs) =
(ctx, us, LSet.remove l algs, insts, cstrs)
-let remove_lower u lower =
- let levels = Universe.levels u in
- LSet.fold (fun l acc -> LMap.remove l acc) levels lower
-
+let not_lower lower (d,l) =
+ (* We're checking if (d,l) is already implied by the lower
+ constraints on some level u. If it represents l < u (d is Lt
+ or d is Le and i > 0, the i < 0 case is impossible due to
+ invariants of Univ), and the lower constraints only have l <=
+ u then it is not implied. *)
+ Univ.Universe.exists
+ (fun (l,i) ->
+ let d =
+ if i == 0 then d
+ else match d with
+ | Le -> Lt
+ | d -> d
+ in
+ try let d' = LMap.find l lower in
+ (* If d is stronger than the already implied lower
+ * constraints we must keep it. *)
+ compare_constraint_type d d' > 0
+ with Not_found ->
+ (** No constraint existing on l *) true) l
+
+exception UpperBoundedAlg
+(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
+ constraints to [lbound], adding them to [cstrs].
+
+ @raise UpperBoundedAlg if any [upper] constraints are strict and
+ [lbound] algebraic. *)
+let enforce_uppers upper lbound cstrs =
+ List.fold_left (fun cstrs (d, r) ->
+ if d == Univ.Le then
+ enforce_leq lbound (Universe.make r) cstrs
+ else
+ match Universe.level lbound with
+ | Some lev -> Constraint.add (lev, d, r) cstrs
+ | None -> raise UpperBoundedAlg)
+ cstrs upper
+
let minimize_univ_variables ctx us algs left right cstrs =
let left, lbounds =
Univ.LMap.fold (fun r lower (left, lbounds as acc) ->
if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
else (* Fixed universe, just compute its glb for sharing *)
- let lbounds' =
+ let lbounds =
match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
| None -> lbounds
- | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower)
+ | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
lbounds
- in (Univ.LMap.remove r left, lbounds'))
+ in (Univ.LMap.remove r left, lbounds))
left (left, Univ.LMap.empty)
in
- let rec instance (ctx', us, algs, insts, cstrs as acc) u =
+ let rec instance (ctx, us, algs, insts, cstrs as acc) u =
let acc, left, lower =
- try
- let l = LMap.find u left in
+ match LMap.find u left with
+ | exception Not_found -> acc, [], LMap.empty
+ | l ->
let acc, left, newlow, lower =
List.fold_left
- (fun (acc, left', newlow, lower') (d, l) ->
- let acc', (enf,alg,l',lower) = aux acc l in
+ (fun (acc, left, newlow, lower') (d, l) ->
+ let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
let l' =
if enf then Universe.make l
else l'
- in acc', (d, l') :: left',
+ in acc', (d, l') :: left,
lower_add l d newlow, lower_union lower lower')
(acc, [], LMap.empty, LMap.empty) l
in
- let not_lower (d,l) =
- (* We're checking if (d,l) is already implied by the lower
- constraints on some level u. If it represents l < u (d is Lt
- or d is Le and i > 0, the i < 0 case is impossible due to
- invariants of Univ), and the lower constraints only have l <=
- u then it is not implied. *)
- Univ.Universe.exists
- (fun (l,i) ->
- let d =
- if i == 0 then d
- else match d with
- | Le -> Lt
- | d -> d
- in
- try let d' = LMap.find l lower in
- (* If d is stronger than the already implied lower
- * constraints we must keep it. *)
- compare_constraint_type d d' > 0
- with Not_found ->
- (** No constraint existing on l *) true) l
- in
- let left = List.uniquize (List.filter not_lower left) in
+ let left = List.uniquize (List.filter (not_lower lower) left) in
(acc, left, LMap.union newlow lower)
- with Not_found -> acc, [], LMap.empty
- and right =
- try Some (LMap.find u right)
- with Not_found -> None
in
let instantiate_lbound lbound =
let alg = LSet.mem u algs in
if alg then
(* u is algebraic: we instantiate it with its lower bound, if any,
or enforce the constraints if it is bounded from the top. *)
- let lower = remove_lower lbound lower in
- instantiate_with_lbound u lbound lower true false acc
+ let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
+ instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
else (* u is non algebraic *)
match Universe.level lbound with
| Some l -> (* The lowerbound is directly a level *)
@@ -867,125 +875,96 @@ let minimize_univ_variables ctx us algs left right cstrs =
if not (Level.equal l u) then
(* Should check that u does not
have upper constraints that are not already in right *)
- let acc' = remove_alg l acc in
- instantiate_with_lbound u lbound lower false false acc'
- else acc, (true, false, lbound, lower)
+ let acc = remove_alg l acc in
+ instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
+ else acc, {enforce=true; alg=false; lbound; lower}
| None ->
- try
- (* Another universe represents the same lower bound,
- we can share them with no harm. *)
- let can, lower = find_inst insts lbound in
- let lower = LMap.remove can lower in
- instantiate_with_lbound u (Universe.make can) lower false false acc
- with Not_found ->
- (* We set u as the canonical universe representing lbound *)
- instantiate_with_lbound u lbound lower false true acc
+ begin match find_inst insts lbound with
+ | can, lower ->
+ (* Another universe represents the same lower bound,
+ we can share them with no harm. *)
+ let lower = LMap.remove can lower in
+ instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
+ | exception Not_found ->
+ (* We set u as the canonical universe representing lbound *)
+ instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
+ end
in
- let acc' acc =
- match right with
- | None -> acc
- | Some cstrs ->
- let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
- if List.is_empty dangling then acc
- else
- let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in
- let cstrs' = List.fold_left (fun cstrs (d, r) ->
- if d == Univ.Le then
- enforce_leq inst (Universe.make r) cstrs
- else
- try let lev = Option.get (Universe.level inst) in
- Constraint.add (lev, d, r) cstrs
- with Option.IsNone -> failwith "")
- cstrs dangling
- in
- (ctx', us, algs, insts, cstrs'), b
+ let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
+ match LMap.find u right with
+ | exception Not_found -> acc
+ | upper ->
+ let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
+ let cstrs = enforce_uppers upper b.lbound cstrs in
+ (ctx, us, algs, insts, cstrs), b
in
- if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
- else
- let lbound = compute_lbound left in
- match lbound with
- | None -> (* Nothing to do *)
- acc' (acc, (true, false, Universe.make u, lower))
- | Some lbound ->
- try acc' (instantiate_lbound lbound)
- with Failure _ -> acc' (acc, (true, false, Universe.make u, lower))
- and aux (ctx', us, algs, seen, cstrs as acc) u =
+ if not (LSet.mem u ctx)
+ then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+ else
+ let lbound = compute_lbound left in
+ match lbound with
+ | None -> (* Nothing to do *)
+ enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
+ | Some lbound ->
+ try enforce_uppers (instantiate_lbound lbound)
+ with UpperBoundedAlg ->
+ enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+ and aux (ctx, us, algs, seen, cstrs as acc) u =
try acc, LMap.find u seen
with Not_found -> instance acc u
in
- LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) ->
+ LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
if v == None then fst (aux acc u)
- else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
+ else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
us (ctx, us, algs, lbounds, cstrs)
let normalize_context_set g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
- let uf = UF.create () in
(** Keep the Prop/Set <= i constraints separate for minimization *)
let smallles, csts =
- Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
- if d == Le then
- if Univ.Level.is_small l then
- if is_set_minimization () && LSet.mem r ctx then
- (Constraint.add cstr smallles, noneqs)
- else (smallles, noneqs)
- else if Level.is_small r then
- if Level.is_prop r then
- raise (Univ.UniverseInconsistency
- (Le,Universe.make l,Universe.make r,None))
- else (smallles, Constraint.add (l,Eq,r) noneqs)
- else (smallles, Constraint.add cstr noneqs)
- else (smallles, Constraint.add cstr noneqs))
- csts (Constraint.empty, Constraint.empty)
+ Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+ in
+ let smallles = if is_set_minimization ()
+ then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+ else Constraint.empty
in
- let csts =
+ let csts, partition =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
- let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+ let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
ctx UGraph.initial_universes
in
- let g =
- Univ.Constraint.fold
- (fun (l, d, r) g ->
- let g =
- if not (Level.is_small l || LSet.mem l ctx) then
- try UGraph.add_universe l false g
- with UGraph.AlreadyDeclared -> g
- else g
- in
- let g =
- if not (Level.is_small r || LSet.mem r ctx) then
- try UGraph.add_universe r false g
- with UGraph.AlreadyDeclared -> g
- else g
- in g) csts g
+ let add_soft u g =
+ if not (Level.is_small u || LSet.mem u ctx)
+ then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+ else g
+ in
+ let g = Constraint.fold
+ (fun (l, d, r) g -> add_soft r (add_soft l g))
+ csts g
in
- let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+ let g = UGraph.merge_constraints csts g in
UGraph.constraints_of_universes g
in
+ (* We ignore the trivial Prop/Set <= i constraints. *)
let noneqs =
- Constraint.fold (fun (l,d,r as cstr) noneqs ->
- if d == Eq then (UF.union l r uf; noneqs)
- else (* We ignore the trivial Prop/Set <= i constraints. *)
- if d == Le && Univ.Level.is_small l then noneqs
- else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
- then noneqs
- else Constraint.add cstr noneqs)
- csts Constraint.empty
+ Constraint.filter
+ (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+ (Level.is_prop l && d == Lt && Level.is_set r)))
+ csts
in
let noneqs = Constraint.union noneqs smallles in
- let partition = UF.partition uf in
let flex x = LMap.mem x us in
let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
(* Add equalities for globals which can't be merged anymore. *)
let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) global
+ Constraint.add (canon, Eq, g) cst) global
cstrs
in
(* Also add equalities for rigid variables *)
let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) rigid
+ Constraint.add (canon, Eq, g) cst) rigid
cstrs
in
let canonu = Some (Universe.make canon) in
diff --git a/engine/universes.mli b/engine/universes.mli
index 4823c57463..a0a7749f8b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -162,8 +162,6 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t ->
(a global one if there is one) and transitively saturate
the constraints w.r.t to the equalities. *)
-module UF : Unionfind.PartitionSig with type elt = Level.t
-
val level_subst_of : universe_subst_fn -> universe_level_subst_fn
val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 70dc6867ac..a771945dd2 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -829,6 +829,8 @@ let is_univ_copy max u =
else
false
+let dump_bytecode = ref false
+
let dump_bytecodes init code fvs =
let open Pp in
(str "code =" ++ fnl () ++
@@ -872,7 +874,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
reloc, init_code
in
let fv = List.rev (!(reloc.in_env).fv_rev) in
- (if !Flags.dump_bytecode then
+ (if !dump_bytecode then
Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive msg ->
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index abab58b60b..1c4cdcbeb4 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool ->
(** Shortcut of the previous function used during module strengthening *)
val compile_alias : Names.Constant.t -> body_code
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 7b637c20e6..641d424e2c 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -807,7 +807,7 @@ and lambda_of_args env start args =
(*********************************)
-
+let dump_lambda = ref false
let optimize_lambda lam =
let lam = simplify subst_id lam in
@@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c =
Renv.push_rels env (Array.of_list ids);
let lam = lambda_of_constr env c in
let lam = if optimize then optimize_lambda lam else lam in
- if !Flags.dump_lambda then
+ if !dump_lambda then
Feedback.msg_debug (pp_lam lam);
lam
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 89b7fd8e3b..6cf46163e3 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -25,3 +25,6 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda
(*spiwack: compiling function to insert dynamic decompilation before
matching integers (in case they are in processor representation) *)
val int31_escape_before_match : bool -> lambda -> lambda
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d1644614d..e6b27077ba 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -21,7 +21,7 @@ open Univ
(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu
Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
(* Universes are stratified by a partial ordering $\le$.
@@ -557,8 +557,7 @@ let get_explanation strict u v g =
else match traverse strict u with Some exp -> exp | None -> assert false
let get_explanation strict u v g =
- if !Flags.univ_print then Some (get_explanation strict u v g)
- else None
+ Some (lazy (get_explanation strict u v g))
(* To compare two nodes, we simply do a forward search.
We implement two improvements:
@@ -768,18 +767,18 @@ let normalize_universes g =
g.entries g
let constraints_of_universes g =
+ let module UF = Unionfind.Make (LSet) (LMap) in
+ let uf = UF.create () in
let constraints_of u v acc =
match v with
| Canonical {univ=u; ltle} ->
UMap.fold (fun v strict acc->
let typ = if strict then Lt else Le in
Constraint.add (u,typ,v) acc) ltle acc
- | Equiv v -> Constraint.add (u,Eq,v) acc
+ | Equiv v -> UF.union u v uf; acc
in
- UMap.fold constraints_of g.entries Constraint.empty
-
-let constraints_of_universes g =
- constraints_of_universes (normalize_universes g)
+ let csts = UMap.fold constraints_of g.entries Constraint.empty in
+ csts, UF.partition uf
(** [sort_universes g] builds a totally ordered universe graph. The
output graph should imply the input graph (and the implication
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index d4fba63fb3..cca2eb472b 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -59,7 +59,10 @@ val empty_universes : t
val sort_universes : t -> t
-val constraints_of_universes : t -> Constraint.t
+(** [constraints_of_universes g] returns [csts] and [partition] where
+ [csts] are the non-Eq constraints and [partition] is the partition
+ of the universes into equivalence classes. *)
+val constraints_of_universes : t -> Constraint.t * LSet.t list
val check_subtype : AUContext.t check_function
(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ea3a522953..8e19fa4e52 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -541,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with
(* Universe inconsistency: error raised when trying to enforce a relation
that would create a cycle in the graph of universes. *)
-type univ_inconsistency = constraint_type * universe * universe * explanation option
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
raise (UniverseInconsistency (o,make u,make v,p))
(* Constraints and sets of constraints. *)
@@ -1235,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) =
| Eq -> str"=" | Lt -> str"<" | Le -> str"<="
in
let reason = match p with
- | None | Some [] -> mt()
+ | None -> mt()
| Some p ->
- str " because" ++ spc() ++ pr_uni v ++
+ let p = Lazy.force p in
+ if p = [] then mt ()
+ else
+ str " because" ++ spc() ++ pr_uni v ++
prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
- p ++
+ p ++
(if Universe.equal (snd (List.last p)) u then mt() else
- (spc() ++ str "= " ++ pr_uni u))
+ (spc() ++ str "= " ++ pr_uni u))
in
str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
pr_rel o ++ spc() ++ pr_uni v ++ reason
diff --git a/kernel/univ.mli b/kernel/univ.mli
index aaed899bf4..b68bbdf359 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -205,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function
Constraint.t...
*)
type explanation = (constraint_type * Universe.t) list
-type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option
+type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e07..56940f1cf7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -60,7 +60,6 @@ let profile = false
let ide_slave = ref false
let raw_print = ref false
-let univ_print = ref false
let we_are_parsing = ref false
@@ -160,11 +159,3 @@ let print_mod_uid = ref false
let profile_ltac = ref false
let profile_ltac_cutoff = ref 2.0
-
-let dump_bytecode = ref false
-let set_dump_bytecode = (:=) dump_bytecode
-let get_dump_bytecode () = !dump_bytecode
-
-let dump_lambda = ref false
-let set_dump_lambda = (:=) dump_lambda
-let get_dump_lambda () = !dump_lambda
diff --git a/lib/flags.mli b/lib/flags.mli
index 85aaf879f3..17776d68a4 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -10,6 +10,25 @@
(** Global options of the system. *)
+(** WARNING: don't add new entries to this file!
+
+ This file is own its way to deprecation in favor of a purely
+ functional state, but meanwhile it will contain options that are
+ truly global to the system such as [compat] or [debug]
+
+ If you are thinking about adding a global flag, well, just
+ don't. First of all, options make testins exponentially more
+ expensive, due to the growth of flag combinations. So please make
+ some effort in order for your idea to work in a configuration-free
+ manner.
+
+ If you absolutely must pass an option to your new system, then do
+ so as a functional argument so flags are exposed to unit
+ testing. Then, register such parameters with the proper
+ state-handling mechanism of the top-level subsystem of Coq.
+
+ *)
+
(** Command-line flags *)
val boot : bool ref
@@ -42,9 +61,6 @@ val we_are_parsing : bool ref
(* Set Printing All flag. For some reason it is a global flag *)
val raw_print : bool ref
-(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
-val univ_print : bool ref
-
type compat_version = V8_6 | V8_7 | Current
val compat_version : compat_version ref
val version_compare : compat_version -> compat_version -> int
@@ -129,13 +145,3 @@ val print_mod_uid : bool ref
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref
-
-(** Dump the bytecode after compilation (for debugging purposes) *)
-val dump_bytecode : bool ref
-val set_dump_bytecode : bool -> unit
-val get_dump_bytecode : unit -> bool
-
-(** Dump the VM lambda code after compilation (for debugging purposes) *)
-val dump_lambda : bool ref
-val set_dump_lambda : bool -> unit
-val get_dump_lambda : unit -> bool
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb563220b6..56e5828918 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -36,7 +36,7 @@ type _ delay =
| Later : [ `thunk ] delay
(** Should we keep details of universes during detyping ? *)
-let print_universes = Flags.univ_print
+let print_universes = ref false
(** If true, prints local context of evars, whatever print_arguments *)
let print_evar_arguments = ref false
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 947469ca0e..e68a25a873 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1118,7 +1118,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
with Not_found ->
try
let (n,_,t') = lookup_rel_id id (rel_context env) in
- if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found
+ if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found
with Not_found ->
try
let t' = env |> lookup_named id |> NamedDecl.get_type in
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 5b13f35d57..253b48e4d9 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -421,3 +421,8 @@ Goal exists n : nat, n = n -> True.
eexists.
set (H := _ = _).
Abort.
+
+(* Check interpretation of default evar instance in pretyping *)
+(* (reported as bug #7356) *)
+
+Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z).
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 19658806c5..8c48490ffe 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1465,22 +1465,22 @@ let _ =
optkey = ["Printing";"Universes"];
optread = (fun () -> !Constrextern.print_universes);
optwrite = (fun b -> Constrextern.print_universes:=b) }
-
+
let _ =
declare_bool_option
{ optdepr = false;
optname = "dumping bytecode after compilation";
optkey = ["Dump";"Bytecode"];
- optread = Flags.get_dump_bytecode;
- optwrite = Flags.set_dump_bytecode }
+ optread = (fun () -> !Cbytegen.dump_bytecode);
+ optwrite = (:=) Cbytegen.dump_bytecode }
let _ =
declare_bool_option
{ optdepr = false;
optname = "dumping VM lambda code after compilation";
optkey = ["Dump";"Lambda"];
- optread = Flags.get_dump_lambda;
- optwrite = Flags.set_dump_lambda }
+ optread = (fun () -> !Clambda.dump_lambda);
+ optwrite = (:=) Clambda.dump_lambda }
let _ =
declare_bool_option
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:14:22 +0000