aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore3
-rw-r--r--INSTALL.md13
-rw-r--r--Makefile2
-rw-r--r--ci/manifest-sources-8.111
-rw-r--r--examples/Example.v2
-rw-r--r--src/Makefile801
-rw-r--r--src/Makefile.local4
-rw-r--r--src/PropToBool.v4
-rw-r--r--src/State.v2
-rw-r--r--src/_CoqProject2
-rwxr-xr-xsrc/configure.sh4
-rw-r--r--src/trace/coqInterface.ml43
-rw-r--r--src/trace/coqInterface.mli6
13 files changed, 45 insertions, 842 deletions
diff --git a/.gitignore b/.gitignore
index 0f92c0b..1c3eaea 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,11 +17,14 @@ setup.log
*.v.d
*.aux
*.vo
+*.vok
+*.vos
*.d
.lia.cache
.nia.cache
# targets of coq_makefile:
+src/Makefile
src/Makefile.conf
src/g_smtcoq.ml
diff --git a/INSTALL.md b/INSTALL.md
index 2b83320..0667a05 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -73,7 +73,7 @@ Then follow the instructions of the previous section.
### Requirements
-You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*.
+You need to have OCaml version >= 4.09.0 and Coq version 8.11.*.
> **Warning**: The version of Coq that you plan to use must have been compiled
> with the same version of OCaml that you are going to use to compile
@@ -103,24 +103,24 @@ eval `opam config env`
### Install OCaml
-Now you can install an OCaml compiler (we recommend 4.09.0):
+Now you can install an OCaml compiler (we recommend 4.10.0):
```bash
-opam switch create ocaml-base-compiler.4.09.0
+opam switch create ocaml-base-compiler.4.10.0
```
### Install Coq
-After OCaml is installed, you can install Coq-8.10.2 through opam.
+After OCaml is installed, you can install Coq-8.11.2 through opam.
```bash
-opam install coq.8.10.2
+opam install coq.8.11.2
```
If you also want to install CoqIDE at the same time you can do
```bash
-opam install coq.8.10.2 coqide.8.10.2
+opam install coq.8.11.2 coqide.8.11.2
```
but you might need to install some extra packages and libraries for your system
@@ -132,6 +132,7 @@ but you might need to install some extra packages and libraries for your system
Compile and install SMTCoq by using the following commands in the src directory.
```bash
+./configure.sh
make
make install
```
diff --git a/Makefile b/Makefile
index c31aa9b..5e3b013 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
all:
- cd src && $(MAKE)
+ cd src && ./configure.sh && $(MAKE)
install: all
cd src && $(MAKE) install
diff --git a/ci/manifest-sources-8.11 b/ci/manifest-sources-8.11
index 043c626..b93f959 100644
--- a/ci/manifest-sources-8.11
+++ b/ci/manifest-sources-8.11
@@ -27,6 +27,7 @@ tasks:
cd smtcoq
git checkout coq-8.11
cd src
+ ./configure.sh
make
make install
cd ../..
diff --git a/examples/Example.v b/examples/Example.v
index 06d5aba..b949740 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -11,7 +11,7 @@
(* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library.
- If you are using native-coq instead of Coq 8.10, replace it with:
+ If you are using native-coq instead of Coq 8.11, replace it with:
Require Import SMTCoq.
*)
diff --git a/src/Makefile b/src/Makefile
deleted file mode 100644
index 5d24b0c..0000000
--- a/src/Makefile
+++ /dev/null
@@ -1,801 +0,0 @@
-###############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # ##
-###############################################################################
-## GNUMakefile for Coq 8.10.2
-
-# For debugging purposes (must stay here, don't move below)
-INITIAL_VARS := $(.VARIABLES)
-# To implement recursion we save the name of the main Makefile
-SELF := $(lastword $(MAKEFILE_LIST))
-PARENT := $(firstword $(MAKEFILE_LIST))
-
-# This file is generated by coq_makefile and contains many variable
-# definitions, like the list of .v files or the path to Coq
-include Makefile.conf
-
-# Put in place old names
-VFILES := $(COQMF_VFILES)
-MLIFILES := $(COQMF_MLIFILES)
-MLFILES := $(COQMF_MLFILES)
-MLGFILES := $(COQMF_MLGFILES)
-MLPACKFILES := $(COQMF_MLPACKFILES)
-MLLIBFILES := $(COQMF_MLLIBFILES)
-CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES)
-INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
-OTHERFLAGS := $(COQMF_OTHERFLAGS)
-COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS)
-OCAMLLIBS := $(COQMF_OCAMLLIBS)
-SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS)
-COQLIBS := $(COQMF_COQLIBS)
-COQLIBS_NOML := $(COQMF_COQLIBS_NOML)
-CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS)
-LOCAL := $(COQMF_LOCAL)
-COQLIB := $(COQMF_COQLIB)
-DOCDIR := $(COQMF_DOCDIR)
-OCAMLFIND := $(COQMF_OCAMLFIND)
-CAMLFLAGS := $(COQMF_CAMLFLAGS)
-HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
-OCAMLWARN := $(COQMF_WARN)
-
-Makefile.conf: _CoqProject
- coq_makefile -f _CoqProject -o Makefile
-
-# This file can be created by the user to hook into double colon rules or
-# add any other Makefile code he may need
--include Makefile.local
-
-# Parameters ##################################################################
-#
-# Parameters are make variable assignments.
-# They can be passed to (each call to) make on the command line.
-# They can also be put in Makefile.local once an for all.
-# For retro-compatibility reasons they can be put in the _CoqProject, but this
-# practice is discouraged since _CoqProject better not contain make specific
-# code (be nice to user interfaces).
-
-# Print shell commands (set to non empty)
-VERBOSE ?=
-
-# Time the Coq process (set to non empty), and how (see default value)
-TIMED?=
-TIMECMD?=
-# Use command time on linux, gtime on Mac OS
-TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
-ifneq (,$(TIMED))
-ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
-STDTIME?=command time -f $(TIMEFMT)
-else
-ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
-STDTIME?=gtime -f $(TIMEFMT)
-else
-STDTIME?=command time
-endif
-endif
-else
-STDTIME?=command time -f $(TIMEFMT)
-endif
-
-# Coq binaries
-COQC ?= "$(COQBIN)coqc"
-COQTOP ?= "$(COQBIN)coqtop"
-COQCHK ?= "$(COQBIN)coqchk"
-COQDEP ?= "$(COQBIN)coqdep"
-COQDOC ?= "$(COQBIN)coqdoc"
-COQPP ?= "$(COQBIN)coqpp"
-COQMKFILE ?= "$(COQBIN)coq_makefile"
-
-# Timing scripts
-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
-BEFORE ?=
-AFTER ?=
-
-# FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=unix,str
-
-# OCaml binaries
-CAMLC ?= "$(OCAMLFIND)" ocamlc -c
-CAMLOPTC ?= "$(OCAMLFIND)" opt -c
-CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLDOC ?= "$(OCAMLFIND)" ocamldoc
-CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack
-
-# DESTDIR is prepended to all installation paths
-DESTDIR ?=
-
-# Debug builds, typically -g to OCaml, -debug to Coq.
-CAMLDEBUG ?=
-COQDEBUG ?=
-
-# Extra packages to be linked in (as in findlib -package)
-CAMLPKGS ?=
-
-# Option for making timing files
-TIMING?=
-# Option for changing sorting of timing output file
-TIMING_SORT_BY ?= auto
-# Output file names for timed builds
-TIME_OF_BUILD_FILE ?= time-of-build.log
-TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log
-TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log
-TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log
-TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log
-TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
-
-TGTS ?=
-
-########## End of parameters ##################################################
-# What follows may be relevant to you only if you need to
-# extend this Makefile. If so, look for 'Extension point' here and
-# put in Makefile.local double colon rules accordingly.
-# E.g. to perform some work after the all target completes you can write
-#
-# post-all::
-# echo "All done!"
-#
-# in Makefile.local
-#
-###############################################################################
-
-
-
-
-# Flags #######################################################################
-#
-# We define a bunch of variables combining the parameters.
-# To add additional flags to coq, coqchk or coqdoc, set the
-# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
-# To overwrite the default choice and set your own flags entirely, set the
-# {COQ,COQCHK,COQDOC}FLAGS variable.
-
-SHOW := $(if $(VERBOSE),@true "",@echo "")
-HIDE := $(if $(VERBOSE),,@)
-
-TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
-
-OPT?=
-
-# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
-ifeq '$(OPT)' '-byte'
-USEBYTE:=true
-DYNOBJ:=.cma
-DYNLIB:=.cma
-else
-USEBYTE:=
-DYNOBJ:=.cmxs
-DYNLIB:=.cmxs
-endif
-
-# these variables are meant to be overridden if you want to add *extra* flags
-COQEXTRAFLAGS?=
-COQCHKEXTRAFLAGS?=
-COQDOCEXTRAFLAGS?=
-
-# these flags do NOT contain the libraries, to make them easier to overwrite
-COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)
-COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
-COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
-
-COQDOCLIBS?=$(COQLIBS_NOML)
-
-# The version of Coq being run and the version of coq_makefile that
-# generated this makefile
-COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.10.2
-
-COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
-
-CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
-# ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
-CAMLFLAGS+=$(OCAMLWARN)
-
-ifneq (,$(TIMING))
-TIMING_ARG=-time
-ifeq (after,$(TIMING))
-TIMING_EXT=after-timing
-else
-ifeq (before,$(TIMING))
-TIMING_EXT=before-timing
-else
-TIMING_EXT=timing
-endif
-endif
-else
-TIMING_ARG=
-endif
-
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
-
-# Files #######################################################################
-#
-# We here define a bunch of variables about the files being part of the
-# Coq project in order to ease the writing of build target and build rules
-
-VDFILE := .coqdeps
-
-ALLSRCFILES := \
- $(MLGFILES) \
- $(MLFILES) \
- $(MLPACKFILES) \
- $(MLLIBFILES) \
- $(MLIFILES)
-
-# helpers
-vo_to_obj = $(addsuffix .o,\
- $(filter-out Warning: Error:,\
- $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
-strip_dotslash = $(patsubst ./%,%,$(1))
-
-# without this we get undefined variables in the expansion for the
-# targets of the [deprecated,use-mllib-or-mlpack] rule
-with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1)))
-
-VO = vo
-
-VOFILES = $(VFILES:.v=.$(VO))
-GLOBFILES = $(VFILES:.v=.glob)
-HTMLFILES = $(VFILES:.v=.html)
-GHTMLFILES = $(VFILES:.v=.g.html)
-BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
-TEXFILES = $(VFILES:.v=.tex)
-GTEXFILES = $(VFILES:.v=.g.tex)
-CMOFILES = \
- $(MLGFILES:.mlg=.cmo) \
- $(MLFILES:.ml=.cmo) \
- $(MLPACKFILES:.mlpack=.cmo)
-CMXFILES = $(CMOFILES:.cmo=.cmx)
-OFILES = $(CMXFILES:.cmx=.o)
-CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma)
-CMXAFILES = $(CMAFILES:.cma=.cmxa)
-CMIFILES = \
- $(CMOFILES:.cmo=.cmi) \
- $(MLIFILES:.mli=.cmi)
-# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
-# a .ml4 file
-CMXSFILES = \
- $(MLPACKFILES:.mlpack=.cmxs) \
- $(CMXAFILES:.cmxa=.cmxs) \
- $(if $(MLPACKFILES)$(CMXAFILES),,\
- $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
-
-# files that are packed into a plugin (no extension)
-PACKEDFILES = \
- $(call strip_dotslash, \
- $(foreach lib, \
- $(call strip_dotslash, \
- $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib))))
-# files that are archived into a .cma (mllib)
-LIBEDFILES = \
- $(call strip_dotslash, \
- $(foreach lib, \
- $(call strip_dotslash, \
- $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib))))
-CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
-CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
-OBJFILES = $(call vo_to_obj,$(VOFILES))
-ALLNATIVEFILES = \
- $(OBJFILES:.o=.cmi) \
- $(OBJFILES:.o=.cmx) \
- $(OBJFILES:.o=.cmxs)
-# trick: wildcard filters out non-existing files, so that `install` doesn't show
-# warnings and `clean` doesn't pass to rm a list of files that is too long for
-# the shell.
-NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
-FILESTOINSTALL = \
- $(VOFILES) \
- $(VFILES) \
- $(GLOBFILES) \
- $(NATIVEFILES) \
- $(CMIFILESTOINSTALL)
-BYTEFILESTOINSTALL = \
- $(CMOFILESTOINSTALL) \
- $(CMAFILES)
-ifeq '$(HASNATDYNLINK)' 'true'
-DO_NATDYNLINK = yes
-FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
-else
-DO_NATDYNLINK =
-endif
-
-ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE))
-
-# Compilation targets #########################################################
-
-all:
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
-.PHONY: all
-
-all.timing.diff:
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
-.PHONY: all.timing.diff
-
-make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
-make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
-make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
- $(HIDE)rm -f pretty-timed-success.ok
- $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
- $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
-print-pretty-timed::
- $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
-print-pretty-timed-diff::
- $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
-ifeq (,$(BEFORE))
-print-pretty-single-time-diff::
- @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
- $(HIDE)false
-else
-ifeq (,$(AFTER))
-print-pretty-single-time-diff::
- @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
- $(HIDE)false
-else
-print-pretty-single-time-diff::
- $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
-endif
-endif
-pretty-timed:
- $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
-.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
-
-# Extension points for actions to be performed before/after the all target
-pre-all::
- @# Extension point
- $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
- echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
- echo "W: while the current Coq version is $(COQ_VERSION)";\
- fi
-.PHONY: pre-all
-
-post-all::
- @# Extension point
-.PHONY: post-all
-
-real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
-.PHONY: real-all
-
-real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
-.PHONY: real-all.timing.diff
-
-bytefiles: $(CMOFILES) $(CMAFILES)
-.PHONY: bytefiles
-
-optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
-.PHONY: optfiles
-
-# FIXME, see Ralf's bugreport
-quick: $(VOFILES:.vo=.vio)
-.PHONY: quick
-
-vio2vo:
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
- -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: vio2vo
-
-quick2vo:
- $(HIDE)make -j $(J) quick
- $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
- viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
- if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
- done); \
- echo "VIO2VO: $$VIOFILES"; \
- if [ -n "$$VIOFILES" ]; then \
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
- fi
-.PHONY: quick2vo
-
-checkproofs:
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
- -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: checkproofs
-
-validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
-.PHONY: validate
-
-only: $(TGTS)
-.PHONY: only
-
-# Documentation targets #######################################################
-
-html: $(GLOBFILES) $(VFILES)
- $(SHOW)'COQDOC -d html $(GAL)'
- $(HIDE)mkdir -p html
- $(HIDE)$(COQDOC) \
- -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
-
-mlihtml: $(MLIFILES:.mli=.cmi)
- $(SHOW)'CAMLDOC -d $@'
- $(HIDE)mkdir $@ || rm -rf $@/*
- $(HIDE)$(CAMLDOC) -html \
- -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
-
-all-mli.tex: $(MLIFILES:.mli=.cmi)
- $(SHOW)'CAMLDOC -latex $@'
- $(HIDE)$(CAMLDOC) -latex \
- -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
-
-all.ps: $(VFILES)
- $(SHOW)'COQDOC -ps $(GAL)'
- $(HIDE)$(COQDOC) \
- -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
- -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all.pdf: $(VFILES)
- $(SHOW)'COQDOC -pdf $(GAL)'
- $(HIDE)$(COQDOC) \
- -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
- -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-# FIXME: not quite right, since the output name is different
-gallinahtml: GAL=-g
-gallinahtml: html
-
-all-gal.ps: GAL=-g
-all-gal.ps: all.ps
-
-all-gal.pdf: GAL=-g
-all-gal.pdf: all.pdf
-
-# ?
-beautify: $(BEAUTYFILES)
- for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
- @echo 'Do not do "make clean" until you are sure that everything went well!'
- @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-.PHONY: beautify
-
-# Installation targets ########################################################
-#
-# There rules can be extended in Makefile.local
-# Extensions can't assume when they run.
-
-install:
- $(HIDE)code=0; for f in $(FILESTOINSTALL); do\
- if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
- done; exit $$code
- $(HIDE)for f in $(FILESTOINSTALL); do\
- df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
- if [ "$$?" != "0" -o -z "$$df" ]; then\
- echo SKIP "$$f" since it has no logical path;\
- else\
- install -d "$(COQLIBINSTALL)/$$df" &&\
- install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
- echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
- fi;\
- done
- $(HIDE)$(MAKE) install-extra -f "$(SELF)"
-install-extra::
- @# Extension point
-.PHONY: install install-extra
-
-install-byte:
- $(HIDE)for f in $(BYTEFILESTOINSTALL); do\
- df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
- if [ "$$?" != "0" -o -z "$$df" ]; then\
- echo SKIP "$$f" since it has no logical path;\
- else\
- install -d "$(COQLIBINSTALL)/$$df" &&\
- install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
- echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
- fi;\
- done
-
-install-doc:: html mlihtml
- @# Extension point
- $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
- $(HIDE)for i in html/*; do \
- dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
- install -m 0644 "$$i" "$$dest";\
- echo INSTALL "$$i" "$$dest";\
- done
- $(HIDE)install -d \
- "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
- $(HIDE)for i in mlihtml/*; do \
- dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
- install -m 0644 "$$i" "$$dest";\
- echo INSTALL "$$i" "$$dest";\
- done
-.PHONY: install-doc
-
-uninstall::
- @# Extension point
- $(HIDE)for f in $(FILESTOINSTALL); do \
- df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
- instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
- rm -f "$$instf" &&\
- echo RM "$$instf" &&\
- (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
- done
-.PHONY: uninstall
-
-uninstall-doc::
- @# Extension point
- $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
- $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
- $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
- $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
- $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
-.PHONY: uninstall-doc
-
-# Cleaning ####################################################################
-#
-# There rules can be extended in Makefile.local
-# Extensions can't assume when they run.
-
-clean::
- @# Extension point
- $(SHOW)'CLEAN'
- $(HIDE)rm -f $(CMOFILES)
- $(HIDE)rm -f $(CMIFILES)
- $(HIDE)rm -f $(CMAFILES)
- $(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
- $(HIDE)rm -f $(CMXAFILES)
- $(HIDE)rm -f $(CMXSFILES)
- $(HIDE)rm -f $(CMOFILES:.cmo=.o)
- $(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
- $(HIDE)rm -f $(MLGFILES:.mlg=.ml)
- $(HIDE)rm -f $(ALLDFILES)
- $(HIDE)rm -f $(NATIVEFILES)
- $(HIDE)find . -name .coq-native -type d -empty -delete
- $(HIDE)rm -f $(VOFILES)
- $(HIDE)rm -f $(VOFILES:.vo=.vio)
- $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
- $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
- $(HIDE)rm -f $(VFILES:.v=.glob)
- $(HIDE)rm -f $(VFILES:.v=.tex)
- $(HIDE)rm -f $(VFILES:.v=.g.tex)
- $(HIDE)rm -f pretty-timed-success.ok
- $(HIDE)rm -rf html mlihtml
-.PHONY: clean
-
-cleanall:: clean
- @# Extension point
- $(SHOW)'CLEAN *.aux *.timing'
- $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
- $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
- $(HIDE)rm -f $(VOFILES:.vo=.v.timing)
- $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
- $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
- $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
-.PHONY: cleanall
-
-archclean::
- @# Extension point
- $(SHOW)'CLEAN *.cmx *.o'
- $(HIDE)rm -f $(NATIVEFILES)
- $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
-.PHONY: archclean
-
-
-# Compilation rules ###########################################################
-
-$(MLIFILES:.mli=.cmi): %.cmi: %.mli
- $(SHOW)'CAMLC -c $<'
- $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
-
-$(MLGFILES:.mlg=.ml): %.ml: %.mlg
- $(SHOW)'COQPP $<'
- $(HIDE)$(COQPP) $<
-
-# Stupid hack around a deficient syntax: we cannot concatenate two expansions
-$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
- $(SHOW)'CAMLC -c $<'
- $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
-
-# Same hack
-$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
- $(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
- $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
-
-
-$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
- $(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
- -linkall -shared -o $@ $<
-
-$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
- $(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-
-$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
- $(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-
-
-$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
- $(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
- -shared -linkall -o $@ $<
-
-$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
- $(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
-
-$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
- $(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-
-$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
- $(SHOW)'CAMLC -pack -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
-
-$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
- $(SHOW)'CAMLOPT -pack -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
-
-# This rule is for _CoqProject with no .mllib nor .mlpack
-$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
- $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
- -shared -o $@ $<
-
-ifneq (,$(TIMING))
-TIMING_EXTRA = > $<.$(TIMING_EXT)
-else
-TIMING_EXTRA =
-endif
-
-$(VOFILES): %.vo: %.v
- $(SHOW)COQC $<
- $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
-
-# FIXME ?merge with .vo / .vio ?
-$(GLOBFILES): %.glob: %.v
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
-$(VFILES:.v=.vio): %.vio: %.v
- $(SHOW)COQC -quick $<
- $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
-$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
- $(SHOW)PYTHON TIMING-DIFF $<
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
-
-$(BEAUTYFILES): %.v.beautified: %.v
- $(SHOW)'BEAUTIFY $<'
- $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
-
-$(TEXFILES): %.tex: %.v
- $(SHOW)'COQDOC -latex $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-$(GTEXFILES): %.g.tex: %.v
- $(SHOW)'COQDOC -latex -g $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-$(HTMLFILES): %.html: %.v %.glob
- $(SHOW)'COQDOC -html $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-$(GHTMLFILES): %.g.html: %.v %.glob
- $(SHOW)'COQDOC -html -g $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
-
-# Dependency files ############################################################
-
-ifndef MAKECMDGOALS
- -include $(ALLDFILES)
-else
- ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
- -include $(ALLDFILES)
- endif
-endif
-
-.SECONDARY: $(ALLDFILES)
-
-redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
-
-GENMLFILES:=$(MLGFILES:.mlg=.ml)
-$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES)
-
-$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
- $(SHOW)'CAMLDEP $<'
- $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml
- $(SHOW)'CAMLDEP $<'
- $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
- $(SHOW)'CAMLDEP $<'
- $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
- $(SHOW)'COQDEP $<'
- $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
- $(SHOW)'COQDEP $<'
- $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
-
-# If this makefile is created using a _CoqProject we have coqdep get
-# options from it. This avoids argument length limits for pathological
-# projects. Note that extra options might be on the command line.
-VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
-
-$(VDFILE).d: $(VFILES)
- $(SHOW)'COQDEP VFILES'
- $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
-
-# Misc ########################################################################
-
-byte:
- $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
-.PHONY: byte
-
-opt:
- $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
-.PHONY: opt
-
-# This is deprecated. To extend this makefile use
-# extension points and Makefile.local
-printenv::
- $(warning printenv is deprecated)
- $(warning write extensions in Makefile.local or include Makefile.conf)
- @echo 'LOCAL = $(LOCAL)'
- @echo 'COQLIB = $(COQLIB)'
- @echo 'DOCDIR = $(DOCDIR)'
- @echo 'OCAMLFIND = $(OCAMLFIND)'
- @echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
- @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
- @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
- @echo 'OCAMLFIND = $(OCAMLFIND)'
- @echo 'PP = $(PP)'
- @echo 'COQFLAGS = $(COQFLAGS)'
- @echo 'COQLIB = $(COQLIBS)'
- @echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
- @echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
-.PHONY: printenv
-
-# Generate a .merlin file. If you need to append directives to this
-# file you can extend the merlin-hook target in Makefile.local
-.merlin:
- $(SHOW)'FILL .merlin'
- $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
- $(HIDE)echo 'B $(COQLIB)' >> .merlin
- $(HIDE)echo 'S $(COQLIB)' >> .merlin
- $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
- echo 'B $(COQLIB)$(d)' >> .merlin;)
- $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
- echo 'S $(COQLIB)$(d)' >> .merlin;)
- $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
- $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
- $(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
-.PHONY: merlin
-
-merlin-hook::
- @# Extension point
-.PHONY: merlin-hook
-
-# prints all variables
-debug:
- $(foreach v,\
- $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
- $(.VARIABLES))),\
- $(info $(v) = $($(v))))
-.PHONY: debug
-
-.DEFAULT_GOAL := all
-
-# Local Variables:
-# mode: makefile-gmake
-# End:
diff --git a/src/Makefile.local b/src/Makefile.local
index 8abc72c..c57842a 100644
--- a/src/Makefile.local
+++ b/src/Makefile.local
@@ -25,6 +25,10 @@ clean::
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
+CAMLPKGS += -package num
+
+merlin-hook::
+ $(HIDE)echo 'PKG num' >> .merlin
%.ml : %.mll
$(CAMLLEX) $<
diff --git a/src/PropToBool.v b/src/PropToBool.v
index 6f7c5ca..31f8b2d 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -243,7 +243,7 @@ Ltac prop2bool_hyps Hs :=
Section Test.
Variable A : Type.
- Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
+ Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = (length l1 + length l2)%nat.
Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
Hypothesis uninterpreted_type : forall (a:A), a = a.
Hypothesis bool_eq : forall (b:bool), negb (negb b) = b.
@@ -318,7 +318,7 @@ End MultipleCompDec.
polymorphism will be removed before *)
Section Poly.
Hypothesis basic : forall (A:Type) (l1 l2:list A),
- length (l1++l2) = length l1 + length l2.
+ length (l1++l2) = (length l1 + length l2)%nat.
Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
Goal True.
diff --git a/src/State.v b/src/State.v
index dca62e3..16868b7 100644
--- a/src/State.v
+++ b/src/State.v
@@ -10,7 +10,7 @@
(**************************************************************************)
-Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc.
+Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc Ring.
(* Require Import AxiomesInt. *)
diff --git a/src/_CoqProject b/src/_CoqProject
index 2a883c8..9ac5799 100644
--- a/src/_CoqProject
+++ b/src/_CoqProject
@@ -9,6 +9,8 @@
########################################################################
## To generate the Makefile: ##
## coq_makefile -f Make -o Makefile ##
+## sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile ##
+## WARNING: DO NOT FORGET THE SECOND LINE (see PR#62) ##
########################################################################
diff --git a/src/configure.sh b/src/configure.sh
new file mode 100755
index 0000000..7b0c264
--- /dev/null
+++ b/src/configure.sh
@@ -0,0 +1,4 @@
+#!/bin/sh
+
+coq_makefile -f _CoqProject -o Makefile
+sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml
index 81a22c9..5aa1087 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -10,9 +10,6 @@
(**************************************************************************)
-open Entries
-
-
(* Constr generation and manipulation *)
type id = Names.variable
let mkId = Names.Id.of_string
@@ -50,47 +47,39 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
let pr_constr = pr_constr_env Environ.empty_env
-let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c ->
+let mkUConst : Constr.t -> Evd.side_effects Declare.proof_entry = fun c ->
let env = Global.env () in
let evd = Evd.from_env env in
let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in
- { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
- const_entry_universes = Evd.univ_entry ~poly:false evd;
- const_entry_opaque = false;
- const_entry_inline_code = false }
+ Declare.definition_entry
+ ~opaque:false
+ ~inline:false
+ ~types:(EConstr.Unsafe.to_constr ty) (* Cannot contain evars since it comes from a Constr.t *)
+ ~univs:(Evd.univ_entry ~poly:false evd)
+ c
let mkTConst c noc ty =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in
- { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some ty;
- const_entry_universes = Evd.univ_entry ~poly:false evd;
- const_entry_opaque = false;
- const_entry_inline_code = false }
+ Declare.definition_entry
+ ~opaque:false
+ ~inline:false
+ ~types:ty
+ ~univs:(Evd.univ_entry ~poly:false evd)
+ c
(* TODO : Set -> Type *)
let declare_new_type t =
- let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
+ let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional Constr.mkSet [] Glob_term.Explicit (CAst.make t) in
Constr.mkVar t
let declare_new_variable v constr_t =
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
- let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
+ let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional constr_t [] Glob_term.Explicit (CAst.make v) in
Constr.mkVar v
let declare_constant n c =
- Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
-
+ Declare.declare_constant ~name:n ~kind:(Decls.IsDefinition Decls.Definition) (Declare.DefinitionEntry c)
type cast_kind = Constr.cast_kind
diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli
index 38d78d8..0b0914a 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -43,11 +43,11 @@ val mkArrow : types -> types -> constr
val pr_constr_env : Environ.env -> constr -> Pp.t
val pr_constr : constr -> Pp.t
-val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry
-val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry
+val mkUConst : constr -> Evd.side_effects Declare.proof_entry
+val mkTConst : constr -> constr -> types -> Evd.side_effects Declare.proof_entry
val declare_new_type : id -> types
val declare_new_variable : id -> types -> constr
-val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+val declare_constant : id -> Evd.side_effects Declare.proof_entry -> Names.Constant.t
type cast_kind
val vmcast : cast_kind
generated by cgit (git 2.34.1) at 2024-05-18 15:38:44 +0000