aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.dune8
-rw-r--r--checker/checker.ml4
-rw-r--r--checker/univ.ml5
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh474
-rw-r--r--dev/build/windows/patches_coq/coq_new.nsi188
-rwxr-xr-xdev/build/windows/patches_coq/quickchick.patch26
-rwxr-xr-xdev/ci/ci-basic-overlay.sh25
-rwxr-xr-xdev/ci/gitlab.bat16
-rw-r--r--dev/dune-workspace.all2
-rw-r--r--engine/termops.mli6
-rw-r--r--library/decls.ml22
-rw-r--r--library/decls.mli9
-rw-r--r--pretyping/typeclasses.ml14
-rw-r--r--pretyping/typeclasses.mli3
-rw-r--r--vernac/lemmas.ml8
-rw-r--r--vernac/lemmas.mli6
-rw-r--r--vernac/obligations.ml4
17 files changed, 667 insertions, 153 deletions
diff --git a/Makefile.dune b/Makefile.dune
index ac5f584b90..6733c485fa 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,7 +1,7 @@
# -*- mode: makefile -*-
# Dune Makefile for Coq
-.PHONY: help voboot states world watch release apidoc clean
+.PHONY: voboot states world watch release apidoc ocheck clean help
# use DUNEOPT=--display=short for a more verbose build
# DUNEOPT=--display=short
@@ -29,9 +29,6 @@ states: voboot
world: voboot
dune build $(DUNEOPT) @install
-ocheck: voboot
- dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
-
watch: voboot
dune build $(DUNEOPT) @install -w
@@ -41,6 +38,9 @@ release: voboot
apidoc: voboot
dune build $(DUNEOPT) @doc
+ocheck: voboot
+ dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
+
clean:
dune clean
diff --git a/checker/checker.ml b/checker/checker.ml
index d3d114d7d7..8a5220c9ca 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -243,7 +243,9 @@ let explain_exn = function
| Invalid_argument s ->
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
| Sys.Break ->
- hov 0 (fnl () ++ str "User interrupt.")
+ hov 0 (fnl () ++ str "User interrupt.")
+ | Univ.AlreadyDeclared ->
+ hov 0 (str "Error: Multiply declared universe.")
| Univ.UniverseInconsistency (o,u,v) ->
let msg =
if !Flags.debug (*!Constrextern.print_universes*) then
diff --git a/checker/univ.ml b/checker/univ.ml
index e50e883adf..a0511ad21b 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1088,14 +1088,13 @@ let subst_univs_universe fn ul =
let merge_context strict ctx g =
let g = Array.fold_left
- (* Be lenient, module typing reintroduces universes and
- constraints due to includes *)
- (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+ (fun g v -> add_universe v strict g)
g (UContext.instance ctx)
in merge_constraints (UContext.constraints ctx) g
let merge_context_set strict ctx g =
let g = LSet.fold
+ (* Include and side effects still have double-declared universes *)
(fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
(ContextSet.levels ctx) g
in merge_constraints (ContextSet.constraints ctx) g
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 74dd4d41c1..5f07aa8fca 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -2,7 +2,7 @@
###################### COPYRIGHT/COPYLEFT ######################
-# (C) 2016 Intel Deutschland GmbH
+# (C) 2016..2018 Intel Deutschland GmbH
# Author: Michael Soegtrop
#
# Released to the public by Intel under the
@@ -238,9 +238,10 @@ fi
# $1 file server name including protocol prefix
# $2 file name (without extension)
# $3 file extension
-# $4 number of path levels to strip from tar (usually 1)
-# $5 module name (if different from archive)
-# $6 expand folder name (if different from module name)
+# $4 [optional] number of path levels to strip from tar (usually 1)
+# $5 [optional] module name (if different from archive)
+# $6 [optional] expand folder name (if different from module name)
+# $7 [optional] module base name (used as 2nd choice for patches, defaults to $5)
# ------------------------------------------------------------------------------
function get_expand_source_tar {
@@ -263,6 +264,12 @@ function get_expand_source_tar {
folder=$name
fi
+ if [ "$#" -ge 7 ] ; then
+ basename=$7
+ else
+ basename=$name
+ fi
+
# Set logging target
logtargetold=$LOGTARGET
LOGTARGET=$name
@@ -314,8 +321,11 @@ function get_expand_source_tar {
fi
# Patch if patch file exists
+ # First try specific patch file name then generic patch file name
if [ -f "$PATCHES/$name.patch" ] ; then
log1 patch -p1 -i "$PATCHES/$name.patch"
+ elif [ -f "$PATCHES/$basename.patch" ] ; then
+ log1 patch -p1 -i "$PATCHES/$basename.patch"
fi
# Go back to base folder
@@ -340,6 +350,7 @@ function get_expand_source_tar {
# $3 file extension
# $4 [optional] number of path levels to strip from tar (usually 1)
# $5 [optional] module name (if different from archive)
+# $6 [optional] module base name (used as 2nd choice for patches, defaults to $5)
# ------------------------------------------------------------------------------
function build_prep {
@@ -356,6 +367,15 @@ function build_prep {
name=$2
fi
+ if [ "$#" -ge 6 ] ; then
+ basename=$6
+ else
+ basename=$name
+ fi
+
+ # Set installer section to not set by default
+ installersection=
+
# Check if build is already done
if [ ! -f "$FLAGFILES/$name.finished" ] ; then
BUILD_PACKAGE_NAME=$name
@@ -365,7 +385,7 @@ function build_prep {
touch "$FLAGFILES/$name.started"
- get_expand_source_tar "$1" "$2" "$3" "$strip" "$name"
+ get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" "$name" "$basename"
cd "$name"
@@ -381,6 +401,61 @@ function build_prep {
}
# ------------------------------------------------------------------------------
+# Like build_prep, but gets the data from an entry in ci-basic-overlay.sh
+# This assumes the following definitions exist in ci-basic-overlay.sh,
+# or in a file in the user-overlays folder:
+# $1_CI_REF
+# $1_CI_ARCHIVEURL
+# $1_CI_GITURL
+# ATTENTION: variables in ci-basic-overlay.sh are loaded by load_overlay_data.
+# load_overlay_data is is called at the end of make_coq (even if the build is skipped)
+#
+# Parameters
+# $1 base name of module in ci-basic-overlay.sh, e.g. mathcomp, bignums, ...
+# ------------------------------------------------------------------------------
+
+function build_prep_overlay {
+ urlvar=$1_CI_ARCHIVEURL
+ gitvar=$1_CI_GITURL
+ refvar=$1_CI_REF
+ url=${!urlvar}
+ git=${!gitvar}
+ ref=${!refvar}
+ ver=$(git ls-remote "$git" "refs/heads/$ref" | cut -f 1)
+ if [[ "$ver" == "" ]]; then
+ # $1_CI_REF must have been a tag or hash, not a branch
+ ver="$ref"
+ fi
+ build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
+}
+
+# ------------------------------------------------------------------------------
+# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh
+# ------------------------------------------------------------------------------
+
+function load_overlay_data {
+ if [ -n "${GITLAB_CI+}" ]; then
+ export CI_BRANCH="$CI_COMMIT_REF_NAME"
+ if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
+ export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+ else
+ export CI_PULL_REQUEST=""
+ fi
+ else
+ export CI_BRANCH=""
+ export CI_PULL_REQUEST=""
+ # Used when building 8.8.0 with the latest scripts
+ export TRAVIS_BRANCH=""
+ export TRAVIS_PULL_REQUEST=""
+ fi
+
+ for overlay in /build/user-overlays/*.sh; do
+ . "$overlay"
+ done
+ . /build/ci-basic-overlay.sh
+}
+
+# ------------------------------------------------------------------------------
# Finalize a module build
# - create name.finished
# - go back to base folder
@@ -392,6 +467,7 @@ function build_post {
touch "$FLAGFILES/$BUILD_PACKAGE_NAME.finished"
PATH=$BUILD_OLDPATH
LOGTARGET=other
+ installer_addon_end
fi
}
@@ -522,6 +598,101 @@ function files_to_nsis {
tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
}
+# ------------------------------------------------------------------------------
+# Create an nsis installer addon section
+#
+# parameters
+# $1 identifier of installer section and base name of file list files
+# $2 human readable name of section
+# $3 description of section
+# $4 flags (space separated list of keywords): off = default off
+#
+# $1 must be a valid NSIS identifier!
+# ------------------------------------------------------------------------------
+
+function installer_addon_section {
+ installersection=$1
+ list_files "addon_pre_$installersection"
+
+ echo 'LangString' "DESC_$1" '${LANG_ENGLISH}' "\"$3\"" >> "/build/filelists/addon_strings.nsh"
+
+ echo '!insertmacro MUI_DESCRIPTION_TEXT' '${'"Sec_$1"'}' '$('"DESC_$1"')' >> "/build/filelists/addon_descriptions.nsh"
+
+ local sectionoptions=
+ if [[ "$4" == *off* ]] ; then sectionoptions+=" /o" ; fi
+
+ echo "Section $sectionoptions \"$2\" Sec_$1" >> "/build/filelists/addon_sections.nsh"
+ echo 'SetOutPath "$INSTDIR\"' >> "/build/filelists/addon_sections.nsh"
+ echo '!include "..\..\..\filelists\addon_'"$1"'.nsh"' >> "/build/filelists/addon_sections.nsh"
+ echo 'SectionEnd' >> "/build/filelists/addon_sections.nsh"
+}
+
+# ------------------------------------------------------------------------------
+# Start an installer addon dependency group
+#
+# parameters
+# $1 identifier of the section which depends on other sections
+# The parameters must match the $1 parameter of a installer_addon_section call
+# ------------------------------------------------------------------------------
+
+dependencysections=
+
+function installer_addon_dependency_beg {
+ installer_addon_dependency "$1"
+ dependencysections="$1 $dependencysections"
+}
+
+# ------------------------------------------------------------------------------
+# End an installer addon dependency group
+# ------------------------------------------------------------------------------
+
+function installer_addon_dependency_end {
+ set -- $dependencysections
+ shift
+ dependencysections="$*"
+}
+
+# ------------------------------------------------------------------------------
+# Create an nsis installer addon dependency entry
+# This needs to be bracketed with installer_addon_dependencies_beg/end
+#
+# parameters
+# $1 identifier of the section on which other sections might depend
+# The parameters must match the $1 parameter of a installer_addon_section call
+# ------------------------------------------------------------------------------
+
+function installer_addon_dependency {
+ for section in $dependencysections ; do
+ echo '${CheckSectionDependency} ${Sec_'"$section"'} ${Sec_'"$1"'} '"'$section' '$1'" >> "/build/filelists/addon_dependencies.nsh"
+ done
+}
+
+# ------------------------------------------------------------------------------
+# Finish an installer section after an addon build
+#
+# This creates the file list files
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function installer_addon_end {
+ if [ -n "$installersection" ]; then
+ list_files "addon_post_$installersection"
+ diff_files "addon_$installersection" "addon_post_$installersection" "addon_pre_$installersection"
+ files_to_nsis "addon_$installersection"
+ fi
+}
+
+# ------------------------------------------------------------------------------
+# Set all timeouts in all .v files to 1000
+# Since timeouts can lead to CI failures, this is useful
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function coq_set_timeouts_1000 {
+ find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/'
+}
###################### MODULE BUILD FUNCTIONS #####################
@@ -1287,6 +1458,8 @@ function make_coq {
build_post
fi
+
+ load_overlay_data
}
##### GNU Make for MinGW #####
@@ -1450,18 +1623,15 @@ function make_coq_installer {
fi
}
-###################### ADDONS #####################
+###################### ADDON COQ LIBRARIES / PLUGINS / TOOLS #####################
# The bignums library
# Provides BigN, BigZ, BigQ that used to be part of Coq standard library
function make_addon_bignums {
- bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1)
- if [[ "$bignums_SHA" == "" ]]; then
- # $bignums_CI_REF must have been a tag / commit and not a branch
- bignums_SHA="$bignums_CI_REF"
- fi
- if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then
+ installer_addon_dependency bignums
+ if build_prep_overlay bignums; then
+ installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" ""
# To make command lines shorter :-(
echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
log1 make all
@@ -1470,61 +1640,277 @@ function make_addon_bignums {
fi
}
+# Equations plugin
+# A function definition plugin
+
+function make_addon_equations {
+ installer_addon_dependency equations
+ if build_prep_overlay Equations; then
+ installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" ""
+ # Note: PATH is automatically saved/restored by build_prep / build_post
+ PATH=$COQBIN:$PATH
+ logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+ log1 make
+ log2 make install
+ build_post
+ fi
+}
+
+# mathcomp - ssreflect and mathematical components library
+
+function make_addon_mathcomp {
+ installer_addon_dependency mathcomp
+ if build_prep_overlay mathcomp; then
+ installer_addon_section mathcomp "Math-Components" "Coq library with mathematical components" ""
+ cd mathcomp
+ log1 make $MAKE_OPT
+ log2 make install
+ build_post
+ fi
+}
+
+# ssreflect part of mathcomp
+
+function make_addon_ssreflect {
+ # if mathcomp addon is requested, build this instead
+ if [[ "$COQ_ADDONS" == *mathcomp* ]]; then
+ make_addon_mathcomp
+ else
+ # Note: since either mathcomp or ssreflect is defined, it is fine to name both mathcomp
+ installer_addon_dependency ssreflect
+ if build_prep_overlay mathcomp; then
+ installer_addon_section ssreflect "SSReflect" "Coq support library for small scale reflection plugin" ""
+ cd mathcomp
+ logn make-makefile make Makefile.coq
+ logn make-ssreflect make $MAKE_OPT -f Makefile.coq ssreflect/all_ssreflect.vo
+ logn make-install make -f Makefile.coq install
+ build_post
+ fi
+ fi
+}
+
# Ltac-2 plugin
# A new (experimental) tactic language
function make_addon_ltac2 {
- ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1)
- if [[ "$ltac2_SHA" == "" ]]; then
- # $ltac2_CI_REF must have been a tag / commit and not a branch
- ltac2_SHA="$ltac2_CI_REF"
- fi
- if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then
+ installer_addon_dependency ltac2
+ if build_prep_overlay ltac2; then
+ installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
log1 make all
log2 make install
build_post
fi
}
-# Equations plugin
-# A function definition plugin
-
-function make_addon_equations {
- Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1)
- if [[ "$Equations_SHA" == "" ]]; then
- # $Equations_CI_REF must have been a tag / commit and not a branch
- Equations_SHA="$Equations_CI_REF"
+# UniCoq plugin
+# An alternative unification algorithm
+function make_addon_unicoq {
+ installer_addon_dependency unicoq
+ if build_prep_overlay unicoq; then
+ installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" ""
+ log1 coq_makefile -f Make -o Makefile
+ log1 make
+ log2 make install
+ build_post
fi
- if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then
- # Note: PATH is autmatically saved/restored by build_prep / build_post
- PATH=$COQBIN:$PATH
- logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+}
+
+# Mtac2 plugin
+# An alternative typed tactic language
+function make_addon_mtac2 {
+ installer_addon_dependency_beg mtac2
+ make_addon_unicoq
+ installer_addon_dependency_end
+ if build_prep_overlay mtac2; then
+ installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." ""
+ log1 coq_makefile -f _CoqProject -o Makefile
log1 make
log2 make install
build_post
fi
}
-function make_addons {
- if [ -n "$GITLAB_CI" ]; then
- export CI_BRANCH="$CI_COMMIT_REF_NAME"
- if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
- export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
- else
- export CI_PULL_REQUEST=""
+# Menhir parser generator
+
+function make_addon_menhir {
+ make_menhir
+ # If COQ and OCaml are installed to the same folder, there is nothing to do
+ installer_addon_dependency menhir
+ if [ "$PREFIXOCAML" != "$PREFIXCOQ" ] ; then
+ # Just install menhir files required for COQ to COQ target folder
+ if [ ! -f "$FLAGFILES/menhir-addon.finished" ] ; then
+ installer_addon_section menhir "Menhir" "Menhir parser generator windows executable and libraries" ""
+ LOGTARGET=menhir-addon
+ touch "$FLAGFILES/menhir-addon.started"
+ # Menhir executable
+ install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/"
+ # Menhir Standard library
+ install_glob "$PREFIXOCAML/share/menhir/" '*.mly' "$PREFIXCOQ/share/menhir/"
+ # Menhir PDF doc
+ install_glob "$PREFIXOCAML/share/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/"
+ touch "$FLAGFILES/menhir-addon.finished"
+ LOGTARGET=other
+ installer_addon_end
fi
- else
- export CI_BRANCH=""
- export CI_PULL_REQUEST=""
fi
- for overlay in /build/user-overlays/*.sh; do
- . "$overlay"
- done
- . /build/ci-basic-overlay.sh
+}
+
+# COQ library for Menhir
+
+function make_addon_menhirlib {
+ installer_addon_dependency menhirlib
+ if build_prep_overlay menhirlib; then
+ installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" ""
+ # The supplied makefiles don't work in any way on cygwin
+ cd src
+ echo -R . MenhirLib > _CoqProject
+ ls -1 *.v >> _CoqProject
+ log1 coq_makefile -f _CoqProject -o Makefile.coq
+ log1 make -f Makefile.coq all
+ logn make-install make -f Makefile.coq install
+ build_post
+ fi
+}
+
+# CompCert
+
+function make_addon_compcert {
+ installer_addon_dependency_beg compcert
+ make_menhir
+ make_addon_menhirlib
+ installer_addon_dependency_end
+ if build_prep_overlay CompCert; then
+ installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off"
+ logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin
+ log1 make
+ log2 make install
+ logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE"
+ logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE"
+ build_post
+ fi
+}
+
+# Princeton VST
+
+function install_addon_vst {
+ VSTDEST="$PREFIXCOQ/lib/coq/user-contrib/VST"
+
+ # Install VST .v, .vo, .c and .h files
+ install_rec compcert '*.v' "$VSTDEST/compcert/"
+ install_rec compcert '*.vo' "$VSTDEST/compcert/"
+ install_glob "msl" '*.v' "$VSTDEST/msl/"
+ install_glob "msl" '*.vo' "$VSTDEST/msl/"
+ install_glob "sepcomp" '*.v' "$VSTDEST/sepcomp/"
+ install_glob "sepcomp" '*.vo' "$VSTDEST/sepcomp/"
+ install_glob "floyd" '*.v' "$VSTDEST/floyd/"
+ install_glob "floyd" '*.vo' "$VSTDEST/floyd/"
+ install_glob "progs" '*.v' "$VSTDEST/progs/"
+ install_glob "progs" '*.c' "$VSTDEST/progs/"
+ install_glob "progs" '*.h' "$VSTDEST/progs/"
+ install_glob "veric" '*.v' "$VSTDEST/msl/"
+ install_glob "veric" '*.vo' "$VSTDEST/msl/"
+
+ # Install VST documentation files
+ install_glob "." 'LICENSE' "$VSTDEST"
+ install_glob "." '*.md' "$VSTDEST"
+ install_glob "compcert" '*' "$VSTDEST/compcert"
+ install_glob "doc" '*.pdf' "$VSTDEST/doc"
+
+ # Install VST _CoqProject files
+ install_glob "." '_CoqProject*' "$VSTDEST"
+ install_glob "." '_CoqProject-export' "$VSTDEST/progs"
+}
+
+function make_addon_vst {
+ installer_addon_dependency vst
+ if build_prep_overlay VST; then
+ installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off"
+ log1 coq_set_timeouts_1000
+ log1 make IGNORECOQVERSION=true $MAKE_OPT
+ log1 install_addon_vst
+ build_post
+ fi
+}
+
+# coquelicot Real analysis
+
+function make_addon_coquelicot {
+ installer_addon_dependency_beg coquelicot
+ make_addon_ssreflect
+ installer_addon_dependency_end
+ if build_prep_overlay Coquelicot; then
+ installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" ""
+ logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot"
+ logn remake ./remake
+ logn remake-install ./remake install
+ build_post
+ fi
+}
+
+# AAC associative / commutative rewriting
+
+function make_addon_aactactics {
+ installer_addon_dependency aac
+ if build_prep_overlay aactactis; then
+ installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
+ log1 make
+ log2 make install
+ build_post
+ fi
+}
+
+# extlib
+
+function make_addon_extlib {
+ installer_addon_dependency extlib
+ if build_prep_overlay ext_lib; then
+ installer_addon_section extlib "Ext-Lib" "Coq library with many reusable general purpose components" ""
+ log1 make $MAKE_OPT
+ log2 make install
+ build_post
+ fi
+}
+
+# SimpleIO
+
+function make_addon_simple_io {
+ installer_addon_dependency simpleIO
+ if build_prep_overlay simple_io; then
+ installer_addon_section simpleIO "SimpleIO" "Coq plugin for reading and writing files directly from Coq code" ""
+ log1 make $MAKE_OPT
+ log2 make install
+ build_post
+ fi
+}
+
+# Quickchick Randomized Property-Based Testing Plugin for Coq
+
+function make_addon_quickchick {
+ installer_addon_dependency_beg quickchick
+ make_addon_ssreflect
+ make_addon_extlib
+ make_addon_simple_io
+ make_ocamlbuild
+ installer_addon_dependency_end
+ if build_prep_overlay quickchick; then
+ installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" ""
+ log1 make
+ log2 make install
+ build_post
+ fi
+}
+
+# Main function for building addons
+
+function make_addons {
+ # Note: ':' is the empty command, which does not produce any output
+ : > "/build/filelists/addon_dependencies.nsh"
for addon in $COQ_ADDONS; do
"make_addon_$addon"
done
+
+ sort -u -o "/build/filelists/addon_dependencies.nsh" "/build/filelists/addon_dependencies.nsh"
}
###################### TOP LEVEL BUILD #####################
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
index 55fba6d5ab..9947965c28 100644
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -38,43 +38,20 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \
;Folder selection page
InstallDir "C:\${MY_PRODUCT}"
-
+
;Remember install folder
InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
;--------------------------------
-;Modern UI Configuration
-
- !define MUI_ICON "${COQ_ICON}"
-
- !insertmacro MUI_PAGE_WELCOME
- !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
- !insertmacro MUI_PAGE_COMPONENTS
- !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces."
- !insertmacro MUI_PAGE_DIRECTORY
- !insertmacro MUI_PAGE_INSTFILES
- !insertmacro MUI_PAGE_FINISH
-
- !insertmacro MUI_UNPAGE_WELCOME
- !insertmacro MUI_UNPAGE_CONFIRM
- !insertmacro MUI_UNPAGE_INSTFILES
- !insertmacro MUI_UNPAGE_FINISH
-
-;--------------------------------
-;Languages
-
- !insertmacro MUI_LANGUAGE "English"
-
-;--------------------------------
-;Language Strings
+;Extra license pages
- ;Description
- LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
- LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
- ;LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development."
- LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
- LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
- LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
+!macro MUI_PAGE_LICENSE_EXTRA Licensefile Header Subheader Bottom SelFunc
+ !define MUI_PAGE_HEADER_TEXT "${Header}"
+ !define MUI_PAGE_HEADER_SUBTEXT "${Subheader}"
+ !define MUI_LICENSEPAGE_TEXT_BOTTOM "${Bottom}"
+ !define MUI_PAGE_CUSTOMFUNCTION_PRE ${SelFunc}
+ !insertmacro MUI_PAGE_LICENSE "${Licensefile}"
+!macroend
;--------------------------------
; Check for white spaces
@@ -95,7 +72,6 @@ FunctionEnd
;--------------------------------
;Installer Sections
-
Section "Coq" Sec1
SetOutPath "$INSTDIR\"
@@ -105,7 +81,7 @@ Section "Coq" Sec1
;Store install folder
WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
-
+
;Create uninstaller
WriteUninstaller "$INSTDIR\Uninstall.exe"
WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
@@ -123,7 +99,7 @@ Section "Coq" Sec1
; Create start menu entries
; SetOutPath is required for the path in the .lnk files
- SetOutPath "$INSTDIR"
+ SetOutPath "$INSTDIR"
CreateDirectory "$SMPROGRAMS\Coq"
; The first shortcut set here is treated as main application by Windows 7/8.
; Use CoqIDE as main application
@@ -138,24 +114,23 @@ SectionEnd
;OCAML Section "Ocaml for native compute and plugin development" Sec2
;OCAML SetOutPath "$INSTDIR\"
;OCAML !include "..\..\..\filelists\ocaml.nsh"
-;OCAML
+;OCAML
;OCAML ; Create a few slash / backslash variants of the source and install path
;OCAML ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR}
;OCAML !insertmacro StrRep $COQ_SRC_PATH_BS ${COQ_SRC_PATH} "/" "\"
;OCAML !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\"
;OCAML !insertmacro StrRep $INSTDIR_DBS $INSTDIR "\" "\\"
-;OCAML
+;OCAML
;OCAML ; Replace absolute paths in some OCaml config files
;OCAML ; These are not all, see ReadMe.txt
;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/" "\"
;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS" "$INSTDIR"
;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS"
;OCAML SectionEnd
-
-Section "Coq packages" Sec2
- SetOutPath "$INSTDIR\"
- !include "..\..\..\filelists\coq_addons.nsh"
-SectionEnd
+
+SectionGroup "Coq addons" Sec2
+ !include "..\..\..\filelists\addon_sections.nsh"
+SectionGroupEnd
Section "Coq files for plugin developers" Sec3
SetOutPath "$INSTDIR\"
@@ -179,6 +154,130 @@ SectionEnd
;OCAML SectionEnd
;--------------------------------
+;Section dependencies
+
+; Parameters on the stack:
+; top-0 : section B on which section A dependencies
+; top-1 : section A, which depends on section B
+; top-2 : name of section B
+; top-3 : name of section A
+
+Function CheckSectionDependency
+ ; stack=nameB nameA secB secA rest
+ Exch $R3 ; stack=$R3 nameA secB secA rest; $R3=nameB
+ Exch ; stack=nameA $R3 secB secA rest
+ Exch $R2 ; stack=$R2 $R3 secB secA rest; $R2=nameA
+ Exch 2 ; stack=secB $R3 $R2 secA rest
+ Exch $R1 ; stack=$R1 $R3 $R2 secA rest; $R1=secB
+ Exch 3 ; stack=secA $R3 $R2 $R1 rest;
+ Exch $R0 ; stack=$R0 $R3 $R2 $R1 rest; $R0=secA
+ ; Take care of save order when popping the stack!
+ Push $R4
+ Push $R5
+
+ SectionGetFlags $R0 $R0
+ IntOp $R0 $R0 & ${SF_SELECTED}
+
+ SectionGetFlags $R1 $R4
+ IntOp $R5 $R4 & ${SF_SELECTED}
+
+ ${If} $R0 == ${SF_SELECTED}
+ ${AndIf} $R5 != ${SF_SELECTED}
+
+ IntOp $R5 $R4 | ${SF_SELECTED}
+ SectionSetFlags $R1 $R5
+ MessageBox MB_OK '"$R3" has been selected, because "$R2" depends on it'
+
+ ${EndIf}
+
+ Pop $R5
+ Pop $R4
+ Pop $R0
+ Pop $R3
+ Pop $R2
+ Pop $R1
+FunctionEnd
+
+!macro CheckSectionDependency secA secB nameA nameB
+ Push "${secA}"
+ Push "${secB}"
+ Push "${nameA}"
+ Push "${nameB}"
+ Call CheckSectionDependency
+!macroend
+
+!define CheckSectionDependency "!insertmacro CheckSectionDependency"
+
+Function .onSelChange
+ !include "..\..\..\filelists\addon_dependencies.nsh"
+FunctionEnd
+
+;--------------------------------
+;Modern UI Configuration
+
+; Note: this must be placed after the sections, because below we need to check at compile time
+; if sections exist (by !ifdef <section_index_var>) to decide if the license page must be included.
+; The section index variables are only defined after the section definitions.
+
+ !define MUI_ICON "${COQ_ICON}"
+
+ !insertmacro MUI_PAGE_WELCOME
+ !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
+ !insertmacro MUI_PAGE_COMPONENTS
+
+ !ifdef Sec_compcert
+ !define LicCompCert_Title "CompCert License Agreement"
+ !define LicCompCert_SubTitle "You selected the CompCert addon. CompCert is not open source. Please review the license terms before installing CompCert!"
+ !define LicCompCert_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the CompCert addon."
+ !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/compcert/LICENSE" "${LicCompCert_Title}" "${LicCompCert_SubTitle}" "${LicCompCert_Bottom}" SelFuncCompCert
+
+ Function SelFuncCompCert
+ ${Unless} ${SectionIsSelected} ${Sec_compcert}
+ Abort
+ ${EndUnless}
+ FunctionEnd
+ !endif
+
+ !ifdef Sec_vst
+ !define LicVST_Title "Princeton VST License Agreement"
+ !define LicVST_SubTitle "You selected the VST addon. VST contains parts of CompCert which are not open source. Please review the license terms before installing VST!"
+ !define LicVST_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the VST addon."
+ !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/VST/LICENSE" "${LicVST_Title}" "${LicVST_SubTitle}" "${LicVST_Bottom}" SelFuncVST
+
+ Function SelFuncVST
+ ${Unless} ${SectionIsSelected} ${Sec_vst}
+ Abort
+ ${EndUnless}
+ FunctionEnd
+ !endif
+
+ !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces."
+ !insertmacro MUI_PAGE_DIRECTORY
+ !insertmacro MUI_PAGE_INSTFILES
+ !insertmacro MUI_PAGE_FINISH
+
+ !insertmacro MUI_UNPAGE_WELCOME
+ !insertmacro MUI_UNPAGE_CONFIRM
+ !insertmacro MUI_UNPAGE_INSTFILES
+ !insertmacro MUI_UNPAGE_FINISH
+
+;--------------------------------
+;Languages
+
+ !insertmacro MUI_LANGUAGE "English"
+
+;--------------------------------
+;Language Strings
+
+ ;Description
+ LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
+ LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
+ LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
+ ; LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
+ ; LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
+ !include "..\..\..\filelists\addon_strings.nsh"
+
+;--------------------------------
;Descriptions
!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
@@ -187,8 +286,9 @@ SectionEnd
!insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
+ !include "..\..\..\filelists\addon_descriptions.nsh"
!insertmacro MUI_FUNCTION_DESCRIPTION_END
-
+
;--------------------------------
;Uninstaller Section
@@ -214,7 +314,7 @@ Section "Uninstall"
Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
Delete "$INSTDIR\Uninstall.exe"
-
+
; Registry keys
DeleteRegKey HKCU "Software\${MY_PRODUCT}"
DeleteRegKey HKLM "SOFTWARE\Coq"
diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
new file mode 100755
index 0000000000..1afa6e7f95
--- /dev/null
+++ b/dev/build/windows/patches_coq/quickchick.patch
@@ -0,0 +1,26 @@
+diff/patch file created on Mon, Aug 27, 2018 9:21:52 AM with:
+difftar-folder.sh tarballs/quickchick-v1.0.2.tar.gz quickchick-v1.0.2 1
+TARFILE= tarballs/quickchick-v1.0.2.tar.gz
+FOLDER= quickchick-v1.0.2
+TARSTRIP= 1
+TARPREFIX= QuickChick-1.0.2/
+ORIGFOLDER= quickchick-v1.0.2.orig
+--- quickchick-v1.0.2.orig/Makefile 2018-08-22 18:21:39.000000000 +0200
++++ quickchick-v1.0.2/Makefile 2018-08-27 09:21:04.710461100 +0200
+@@ -2,7 +2,7 @@
+ .PHONY: plugin install install-plugin clean quickChickTool
+
+ QCTOOL_DIR=quickChickTool
+-QCTOOL_EXE=quickChickTool.byte
++QCTOOL_EXE=quickChickTool.native
+ QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \
+ $(QCTOOL_DIR)/quickChickToolTypes.ml \
+ $(QCTOOL_DIR)/quickChickToolLexer.mll \
+@@ -32,7 +32,7 @@
+ install: all
+ $(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE)
+ # Manually copying the remaining files
+- $(V)cp $(QCTOOL_EXE) $(shell opam config var bin)/quickChick
++ $(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick"
+ # $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
+ # $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8620b01b26..1b1aeafa0d 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -92,8 +92,15 @@
########################################################################
# Coquelicot
########################################################################
-: "${Coquelicot_CI_REF:=master}"
+# The URL for downloading a tgz snapshot of the master branch is
+# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz
+# See https://gforge.inria.fr/scm/browser.php?group_id=3599
+# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently,
+# we use a fixed version, which has a download path which does fit to our standard mechanism.
+# ATTENTION: The archive URL might depend on the version!
+: "${Coquelicot_CI_REF:=coquelicot-3.0.2}"
: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
+: "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}"
########################################################################
# CompCert
@@ -228,8 +235,22 @@
: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
########################################################################
-# quickchick
+# plugin_tutorial
########################################################################
: "${plugin_tutorial_CI_REF:=master}"
: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
+
+########################################################################
+# menhirlib
+########################################################################
+: "${menhirlib_CI_REF:=master}"
+: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}"
+: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
+
+########################################################################
+# aac-tactics
+########################################################################
+: "${aactactis_CI_REF:=master}"
+: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
+: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}"
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 09e9762261..deda42e2b7 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -43,9 +43,23 @@ if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -addon="bignums ltac2 equations" -make=N ^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
+ -addon=mathcomp ^
+ -addon=menhir ^
+ -addon=menhirlib ^
+ -addon=compcert ^
+ -addon=extlib ^
+ -addon=quickchick ^
+ -addon=coquelicot ^
+ -make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+REM addons with build issues
+REM -addon=vst ^
+REM -addon=aactactics ^
ECHO "Start Artifact Creation"
TIME /T
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 44857ed050..1a8a816aaa 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -2,7 +2,7 @@
; Add custom flags here. Default developer profile is `dev`
(env
- (dev (flags :standard -rectypes -w -9-27-50))
+ (dev (flags :standard -rectypes -w -9-27-50+60))
(release (flags :standard -rectypes)))
(context (opam (switch 4.05.0)))
diff --git a/engine/termops.mli b/engine/termops.mli
index aa0f837938..0e5d564d3f 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -341,10 +341,10 @@ val print_constr : constr -> Pp.t
end
val print_constr : constr -> Pp.t
-[@@deprecated "use Internal.print_constr_env"]
+[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"]
val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
-[@@deprecated "use Internal.print_constr_env"]
+[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"]
val print_rel_context : env -> Pp.t
-[@@deprecated "use Internal.print_rel_context"]
+[@@deprecated "This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead"]
diff --git a/library/decls.ml b/library/decls.ml
index 12c820fb7d..b766b6e2cb 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,13 +11,10 @@
(** This module registers tables for some non-logical informations
associated declarations *)
-open Util
open Names
open Decl_kinds
open Libnames
-module NamedDecl = Context.Named.Declaration
-
(** Datas associated to section variables and local definitions *)
type variable_data =
@@ -47,22 +44,3 @@ let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
let constant_kind kn = Cmap.find kn !csttab
-
-(** Miscellaneous functions. *)
-
-let initialize_named_context_for_proof () =
- let sign = Global.named_context () in
- List.fold_right
- (fun d signv ->
- let id = NamedDecl.get_id d in
- let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
- Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-
-let last_section_hyps dir =
- Context.Named.fold_outside
- (fun d sec_ids ->
- let id = NamedDecl.get_id d in
- try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
- with Not_found -> sec_ids)
- (Environ.named_context (Global.env()))
- ~init:[]
diff --git a/library/decls.mli b/library/decls.mli
index d9fc291518..401884736e 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -34,12 +34,3 @@ val variable_exists : variable -> bool
val add_constant_kind : Constant.t -> logical_kind -> unit
val constant_kind : Constant.t -> logical_kind
-
-(* Prepare global named context for proof session: remove proofs of
- opaque section definitions and remove vm-compiled code *)
-
-val initialize_named_context_for_proof : unit -> Environ.named_context_val
-
-(** Miscellaneous functions *)
-
-val last_section_hyps : DirPath.t -> Id.t list
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 55d9838bbb..67c5643459 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -11,7 +11,6 @@
(*i*)
open Names
open Globnames
-open Decl_kinds
open Term
open Constr
open Vars
@@ -482,19 +481,6 @@ let instances r =
let is_class gr =
GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
-let is_instance = function
- | ConstRef c ->
- (match Decls.constant_kind c with
- | IsDefinition Instance -> true
- | _ -> false)
- | VarRef v ->
- (match Decls.variable_kind v with
- | IsDefinition Instance -> true
- | _ -> false)
- | ConstructRef (ind,_) ->
- is_class (IndRef ind)
- | _ -> false
-
(* To embed a boolean for resolvability status.
This is essentially a hack to mark which evars correspond to
goals and do not need to be resolved when we have nested [resolve_all_evars]
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 80c6d82397..f0437be4ed 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -79,13 +79,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
(** Just return None if not a class *)
val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
-
+
val instance_impl : instance -> GlobRef.t
val hint_priority : instance -> int option
val is_class : GlobRef.t -> bool
-val is_instance : GlobRef.t -> bool
(** Returns the term and type for the given instance of the parameters and fields
of the type class. *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 880a11becd..aa9bd20bf3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -344,6 +344,14 @@ let universe_proof_terminator compute_guard hook =
let standard_proof_terminator compute_guard hook =
universe_proof_terminator compute_guard (fun _ -> hook)
+let initialize_named_context_for_proof () =
+ let sign = Global.named_context () in
+ List.fold_right
+ (fun d signv ->
+ let id = NamedDecl.get_id d in
+ let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
+ Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
+
let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
let terminator = match terminator with
| None -> standard_proof_terminator compute_guard hook
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index c9e4876ee3..38683ed6b2 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -56,6 +56,11 @@ val standard_proof_terminator :
val fresh_name_for_anonymous_theorem : unit -> Id.t
+(* Prepare global named context for proof session: remove proofs of
+ opaque section definitions and remove vm-compiled code *)
+
+val initialize_named_context_for_proof : unit -> Environ.named_context_val
+
(** {6 ... } *)
(** A hook the next three functions pass to cook_proof *)
@@ -63,7 +68,6 @@ val set_save_hook : (Proof.t -> unit) -> unit
val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-
(** [get_current_context ()] returns the evar context and env of the
current open proof if any, otherwise returns the empty evar context
and the current global env *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 3987e53bc7..c4a10b4be6 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1102,7 +1102,7 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
- let sign = Decls.initialize_named_context_for_proof () in
+ let sign = Lemmas.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
@@ -1122,7 +1122,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
- let sign = Decls.initialize_named_context_for_proof () in
+ let sign = Lemmas.initialize_named_context_for_proof () in
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:53:12 +0000