diff --git a/.gitignore b/.gitignore
index bc89608..1d0a03f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -23,3 +23,4 @@ plugin/Makefile
 plugin/.merlin
 *.out
 _opam
+src/plibrary.ml
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..c786ebd
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,828 @@
+###############################################################################
+##  v      #                   The Coq Proof Assistant                       ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                   ##
+##   \VV/  #                                                                 ##
+##    //   #                                                                 ##
+###############################################################################
+## GNUMakefile for Coq 8.11.1
+
+# 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
+
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+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.11.1
+
+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 := .Makefile.d
+
+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
+VOS = vos
+
+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 .mlg 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 is deprecated, now renamed vio
+vio: $(VOFILES:.vo=.vio)
+.PHONY: vio
+quick: vio
+	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
+.PHONY: quick
+
+vio2vo:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
+		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: vio2vo
+
+# quick2vo is undocumented
+quick2vo:
+	$(HIDE)make -j $(J) vio
+	$(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
+
+vos: $(VOFILES:%.vo=%.vos)
+.PHONY: vos
+
+vok: $(VOFILES:%.vo=%.vok)
+.PHONY: vok
+
+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 $(VOFILES:.vo=.vos)
+	$(HIDE)rm -f $(VOFILES:.vo=.vok)
+	$(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) -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 -vio $<
+	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+$(VFILES:.v=.vos): %.vos: %.v
+	$(SHOW)COQC -vos $<
+	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+$(VFILES:.v=.vok): %.vok: %.v
+	$(SHOW)COQC -vok $<
+	$(HIDE)$(TIMER) $(COQC) -vok $(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): $(VFILES)
+	$(SHOW)'COQDEP VFILES'
+	$(HIDE)$(COQDEP) -vos -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/Makefile.conf b/Makefile.conf
new file mode 100644
index 0000000..a41d6b4
--- /dev/null
+++ b/Makefile.conf
@@ -0,0 +1,54 @@
+# This configuration file was generated by running:
+# coq_makefile -f _CoqProject -o Makefile
+
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_VFILES = theories/Plib.v
+COQMF_MLIFILES = src/utilities/utilities.mli src/coq/termutils/apputils.mli src/coq/termutils/constutils.mli src/coq/termutils/funutils.mli src/coq/representationutils/defutils.mli src/coq/representationutils/nameutils.mli src/coq/logicutils/typesandequality/inference.mli src/coq/logicutils/typesandequality/convertibility.mli src/coq/logicutils/typesandequality/checking.mli src/coq/constants/equtils.mli src/coq/constants/sigmautils.mli src/coq/constants/produtils.mli src/coq/constants/idutils.mli src/coq/constants/proputils.mli src/coq/logicutils/contexts/stateutils.mli src/coq/logicutils/contexts/envutils.mli src/coq/logicutils/contexts/contextutils.mli src/coq/logicutils/hofs/hofs.mli src/coq/logicutils/hofs/hofimpls.mli src/coq/logicutils/hofs/debruijn.mli src/coq/logicutils/hofs/substitution.mli src/coq/logicutils/hofs/reducers.mli src/coq/logicutils/hofs/typehofs.mli src/coq/logicutils/hofs/zooming.mli src/coq/logicutils/hofs/hypotheses.mli src/coq/logicutils/hofs/filters.mli src/coq/logicutils/inductive/indexing.mli src/coq/logicutils/inductive/indutils.mli src/coq/logicutils/contexts/modutils.mli src/coq/logicutils/transformation/transform.mli src/coq/devutils/printing.mli src/coq/decompiler/decompiler.mli
+COQMF_MLFILES = src/utilities/utilities.ml src/coq/termutils/apputils.ml src/coq/termutils/constutils.ml src/coq/termutils/funutils.ml src/coq/representationutils/defutils.ml src/coq/representationutils/nameutils.ml src/coq/logicutils/typesandequality/inference.ml src/coq/logicutils/typesandequality/convertibility.ml src/coq/logicutils/typesandequality/checking.ml src/coq/constants/equtils.ml src/coq/constants/sigmautils.ml src/coq/constants/produtils.ml src/coq/constants/idutils.ml src/coq/constants/proputils.ml src/coq/logicutils/contexts/stateutils.ml src/coq/logicutils/contexts/envutils.ml src/coq/logicutils/contexts/contextutils.ml src/coq/logicutils/hofs/hofs.ml src/coq/logicutils/hofs/hofimpls.ml src/coq/logicutils/hofs/debruijn.ml src/coq/logicutils/hofs/substitution.ml src/coq/logicutils/hofs/reducers.ml src/coq/logicutils/hofs/typehofs.ml src/coq/logicutils/hofs/zooming.ml src/coq/logicutils/hofs/hypotheses.ml src/coq/logicutils/hofs/filters.ml src/coq/logicutils/inductive/indexing.ml src/coq/logicutils/inductive/indutils.ml src/coq/logicutils/contexts/modutils.ml src/coq/logicutils/transformation/transform.ml src/coq/devutils/printing.ml src/coq/decompiler/decompiler.ml
+COQMF_MLGFILES = src/plibrary.mlg
+COQMF_MLPACKFILES = src/plib.mlpack
+COQMF_MLLIBFILES = 
+COQMF_CMDLINE_VFILES = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = -I src/utilities -I src/coq -I src/coq/termutils -I src/coq/constants -I src/coq/logicutils -I src/coq/logicutils/contexts -I src/coq/logicutils/typesandequality -I src/coq/logicutils/hofs -I src/coq/logicutils/inductive -I src/coq/logicutils/transformation -I src/coq/devutils -I src/coq/representationutils -I src/coq/decompiler -I src
+COQMF_SRC_SUBDIRS = src/utilities src/coq src/coq/termutils src/coq/constants src/coq/logicutils src/coq/logicutils/contexts src/coq/logicutils/typesandequality src/coq/logicutils/hofs src/coq/logicutils/inductive src/coq/logicutils/transformation src/coq/devutils src/coq/representationutils src/coq/decompiler src
+COQMF_COQLIBS = -I src/utilities -I src/coq -I src/coq/termutils -I src/coq/constants -I src/coq/logicutils -I src/coq/logicutils/contexts -I src/coq/logicutils/typesandequality -I src/coq/logicutils/hofs -I src/coq/logicutils/inductive -I src/coq/logicutils/transformation -I src/coq/devutils -I src/coq/representationutils -I src/coq/decompiler -I src -Q theories Plibrary -R src Plibrary
+COQMF_COQLIBS_NOML = -Q theories Plibrary -R src Plibrary
+COQMF_CMDLINE_COQLIBS =   
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_LOCAL=0
+COQMF_COQLIB=/Users/max/.opam/default/lib/coq/
+COQMF_DOCDIR=/Users/max/.opam/default/doc/
+COQMF_OCAMLFIND=/Users/max/.opam/default/bin/ocamlfind
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence
+COQMF_WARN=-warn-error +a-3
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config lib clib kernel library engine pretyping interp gramlib gramlib/.pack parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = Plibrary
diff --git a/Makefile.local b/Makefile.local
new file mode 100644
index 0000000..b5dfc1e
--- /dev/null
+++ b/Makefile.local
@@ -0,0 +1 @@
+OCAMLWARN=-warn-error +a-3-8-40-32-28-33
diff --git a/_CoqProject b/_CoqProject
index 339b268..2edf0c1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -91,7 +91,7 @@ src/coq/devutils/printing.ml
 src/coq/decompiler/decompiler.mli
 src/coq/decompiler/decompiler.ml
 
-src/plibrary.ml4
+src/plibrary.mlg
 src/plib.mlpack
 
 theories/Plib.v
diff --git a/src/coq/constants/equtils.ml b/src/coq/constants/equtils.ml
index a1ed2a8..323c1a4 100644
--- a/src/coq/constants/equtils.ml
+++ b/src/coq/constants/equtils.ml
@@ -14,7 +14,7 @@ let coq_init_logic =
 
 (* equality *)
 let eq : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "eq")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "eq")), 0)
 
 (* Constructor for quality *)
 let eq_refl : types =
diff --git a/src/coq/constants/idutils.ml b/src/coq/constants/idutils.ml
index 8bf2da7..1f109d8 100644
--- a/src/coq/constants/idutils.ml
+++ b/src/coq/constants/idutils.ml
@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Environ
 open Evd
 
 let coq_init_datatypes =
diff --git a/src/coq/constants/produtils.ml b/src/coq/constants/produtils.ml
index a07adbe..f3942d3 100644
--- a/src/coq/constants/produtils.ml
+++ b/src/coq/constants/produtils.ml
@@ -14,7 +14,7 @@ let coq_init_data =
 
 (* prod types *)
 let prod : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_data (Label.make "prod")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_data (Label.make "prod")), 0)
 
 (* Introduction for sigma types *)
 let pair : constr =
diff --git a/src/coq/constants/proputils.ml b/src/coq/constants/proputils.ml
index ecc32b1..3af7aeb 100644
--- a/src/coq/constants/proputils.ml
+++ b/src/coq/constants/proputils.ml
@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Apputils
 
 let coq_init_logic =
   ModPath.MPfile
@@ -14,7 +13,7 @@ let coq_init_logic =
 
 (* Logical or *)
 let logical_or : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "or")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "or")), 0)
   
 (* left constructor of \/ *)
 let or_introl : types =
@@ -27,7 +26,7 @@ let or_intror : types =
 
 (* Logical and *)
 let logical_and : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "and")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "and")), 0)
   
 (* constructor of /\ *)
 let conj : types =
diff --git a/src/coq/constants/sigmautils.ml b/src/coq/constants/sigmautils.ml
index a7ed555..b92acf9 100644
--- a/src/coq/constants/sigmautils.ml
+++ b/src/coq/constants/sigmautils.ml
@@ -14,7 +14,7 @@ let coq_init_specif =
 
 (* sigma types *)
 let sigT : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_specif (Label.make "sigT")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_specif (Label.make "sigT")), 0)
 
 (* Introduction for sigma types *)
 let existT : types =
diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml
index a7c24bd..4dfdbb7 100644
--- a/src/coq/decompiler/decompiler.ml
+++ b/src/coq/decompiler/decompiler.ml
@@ -36,11 +36,11 @@ let parse_tac_str (s : string) : unit Proofview.tactic =
 (* Run a coq tactic against a given goal, returning generated subgoals *)
 let run_tac env sigma (tac : unit Proofview.tactic) (goal : constr)
     : Goal.goal list * Evd.evar_map =
-  let p = Proof.start sigma [(env, EConstr.of_constr goal)] in
-  let (p', _) = Proof.run_tactic env tac p in
-  let (subgoals, _, _, _, sigma) = Proof.proof p' in
-  subgoals, sigma
-    
+  let p = Proof.start ~name:(destVar goal) ~poly:true sigma [(env, EConstr.of_constr goal)] in
+  let (p', _, _) = Proof.run_tactic env tac p in
+  let compact_p = Proof.data p' in
+  (compact_p.goals, compact_p.sigma)
+
 (* Returns true if the given tactic solves the goal. *)
 let solves env sigma (tac : unit Proofview.tactic) (goal : constr) : bool state =
   try
@@ -476,7 +476,7 @@ and apply_in (n, valu, typ, body) (env, sigma, opts) : tactical option =
     
 (* Last resort decompile let-in as a pose.  *)
 and pose (n, valu, t, body) (env, sigma, opts) : tactical option =
-  let n' = fresh_name env n in
+  let n' = fresh_name env n.binder_name in
   let env' = push_let_in (Name n', valu, t) env in
   let decomp_body = first_pass env' sigma opts body in
   (* If the binding is NEVER used, just skip this. *)
diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml
index 51787a2..1c009a5 100644
--- a/src/coq/devutils/printing.ml
+++ b/src/coq/devutils/printing.ml
@@ -24,7 +24,7 @@ module CRD = Context.Rel.Declaration
 let pr_global_as_constr gref =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  pr_constr_env env sigma (Universes.constr_of_global gref)
+  pr_constr_env env sigma (UnivGen.constr_of_monomorphic_global gref)
 
 (* Using pp, prints directly to a string *)
 let print_to_string (pp : formatter -> 'a -> unit) (trm : 'a) : string =
@@ -66,11 +66,12 @@ let sort_as_string s =
 
 (* Prints a term *)
 let rec term_as_string (env : env) (trm : types) =
+  let open Context in
   match kind trm with
   | Rel i ->
      (try
        let (n, _, _) = CRD.to_tuple @@ lookup_rel i env in
-       Printf.sprintf "(%s [Rel %d])" (name_as_string n) i
+       Printf.sprintf "(%s [Rel %d])" (name_as_string n.binder_name) i
      with
        Not_found -> Printf.sprintf "(Unbound_Rel %d)" i)
   | Var v ->
@@ -84,22 +85,22 @@ let rec term_as_string (env : env) (trm : types) =
   | Prod (n, t, b) ->
      Printf.sprintf
        "(Π (%s : %s) . %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env t)
-       (term_as_string (push_local (n, t) env) b)
+       (term_as_string (push_local (n.binder_name, t) env) b)
   | Lambda (n, t, b) ->
      Printf.sprintf
        "(λ (%s : %s) . %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env t)
-       (term_as_string (push_local (n, t) env) b)
+       (term_as_string (push_local (n.binder_name, t) env) b)
   | LetIn (n, trm, typ, e) ->
      Printf.sprintf
        "(let (%s : %s) := %s in %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env typ)
        (term_as_string env trm)
-       (term_as_string (push_let_in (n, trm, typ) env) e)
+       (term_as_string (push_let_in (n.binder_name, trm, typ) env) e)
   | App (f, xs) ->
      Printf.sprintf
        "(%s %s)"
@@ -119,14 +120,15 @@ let rec term_as_string (env : env) (trm : types) =
      let name_id = (ind_bodies.(i_index)).mind_typename in
      Id.to_string name_id
   | Fix ((is, i), (ns, ts, ds)) ->
-     let env_fix = push_rel_context (bindings_for_fix ns ds) env in
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
+     let env_fix = push_rel_context (bindings_for_fix ns_binder_name ds) env in
      String.concat
        " with "
        (map3
           (fun n t d ->
             Printf.sprintf
              "(Fix %s : %s := %s)"
-             (name_as_string n)
+             (name_as_string n.binder_name)
              (term_as_string env t)
              (term_as_string env_fix d))
           (Array.to_list ns)
@@ -180,7 +182,7 @@ let env_as_string (env : env) : string =
          let (n, b, t) = CRD.to_tuple @@ lookup_rel i env in
          Printf.sprintf
            "%s (Rel %d): %s"
-           (name_as_string n)
+           (name_as_string n.binder_name)
            i
            (term_as_string (pop_rel_context i env) t))
        all_relis)
diff --git a/src/coq/devutils/printing.mli b/src/coq/devutils/printing.mli
index d4dc67d..e90a439 100644
--- a/src/coq/devutils/printing.mli
+++ b/src/coq/devutils/printing.mli
@@ -8,7 +8,7 @@ open Evd
 (* --- Coq terms --- *)
 
 (* Pretty-print a `global_reference` with fancy `constr` coloring. *)
-val pr_global_as_constr : global_reference -> Pp.t
+val pr_global_as_constr : Globnames.global_reference -> Pp.t
 
 (* Gets a name as a string *)
 val name_as_string : Name.t -> string
diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml
index d44c7cc..13b9ef9 100644
--- a/src/coq/logicutils/contexts/contextutils.ml
+++ b/src/coq/logicutils/contexts/contextutils.ml
@@ -20,7 +20,8 @@ module CND = Context.Named.Declaration
 let is_rel_assum = CRD.is_local_assum
 
 (* Is the rel declaration a local definition? *)
-let is_rel_defin = CRD.is_local_def
+(* let is_rel_defin x = CRD.is_local_def (get_rel_ctx_name x) *)
+let is_rel_defin x = CRD.is_local_def x
 
 (* Is the named declaration an assumption? *)
 let is_named_assum = CND.is_local_assum
@@ -47,14 +48,25 @@ let named_value decl = CND.get_value decl
 
 (* Get the type of a named declaration *)
 let named_type decl = CND.get_type decl
-    
+
+(* --- Context manipulation tools --- *)
+
+(* Get relative context for a name *)
+let get_rel_ctx_name name = 
+  match name with (* handle if anon or not *)
+  | Anonymous -> Context.anonR
+  | Name idt -> Context.nameR idt
+
+(* Get relative context for a declaration *)
+let get_rel_ctx decl = get_rel_ctx_name (rel_name decl)
+
 (* --- Constructing declarations --- *)
 
 (* Make the rel declaration for a local assumption *)
-let rel_assum (name, typ) = CRD.LocalAssum (name, typ)
+let rel_assum (name, typ) = CRD.LocalAssum (get_rel_ctx_name name, typ)
 
 (* Make the rel declaration for a local definition *)
-let rel_defin (name, def, typ) = CRD.LocalDef (name, def, typ)
+let rel_defin (name, def, typ) = CRD.LocalDef (get_rel_ctx_name name, def, typ)
 
 (* Make the named declaration for a local assumption *)
 let named_assum (id, typ) = CND.LocalAssum (id, typ)
@@ -104,7 +116,7 @@ let smash_prod_assum ctxt body =
     (fun body decl ->
        match rel_value decl with
        | Some defn -> Vars.subst1 defn body
-       | None -> mkProd (rel_name decl, rel_type decl, body))
+       | None -> mkProd (get_rel_ctx decl, rel_type decl, body))
     ~init:body
     ctxt
 
@@ -117,7 +129,7 @@ let smash_lam_assum ctxt body =
     (fun body decl ->
        match rel_value decl with
        | Some defn -> Vars.subst1 defn body
-       | None -> mkLambda (rel_name decl, rel_type decl, body))
+       | None -> mkLambda (get_rel_ctx decl, rel_type decl, body))
     ~init:body
     ctxt
 
@@ -127,11 +139,12 @@ let smash_lam_assum ctxt body =
  *)
 let decompose_prod_n_zeta n term =
   assert (n >= 0);
+  let open Context in
   let rec aux n ctxt body =
     if n > 0 then
       match Constr.kind body with
       | Prod (name, param, body) ->
-        aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body
+        aux (n - 1) (Rel.add (rel_assum (name.binder_name, param)) ctxt) body
       | LetIn (name, def_term, def_type, body) ->
         aux n ctxt (Vars.subst1 def_term body)
       | _ ->
@@ -139,7 +152,7 @@ let decompose_prod_n_zeta n term =
     else
       ctxt, body
   in
-  aux n Context.Rel.empty term
+  aux n Rel.empty term
 
 (*
  * Decompose the first n lambda bindings, zeta-reducing let bindings to reveal
@@ -147,11 +160,12 @@ let decompose_prod_n_zeta n term =
  *)
 let decompose_lam_n_zeta n term =
   assert (n >= 0);
+  let open Context in
   let rec aux n ctxt body =
     if n > 0 then
       match Constr.kind body with
       | Lambda (name, param, body) ->
-        aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body
+        aux (n - 1) (Rel.add (rel_assum (name.binder_name, param)) ctxt) body
       | LetIn (name, def_term, def_type, body) ->
         Vars.subst1 def_term body |> aux n ctxt
       | _ ->
@@ -159,7 +173,7 @@ let decompose_lam_n_zeta n term =
     else
       ctxt, body
   in
-  aux n Context.Rel.empty term
+  aux n Rel.empty term
 
 (* Bind the declarations of a local context as product/let-in bindings *)
 let recompose_prod_assum decls term =
@@ -200,8 +214,8 @@ let bindings_for_inductive env mutind_body ind_bodies : rel_declaration list =
        (fun i ind_body ->
          let name_id = ind_body.mind_typename in
          let typ = type_of_inductive env i mutind_body in
-         CRD.LocalAssum (Name name_id, typ))
-       ind_bodies)
+         CRD.LocalAssum (Context.nameR name_id, typ))
+       mutind_body.mind_packets)
 
 (*
  * Fixpoints
@@ -210,7 +224,8 @@ let bindings_for_fix (names : name array) (typs : types array) : rel_declaration
   Array.to_list
     (CArray.map2_i
        (fun i name typ -> CRD.LocalAssum (name, Vars.lift i typ))
-       names typs)
+       (Array.map get_rel_ctx_name names)
+       typs)
 
 (* --- Combining contexts --- *)
 
diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli
index f227051..9faf1c6 100644
--- a/src/coq/logicutils/contexts/contextutils.mli
+++ b/src/coq/logicutils/contexts/contextutils.mli
@@ -35,8 +35,18 @@ val define_rel_decl :
 (*
  * Construct a named assumption/definition
  *)
+val named_assum : Id.t Context.binder_annot * 'types -> ('constr, 'types) CND.pt
+val named_defin : Id.t Context.binder_annot * 'constr * 'types -> ('constr, 'types) CND.pt
+
+(* Old version, breaking change. TODO: make sure this doesn't affect any downstream plugins
 val named_assum : Id.t * 'types -> ('constr, 'types) CND.pt
 val named_defin : Id.t * 'constr * 'types -> ('constr, 'types) CND.pt
+*)
+
+(* Context name/decl manipulation *)
+val get_rel_ctx_name : Names.name -> Names.Name.t Context.binder_annot
+
+val get_rel_ctx : ('constr, 'types) CRD.pt -> Names.Name.t Context.binder_annot
 
 (* --- Questions about declarations --- *)
 
diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml
index 3b4ebb5..41c8e6f 100644
--- a/src/coq/logicutils/contexts/envutils.ml
+++ b/src/coq/logicutils/contexts/envutils.ml
@@ -6,14 +6,13 @@ open Utilities
 open Environ
 open Constr
 open Declarations
-open Decl_kinds
-open Constrextern
-open Contextutils
 open Evd
 open Names
 open Nameutils
 open Stateutils
-   
+
+open Contextutils
+
 (* Look up all indexes from is in env *)
 let lookup_rels (is : int list) (env : env) : rel_declaration list =
  List.map (fun i -> lookup_rel i env) is
@@ -33,15 +32,15 @@ let lookup_all_rels (env : env) : rel_declaration list =
 (* Return a name-type pair from the given rel_declaration. *)
 let rel_name_type rel : Name.t * types =
   match rel with
-  | CRD.LocalAssum (n, t) -> (n, t)
-  | CRD.LocalDef (n, _, t) -> (n, t)
+  | CRD.LocalAssum (n, t) -> (n.binder_name, t)
+  | CRD.LocalDef (n, _, t) -> (n.binder_name, t)
 
 
 (* Push a local binding to an environment *)
-let push_local (n, t) = push_rel CRD.(LocalAssum (n, t))
+let push_local (n, t) = push_rel CRD.(LocalAssum (get_rel_ctx_name n, t))
 
 (* Push a let-in definition to an environment *)
-let push_let_in (n, e, t) = push_rel CRD.(LocalDef(n, e, t))
+let push_let_in (n, e, t) = push_rel CRD.(LocalDef(get_rel_ctx_name n, e, t))
 
 (* Lookup n rels and remove then *)
 let lookup_pop (n : int) (env : env) =
@@ -53,7 +52,7 @@ let force_constant_body const_body =
   | Def const_def ->
     Mod_subst.force_constr const_def
   | OpaqueDef opaq ->
-    Opaqueproof.force_proof (Global.opaque_tables ()) opaq
+    fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq)
   | _ ->
     CErrors.user_err ~hdr:"force_constant_body"
       (Pp.str "An axiom has no defining term")
diff --git a/src/coq/logicutils/contexts/modutils.ml b/src/coq/logicutils/contexts/modutils.ml
index 709ab84..e204268 100644
--- a/src/coq/logicutils/contexts/modutils.ml
+++ b/src/coq/logicutils/contexts/modutils.ml
@@ -25,9 +25,10 @@ let decompose_module_signature mod_sign =
  * The optional argument specifies functor parameters.
  *)
 let declare_module_structure ?(params=[]) ident declare_elements =
-  let mod_sign = Vernacexpr.Check [] in
+  let mod_sign = Declaremods.Check []in
   let mod_path =
-    Declaremods.start_module Modintern.interp_module_ast None ident params mod_sign
+    (* Declaremods.start_module None ident params Modintern.interp_module_ast mod_sign *)
+    Declaremods.start_module None ident params mod_sign
   in
   Dumpglob.dump_moddef mod_path "mod";
   declare_elements mod_path;
@@ -55,7 +56,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body =
     match mod_elem with
     | SFBconst const_body ->
       let const = Constant.make2 mod_path label in
-      if Refset.mem (ConstRef const) globset then
+      if Names.GlobRef.Set.mem (ConstRef const) globset then
         (globset, acc)
       else
         (globset, fold_const acc const const_body)
@@ -63,9 +64,10 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body =
       check_inductive_supported mind_body;
       let ind_body = mind_body.mind_packets.(0) in
       let ind = (MutInd.make2 mod_path label, 0) in
+      let env = Global.env () in (* might need to pass something other than an empty env *)
       let globset' =
-        List.map (Indrec.lookup_eliminator ind) ind_body.mind_kelim |>
-        List.fold_left (fun gset gref -> Refset.add gref gset) globset
+        List.map (Indrec.lookup_eliminator env ind) [ind_body.mind_kelim] |>
+        List.fold_left (fun gset gref -> Names.GlobRef.Set.add gref gset) globset
       in
       (globset', fold_ind acc ind (mind_body, ind_body))
     | SFBmodule mod_body ->
@@ -77,7 +79,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body =
         Pp.(str "Skipping nested module signature " ++ Label.print label);
       (globset, acc)
   in
-  fold_module_structure_by_elem (Refset.empty, init) fold_mod_elem mod_body |> snd
+  fold_module_structure_by_elem (Names.GlobRef.Set.empty, init) fold_mod_elem mod_body |> snd
 
 (*
  * Same as `fold_module_structure_by_decl` except a single step function
diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli
index b1becf4..b23e60e 100644
--- a/src/coq/logicutils/contexts/modutils.mli
+++ b/src/coq/logicutils/contexts/modutils.mli
@@ -15,7 +15,7 @@ val decompose_module_signature : module_signature -> (Names.MBId.t * module_type
  *
  * The optional argument specifies functor parameters.
  *)
-val declare_module_structure : ?params:(Constrexpr.module_ast Declaremods.module_params) -> Id.t -> (ModPath.t -> unit) -> ModPath.t
+val declare_module_structure : ?params:(Declaremods.module_params) -> Id.t -> (ModPath.t -> unit) -> ModPath.t
 
 (*
  * Fold over the constant/inductive definitions within a module structure,
@@ -24,15 +24,19 @@ val declare_module_structure : ?params:(Constrexpr.module_ast Declaremods.module
  *
  * Elimination schemes (e.g., `Ind_rect`) are filtered out from the definitions.
  *)
-val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> constant_body -> 'a) -> ('a -> inductive -> Inductive.mind_specif -> 'a) -> module_body -> 'a
+(* val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> 'opaque constant_body -> 'a) -> ('a -> inductive -> Inductive.mind_specif -> 'a) -> module_body -> 'a 
+val fold_module_structure_by_decl : 'a -> ('a -> Names.Constant.t -> 'opaque Declarations.constant_body -> 'a) -> ('a -> Names.inductive -> Inductive.mind_specif -> 'a) -> Declarations.module_body -> 'a *)
+val fold_module_structure_by_decl : 'a -> ('a -> Names.Constant.t -> Opaqueproof.opaque Declarations.constant_body -> 'a) -> ('a -> Names.MutInd.t * int -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -> 'a) -> 'b Declarations.generic_module_body -> 'a
 
 (*
  * Same as `fold_module_structure_by_decl` except a single step function
  * accepting a global reference.
  *)
-val fold_module_structure_by_glob : 'a -> ('a -> global_reference -> 'a) -> module_body -> 'a
+(* val fold_module_structure_by_glob : 'a -> ('a -> evaluable_global_reference -> 'a) -> module_body -> 'a *)
+val fold_module_structure_by_glob : 'a -> ('a -> Names.evaluable_global_reference -> 'a) -> Declarations.module_body -> 'a
 
 (*
  * Same as `fold_module_structure_by_glob` except an implicit unit accumulator.
  *)
-val iter_module_structure_by_glob : (global_reference -> unit) -> module_body -> unit
+val iter_module_structure_by_glob : (Globnames.global_reference -> unit) -> 'a Declarations.generic_module_body -> unit
+val fold_module_structure_by_glob : 'a -> ('a -> Globnames.global_reference -> 'a) -> 'b Declarations.generic_module_body -> 'a
diff --git a/src/coq/logicutils/hofs/filters.ml b/src/coq/logicutils/hofs/filters.ml
index 585bae3..96d872b 100644
--- a/src/coq/logicutils/hofs/filters.ml
+++ b/src/coq/logicutils/hofs/filters.ml
@@ -4,7 +4,6 @@ open Constr
 open Environ
 open Debruijn
 open Evd
-open Utilities
 open Checking
 open Inference
 open Stateutils
diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml
index 29bd75a..112ef05 100644
--- a/src/coq/logicutils/hofs/hofs.ml
+++ b/src/coq/logicutils/hofs/hofs.ml
@@ -5,7 +5,6 @@ open Constr
 open Contextutils
 open Envutils
 open Utilities
-open Names
 open Evd
 open Stateutils
 
@@ -147,6 +146,7 @@ let map_rec_env_fix_cartesian (map_rec : ('a, 'b) list_transformer_with_env) d e
  * TODO explain
  *)
 let map_term_env_rec map_rec f d env sigma a trm =
+  let open Context in
   match kind trm with
   | Cast (c, k, t) ->
      let sigma, c' = map_rec env sigma a c in
@@ -154,16 +154,16 @@ let map_term_env_rec map_rec f d env sigma a trm =
      sigma, mkCast (c', k, t')
   | Prod (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkProd (n, t', b')
   | Lambda (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkLambda (n, t', b')
   | LetIn (n, trm, typ, e) ->
      let sigma, trm' = map_rec env sigma a trm in
      let sigma, typ' = map_rec env sigma a typ in
-     let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+     let sigma, e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
      sigma, mkLetIn (n, trm', typ', e')
   | App (fu, args) ->
      let sigma, fu' = map_rec env sigma a fu in
@@ -175,12 +175,15 @@ let map_term_env_rec map_rec f d env sigma a trm =
      let sigma, bs' = map_rec_args map_rec env sigma a bs in
      sigma, mkCase (ci, ct', m', bs')
   | Fix ((is, i), (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args 
+       (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkFix ((is, i), (ns, ts', ds'))
   | CoFix (i, (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkCoFix (i, (ns, ts', ds'))
   | Proj (p, c) ->
      let sigma, c' = map_rec env sigma a c in
@@ -216,6 +219,7 @@ let map_term f d a trm =
  * TODO explain
  *)
 let map_subterms_env_rec map_rec f d env sigma a trm =
+  let open Context in
   match kind trm with
   | Cast (c, k, t) ->
      let sigma, cs' = map_rec env sigma a c in
@@ -223,16 +227,16 @@ let map_subterms_env_rec map_rec f d env sigma a trm =
      sigma, combine_cartesian (fun c' t' -> mkCast (c', k, t')) cs' ts'
   | Prod (n, t, b) ->
      let sigma, ts' = map_rec env sigma a t in
-     let sigma, bs' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, bs' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, combine_cartesian (fun t' b' -> mkProd (n, t', b')) ts' bs'
   | Lambda (n, t, b) ->
      let sigma, ts' = map_rec env sigma a t in
-     let sigma, bs' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, bs' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, combine_cartesian (fun t' b' -> mkLambda (n, t', b')) ts' bs'
   | LetIn (n, trm, typ, e) ->
      let sigma, trms' = map_rec env sigma a trm in
      let sigma, typs' = map_rec env sigma a typ in
-     let sigma, es' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+     let sigma, es' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
      sigma, combine_cartesian (fun trm' (typ', e') -> mkLetIn (n, trm', typ', e')) trms' (cartesian typs' es')
   | App (fu, args) ->
      let sigma, fus' = map_rec env sigma a fu in
@@ -244,12 +248,14 @@ let map_subterms_env_rec map_rec f d env sigma a trm =
      let sigma, bss' = map_rec_args_cartesian map_rec env sigma a bs in
      sigma, combine_cartesian (fun ct' (m', bs') -> mkCase (ci, ct', m', bs')) cts' (cartesian ms' bss')
   | Fix ((is, i), (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, tss' = map_rec_args_cartesian map_rec env sigma a ts in
-     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, combine_cartesian (fun ts' ds' -> mkFix ((is, i), (ns, ts', ds'))) tss' dss'
   | CoFix (i, (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, tss' = map_rec_args_cartesian map_rec env sigma a ts in
-     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, combine_cartesian (fun ts' ds' -> mkCoFix (i, (ns, ts', ds'))) tss' dss'
   | Proj (p, c) ->
      let sigma, cs' = map_rec env sigma a c in
@@ -309,6 +315,7 @@ let rec map_term_env_if p f d env sigma a trm =
  * TODO explain
  *)
 let map_term_env_rec_shallow map_rec f d env sigma a trm =
+  let open Context in
   match kind trm with
   | Cast (c, k, t) ->
      let sigma, c' = map_rec env sigma a c in
@@ -316,16 +323,16 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm =
      sigma, mkCast (c', k, t')
   | Prod (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkProd (n, t', b')
   | Lambda (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkLambda (n, t', b')
   | LetIn (n, trm, typ, e) ->
      let sigma, trm' = map_rec env sigma a trm in
      let sigma, typ' = map_rec env sigma a typ in
-     let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+     let sigma, e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
      sigma, mkLetIn (n, trm', typ', e')
   | App (fu, args) ->
      let sigma, fu' = map_rec env sigma a fu in
@@ -340,12 +347,14 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm =
      let sigma, bs' = map_rec_args map_rec env sigma a bs in
      sigma, mkCase (ci, ct', m', bs')
   | Fix ((is, i), (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkFix ((is, i), (ns, ts', ds'))
   | CoFix (i, (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkCoFix (i, (ns, ts', ds'))
   | Proj (p, c) ->
      let sigma, c' = map_rec env sigma a c in
@@ -483,6 +492,7 @@ let rec map_subterms_env_if_combs p f d env sigma a trm =
  * Like map_term_env_if, but make a list of subterm results
  *)
 let rec map_term_env_if_list p f d env sigma a trm =
+  let open Context in
   let map_rec = map_term_env_if_list p f d in
   let sigma_t, p_holds = p env sigma a trm in
   let new_subterms = if p_holds
@@ -495,16 +505,16 @@ let rec map_term_env_if_list p f d env sigma a trm =
        List.append c' t'
     | Prod (n, t, b) ->
        let t' = map_rec env sigma a t in
-       let b' = map_rec (push_local (n, t) env) sigma (d a) b in
+       let b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
        List.append t' b'
     | Lambda (n, t, b) ->
        let t' = map_rec env sigma a t in
-       let b' = map_rec (push_local (n, t) env) sigma (d a) b in
+       let b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
        List.append t' b'
     | LetIn (n, trm, typ, e) ->
        let trm' = map_rec env sigma a trm in
        let typ' = map_rec env sigma a typ in
-       let e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+       let e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
        List.append trm' (List.append typ' e')
     | App (fu, args) ->
        let fu' = map_rec env sigma a fu in
@@ -516,12 +526,14 @@ let rec map_term_env_if_list p f d env sigma a trm =
        let bs' = Array.map (map_rec env sigma a) bs in
        List.append ct' (List.append m' (List.flatten (Array.to_list bs')))
     | Fix ((is, i), (ns, ts, ds)) ->
+       let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
        let ts' = Array.map (map_rec env sigma a) ts in
-       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in
+       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns_binder_name ts) ds in
        List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds'))
     | CoFix (i, (ns, ts, ds)) ->
+       let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
        let ts' = Array.map (map_rec env sigma a) ts in
-       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in
+       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns_binder_name ts) ds in
        List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds'))
     | Proj (pr, c) ->
        map_rec env sigma a c
@@ -580,16 +592,16 @@ let rec exists_subterm_env p d env sigma (a : 'a) (trm : types) : evar_map * boo
          sigma, c' || t'
       | Prod (n, t, b) ->
          let sigma, t' = map_rec env sigma a t in
-         let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+         let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
          sigma, t' || b'
       | Lambda (n, t, b) ->
          let sigma, t' = map_rec env sigma a t in
-         let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+         let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
          sigma, t' || b'
       | LetIn (n, trm, typ, e) ->
          let sigma, trm' = map_rec env sigma a trm in
          let sigma, typ' = map_rec env sigma a typ in
-         let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+         let sigma, e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
          sigma, trm' || typ' || e'
       | App (fu, args) ->
          let sigma, fu' = map_rec env sigma a fu in
diff --git a/src/coq/logicutils/hofs/substitution.ml b/src/coq/logicutils/hofs/substitution.ml
index f4f0e2e..702f7e3 100644
--- a/src/coq/logicutils/hofs/substitution.ml
+++ b/src/coq/logicutils/hofs/substitution.ml
@@ -117,7 +117,7 @@ let all_typ_substs_combs : (types * types) comb_substitution =
 
  (* --- Substituting global references --- *)
 
-type global_substitution = global_reference Globnames.Refmap.t
+type global_substitution = Globnames.global_reference GlobRef.Map.t
 
 (* Substitute global references throughout a term *)
 let rec subst_globals subst (term : constr) =
@@ -126,7 +126,7 @@ let rec subst_globals subst (term : constr) =
     (fun _ t ->
       try
         pglobal_of_constr t |>
-        map_puniverses (flip Globnames.Refmap.find subst) |>
+        map_puniverses (flip GlobRef.Map.find subst) |>
         constr_of_pglobal
       with _ ->
         match kind t with
diff --git a/src/coq/logicutils/hofs/substitution.mli b/src/coq/logicutils/hofs/substitution.mli
index 205bcf4..f489d26 100644
--- a/src/coq/logicutils/hofs/substitution.mli
+++ b/src/coq/logicutils/hofs/substitution.mli
@@ -3,7 +3,6 @@
 open Environ
 open Constr
 open Evd
-open Names
 
 (* TODO clean up so retrieval is easier *)
 
@@ -76,7 +75,7 @@ val all_typ_substs_combs : (types * types) comb_substitution
 
 (* --- Substituting global references (TODO unify w/ above after cleaning types) --- *)
 
-type global_substitution = global_reference Globnames.Refmap.t
+type global_substitution = Globnames.global_reference Names.GlobRef.Map.t
 
 (* Substitute global references throughout a term *)
 val subst_globals : global_substitution -> constr -> constr
diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml
index 722b554..ce68ff6 100644
--- a/src/coq/logicutils/hofs/zooming.ml
+++ b/src/coq/logicutils/hofs/zooming.ml
@@ -10,7 +10,6 @@ open Envutils
 open Contextutils
 open Debruijn
 open Sigmautils
-open Evd
 open Names
 
 (* --- Zooming --- *)
@@ -22,7 +21,7 @@ let rec zoom_n_prod env npm typ : env * types =
   else
     match kind typ with
     | Prod (n1, t1, b1) ->
-       zoom_n_prod (push_local (n1, t1) env) (npm - 1) b1
+       zoom_n_prod (push_local (n1.binder_name, t1) env) (npm - 1) b1
     | _ ->
        failwith "more parameters expected"
 
@@ -35,7 +34,7 @@ let zoom_n_lambda env npm trm : env * types =
 let rec zoom_lambda_term (env : env) (trm : types) : env * types =
   match kind trm with
   | Lambda (n, t, b) ->
-     zoom_lambda_term (push_local (n, t) env) b
+     zoom_lambda_term (push_local (n.binder_name, t) env) b
   | _ ->
      (env, trm)
 
@@ -43,7 +42,7 @@ let rec zoom_lambda_term (env : env) (trm : types) : env * types =
 let rec zoom_product_type (env : env) (typ : types) : env * types =
   match kind typ with
   | Prod (n, t, b) ->
-     zoom_product_type (push_local (n, t) env) b
+     zoom_product_type (push_local (n.binder_name, t) env) b
   | _ ->
      (env, typ)
 
@@ -56,7 +55,7 @@ let zoom_lambda_names env except trm : env * types * Id.t list =
     | limit ->
      match kind trm with
      | Lambda (n, t, b) ->
-        let name = fresh_name env n in
+        let name = fresh_name env n.binder_name in
         let env' = push_local (Name name, t) env in
         let env, trm, names =
           aux env' (limit - 1) b in
diff --git a/src/coq/logicutils/inductive/.indutils.ml.swp b/src/coq/logicutils/inductive/.indutils.ml.swp
new file mode 100644
index 0000000..b5d0694
Binary files /dev/null and b/src/coq/logicutils/inductive/.indutils.ml.swp differ
diff --git a/src/coq/logicutils/inductive/.indutils.mli.swp b/src/coq/logicutils/inductive/.indutils.mli.swp
new file mode 100644
index 0000000..2e42f74
Binary files /dev/null and b/src/coq/logicutils/inductive/.indutils.mli.swp differ
diff --git a/src/coq/logicutils/inductive/indexing.ml b/src/coq/logicutils/inductive/indexing.ml
index b01d640..9746731 100644
--- a/src/coq/logicutils/inductive/indexing.ml
+++ b/src/coq/logicutils/inductive/indexing.ml
@@ -10,7 +10,6 @@ open Hofimpls
 open Reducers
 open Sigmautils
 open Apputils
-open Evd
 
 (* --- Generic functions --- *)
 
diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml
index c8c1b5b..6655777 100644
--- a/src/coq/logicutils/inductive/indutils.ml
+++ b/src/coq/logicutils/inductive/indutils.ml
@@ -15,6 +15,8 @@ open Envutils
 open Contextutils
 open Inference
 open Evd
+open Entries
+open DeclareInd
 
 (* Don't support mutually inductive or coinductive types yet (TODO move) *)
 let check_inductive_supported mutind_body : unit =
@@ -31,7 +33,7 @@ let check_inductive_supported mutind_body : unit =
 let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option =
   let (c, u) = pc in
   let kn = Constant.canonical c in
-  let (modpath, dirpath, label) = KerName.repr kn in
+  let (modpath, label) = KerName.repr kn in
   let rec try_find_ind is_rev =
     try
       let label_string = Label.to_string label in
@@ -42,7 +44,7 @@ let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option =
       if (suffix = "_ind" || suffix = "_rect" || suffix = "_rec" || suffix = "_ind_r") then
         let ind_label_string = String.sub label_string 0 split_index in
         let ind_label = Label.of_id (Id.of_string_soft ind_label_string) in
-        let ind_name = MutInd.make1 (KerName.make modpath dirpath ind_label) in
+        let ind_name = MutInd.make1 (KerName.make modpath ind_label) in
         let _ = lookup_mind ind_name env in
         Some ind_name
       else
@@ -78,7 +80,10 @@ let is_elim (env : env) (trm : types) =
 
 (* Lookup the eliminator over the type sort *)
 let type_eliminator (env : env) (ind : inductive) =
-  Universes.constr_of_global (Indrec.lookup_eliminator ind InType)
+  UnivGen.constr_of_monomorphic_global (Indrec.lookup_eliminator env ind InType)
+  (* TODO: Does this need to support polymorphic (and not just monomorphic)?
+     E.g.: Evd.fresh_global env (Evd.from_env env) (Indrec.lookup_eliminator env ind InType) 
+   *)
 
 (* Applications of eliminators *)
 type elim_app =
@@ -125,9 +130,9 @@ let rec num_ihs env sigma rec_typ typ =
      let t_red = reduce_stateless reduce_term env sigma t in
      if is_or_applies rec_typ t_red then
        let (n_b_t, b_t, b_b) = destProd b in
-       1 + num_ihs (push_local (n, t) (push_local (n_b_t, b_t) env)) sigma rec_typ b_b
+       1 + num_ihs (push_local (n.binder_name, t) (push_local (n_b_t.binder_name, b_t) env)) sigma rec_typ b_b
      else
-       num_ihs (push_local (n, t) env) sigma rec_typ b
+       num_ihs (push_local (n.binder_name, t) env) sigma rec_typ b
   | _ ->
      0
 
@@ -147,6 +152,7 @@ let arity_of_ind_body ind_body =
     recompose_prod_assum ind_body.mind_arity_ctxt sort
 
 (* Create an Entries.local_entry from a Rel.Declaration.t *)
+(*
 let make_ind_local_entry decl =
   let entry =
     match decl with
@@ -156,38 +162,63 @@ let make_ind_local_entry decl =
   match CRD.get_name decl with
   | Name.Name id -> (id, entry)
   | Name.Anonymous -> failwith "Parameters to an inductive type may not be anonymous"
+*)
 
 (* Instantiate an abstract universe context *)
 let inst_abs_univ_ctx abs_univ_ctx =
   (* Note that we're creating *globally* fresh universe levels. *)
-  Universes.fresh_instance_from_context abs_univ_ctx |> Univ.UContext.make
+   UnivGen.fresh_instance abs_univ_ctx
 
 (* Instantiate an abstract_inductive_universes into an Entries.inductive_universes with Univ.UContext.t (TODO do we do something with evar_map here?) *)
 let make_ind_univs_entry = function
-  | Monomorphic_ind univ_ctx_set ->
+  | Monomorphic univ_ctx_set ->
     let univ_ctx = Univ.UContext.empty in
-    (Entries.Monomorphic_ind_entry univ_ctx_set, univ_ctx)
-  | Polymorphic_ind abs_univ_ctx ->
-    let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in
-    (Entries.Polymorphic_ind_entry univ_ctx, univ_ctx)
+    (Entries.Monomorphic_entry univ_ctx_set, univ_ctx)
+  | Polymorphic abs_univ_ctx ->
+    let univ_ctx_repr = (Univ.AUContext.repr abs_univ_ctx) in
+    (Entries.Polymorphic_entry 
+      (Univ.AUContext.names abs_univ_ctx, univ_ctx_repr), univ_ctx_repr)
+(*
   | Cumulative_ind abs_univ_cumul ->
     let abs_univ_ctx = Univ.ACumulativityInfo.univ_context abs_univ_cumul in
     let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in
     let univ_var = Univ.ACumulativityInfo.variance abs_univ_cumul in
     let univ_cumul = Univ.CumulativityInfo.make (univ_ctx, univ_var) in
     (Entries.Cumulative_ind_entry univ_cumul, univ_ctx)
+*)
 
 let open_inductive ?(global=false) env (mind_body, ind_body) =
   let univs, univ_ctx = make_ind_univs_entry mind_body.mind_universes in
   let subst_univs = Vars.subst_instance_constr (Univ.UContext.instance univ_ctx) in
   let env = Environ.push_context univ_ctx env in
   if global then
-    Global.push_context false univ_ctx;
+    Global.push_context_set false (Univ.ContextSet.of_context univ_ctx);
   let arity = arity_of_ind_body ind_body in
-  let arity_ctx = [CRD.LocalAssum (Name.Anonymous, arity)] in
+  let arity_ctx = [CRD.LocalAssum (get_rel_ctx_name Name.Anonymous, arity)] in
   let ctors_typ = Array.map (recompose_prod_assum arity_ctx) ind_body.mind_user_lc in
   env, univs, subst_univs arity, Array.map_to_list subst_univs ctors_typ
 
+
+(* Internal func from the Coq kernel, for debugging. This func used to be exposed, but now is hidden.
+   TODO: remove 
+let declare_mind mie =
+  let id = match mie.mind_entry_inds with
+  | ind::_ -> ind.mind_entry_typename
+  | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
+  let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
+  let names = List.map map_names mie.mind_entry_inds in
+  List.iter (fun (typ, cons) -> Declare.check_exists typ;
+  List.iter Declare.check_exists cons) names;
+  let _kn' = Global.add_mind id mie in
+  let (sp,kn as oname) = Lib.add_leaf id (DeclareInd.inInductive { ind_names = names }) in
+  if is_unsafe_typing_flags() then feedback_axiom ();
+  let mind = Global.mind_of_delta_kn kn in
+  let isprim = declare_projections mie.mind_entry_universes mind in
+  Impargs.declare_mib_implicits mind;
+  declare_inductive_argument_scopes mind mie;
+  oname, isprim
+*)
+
 let declare_inductive typename consnames template univs nparam arity constypes =
   let open Entries in
   let params, arity = Term.decompose_prod_n_assum nparam arity in
@@ -202,13 +233,18 @@ let declare_inductive typename consnames template univs nparam arity constypes =
   let mind_entry =
     { mind_entry_record = None;
       mind_entry_finite = Declarations.Finite;
-      mind_entry_params = List.map make_ind_local_entry params;
+      mind_entry_params = params;
       mind_entry_inds = [ind_entry];
       mind_entry_universes = univs;
+      mind_entry_variance = None;
       mind_entry_private = None }
   in
-  let ((_, ker_name), _) = Declare.declare_mind mind_entry in
+  let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in
+  (mind, 0)
+  (* 
+  let ((_, ker_name), _) = declare_mind mind_entry in
   let mind = MutInd.make1 ker_name in
   let ind = (mind, 0) in
   Indschemes.declare_default_schemes mind;
   ind
+  *)
diff --git a/src/coq/logicutils/inductive/indutils.mli b/src/coq/logicutils/inductive/indutils.mli
index 502e99b..9c484b8 100644
--- a/src/coq/logicutils/inductive/indutils.mli
+++ b/src/coq/logicutils/inductive/indutils.mli
@@ -69,9 +69,9 @@ val arity_of_ind_body : one_inductive_body -> types
  * universe levels, and return the universe-synchronized environment. If global
  * is true, the global environment is also synchronized with the new universe
  * levels and constraints. A descriptor for the inductive type's universe
- * properties is also returned.
+ * properties is also returned. Mutual inductive types are not supported.
  *)
-val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entries.inductive_universes * types * types list
+val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entries.universes_entry * types * types list
 
 (*
  * Declare a new inductive type in the global environment. Note that the arity
@@ -79,5 +79,5 @@ val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entri
  * a recursive reference and then all parameters (i.e.,
  * forall (I : arity) (P : params), ...).
  *)
-val declare_inductive : Id.t -> Id.t list -> bool -> Entries.inductive_universes -> int -> types -> types list -> inductive
+val declare_inductive : Id.t -> Id.t list -> bool -> Entries.universes_entry -> int -> types -> types list -> inductive
 
diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index 1a786ad..11db6c3 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -4,6 +4,8 @@
  * TODO move out some module stuff etc.
  *)
 
+open Stdlib
+open Map
 open Util
 open Environ
 open Constr
@@ -15,6 +17,8 @@ open Indutils
 open Substitution
 open Stateutils
 open Recordops
+open Record
+open Printing
 
 (* Type-sensitive transformation of terms *)
 type constr_transformer = env -> evar_map -> constr -> evar_map * constr
@@ -28,7 +32,7 @@ let force_constant_body const_body =
   | Def const_def ->
     Mod_subst.force_constr const_def
   | OpaqueDef opaq ->
-    Opaqueproof.force_proof (Global.opaque_tables ()) opaq
+    fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq)
   | _ ->
     CErrors.user_err ~hdr:"force_constant_body"
       (Pp.str "An axiom has no defining term")
@@ -43,9 +47,9 @@ let force_constant_body const_body =
 let transform_constant ident tr_constr const_body =
   let env =
     match const_body.const_universes with
-    | Monomorphic_const univs ->
+    | Monomorphic  univs ->
       Global.env () |> Environ.push_context_set univs
-    | Polymorphic_const univs ->
+    | Polymorphic univs ->
       CErrors.user_err ~hdr:"transform_constant"
         Pp.(str "Universe polymorphism is not supported")
   in
@@ -53,6 +57,7 @@ let transform_constant ident tr_constr const_body =
   let sigma = Evd.from_env env in
   let sigma, term' = tr_constr env sigma term in
   let sigma, type' = tr_constr env sigma const_body.const_type in
+  let open Printing in
   sigma, Globnames.destConstRef (define_term ~typ:type' ident sigma term' true)
 
 (*
@@ -89,20 +94,27 @@ let try_register_record mod_path (ind, ind') =
   try
     let r = lookup_structure ind in
     Feedback.msg_info (Pp.str "Transformed a record");
-    let pks = r.s_PROJKIND in
-    let ps =
-      List.map
-        (Option.map (fun p -> Constant.make2 mod_path (Constant.label p)))
-        r.s_PROJ
-    in
     (try
-       declare_structure (ind', (ind', 1), pks, ps)
+       declare_structure_entry (r.s_CONST, r.s_PROJKIND, r.s_PROJ)
      with _ ->
        Feedback.msg_warning
          (Pp.str "Failed to register projections for transformed record"))
   with Not_found ->
     ()
 
+let lookup_eliminator_error_handling ind sorts = 
+  (* Feedback.msg_warning (Pp.(str "start ")); *)
+  let env = Global.env () in
+  List.filter_map (fun x -> x)
+  (List.map 
+    (fun x -> 
+      (* try Some (x, Indrec.lookup_eliminator env ind x) *)
+      try Some (x, Indrec.lookup_eliminator env ind x)
+      with
+      | _ -> None
+    )
+    sorts)
+
 (*
  * Declare a new module structure under the given name with the compositionally
  * transformed (i.e., forward-substituted) components from the given module
@@ -117,7 +129,7 @@ let try_register_record mod_path (ind, ind') =
  *
  * TODO sigma handling, not sure how to do it here/if we need it
  *)
-let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Globnames.Refset.empty) ident tr_constr mod_body =
+let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef.Set.empty) ident tr_constr mod_body =
   let open Modutils in
   let mod_path = mod_body.mod_mp in
   let mod_arity, mod_elems = decompose_module_signature mod_body.mod_type in
@@ -127,7 +139,7 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl
         match b with
         | SFBconst const_body ->
            let const = Constant.make2 mod_path l in
-           not (Globnames.Refset.mem (ConstRef const) opaques)
+           not (GlobRef.Set.mem (ConstRef const) opaques)
         | _ ->
            true)
       mod_elems
@@ -141,24 +153,63 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl
     match body with
     | SFBconst const_body ->
       let const = Constant.make2 mod_path label in
-      if Globnames.Refmap.mem (ConstRef const) subst then
+      if GlobRef.Map.mem (ConstRef const) subst then
         subst (* Do not transform schematic definitions. *)
       else
         let sigma, const' = transform_constant ident tr_constr const_body in
-        Globnames.Refmap.add (ConstRef const) (ConstRef const') subst
+        GlobRef.Map.add (ConstRef const) (ConstRef const') subst
     | SFBmind mind_body ->
       check_inductive_supported mind_body;
       let ind = (MutInd.make2 mod_path label, 0) in
       let ind_body = mind_body.mind_packets.(0) in
       let sigma, ind' = transform_inductive ident tr_constr (mind_body, ind_body) in
       try_register_record mod_path' (ind, ind');
+      let subst = GlobRef.Map.add (IndRef ind) (IndRef ind') subst in
       let ncons = Array.length ind_body.mind_consnames in
       let list_cons ind = List.init ncons (fun i -> ConstructRef (ind, i + 1)) in
-      let sorts = ind_body.mind_kelim in
-      let list_elim ind = List.map (Indrec.lookup_eliminator ind) sorts in
-      Globnames.Refmap.add (IndRef ind) (IndRef ind') subst |>
-      List.fold_right2 Globnames.Refmap.add (list_cons ind) (list_cons ind') |>
-      List.fold_right2 Globnames.Refmap.add (list_elim ind) (list_elim ind')
+      (* let sorts = List.map Sorts.family [Sorts.sprop; Sorts.set; Sorts.prop; Sorts.type1] in *)
+      let sorts = List.map Sorts.family [Sorts.sprop; Sorts.prop; Sorts.set; Sorts.type1] in
+      let list_elim ind_arg = lookup_eliminator_error_handling ind_arg sorts in
+
+      let list_elim_ind = list_elim ind in
+      let list_elim_ind' = list_elim ind' in
+      (* let list_elim_ind_map = Map.Make.of_seq list_elim_ind in 
+      let list_elim_ind'_map = Map.Make.of_seq list_elim_ind' in *)
+      let list_elim_ind_sorts = List.map fst list_elim_ind in
+      let list_elim_ind'_sorts = List.map fst list_elim_ind' in
+      let common_sorts = List.filter (fun x -> List.exists (fun y -> Sorts.family_equal x y) list_elim_ind_sorts) list_elim_ind'_sorts in 
+      let list_elim_ind_winnowed = List.map snd (List.filter (fun (x, y) -> List.exists (fun z -> Sorts.family_equal x z) common_sorts) list_elim_ind) in
+      let list_elim_ind'_winnowed = List.map snd (List.filter (fun (x, y) -> List.exists (fun z -> Sorts.family_equal x z) common_sorts) list_elim_ind') in
+      (*
+      Feedback.msg_warning (Names.MutInd.print (fst ind));
+      Feedback.msg_warning (Pp.str ("ind level " ^ (string_of_int (snd ind))));
+      Feedback.msg_warning (Names.MutInd.print (fst ind'));
+      Feedback.msg_warning (Pp.str ("ind level " ^ (string_of_int (snd ind'))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_cons ind))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_elim ind))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_cons ind'))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_elim ind'))));
+      *)
+      (* let sorts = List.map (fun x -> x ind_body.mind_kelim) sort_funcs in *)
+      (* let sorts = List.filter (fun x -> match Sorts.relevance_of_sort_family x with 
+                                        | Sorts.Relevant -> true
+                                        | Sorts.Irrelevant -> false 
+                              )  *)
+      (* List.filter (fun x -> Sorts.family_leq x ind_body.mind_kelim) *)
+      (* Feedback.msg_warning (Pp.str (string_of_int (List.length sorts))); *)
+      (*
+      let subst = GlobRef.Map.add (IndRef ind) (IndRef ind') subst in 
+      let subst = List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') subst in
+      let subst = List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind') subst in 
+      subst *)
+      (*
+      GlobRef.Map.add (IndRef ind) (IndRef ind') subst |>
+      List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
+      List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind')
+      *)
+      GlobRef.Map.add (IndRef ind) (IndRef ind') subst |>
+      List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
+      List.fold_right2 GlobRef.Map.add (list_elim_ind_winnowed) (list_elim_ind'_winnowed)
     | SFBmodule mod_body ->
       Feedback.msg_warning (Pp.str "Skipping nested module structure");
       subst
diff --git a/src/coq/logicutils/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli
index 68c42f1..5093e2b 100644
--- a/src/coq/logicutils/transformation/transform.mli
+++ b/src/coq/logicutils/transformation/transform.mli
@@ -20,7 +20,7 @@ type constr_transformer = env -> evar_map -> constr -> evar_map * constr
  * NOTE: Global side effects.
  *)
 val transform_constant :
-  Id.t -> constr_transformer -> constant_body -> evar_map * Constant.t
+  Id.t -> constr_transformer -> Opaqueproof.opaque constant_body -> evar_map * Constant.t
 
 (*
  * Declare a new inductive family under the given name with the transformed type
@@ -45,4 +45,4 @@ val transform_inductive :
  * NOTE: Global side effects.
  *)
 val transform_module_structure :
-  ?init:(unit -> global_substitution) -> ?opaques:(Globnames.Refset.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t
+  env -> ?init:(unit -> global_substitution) -> ?opaques:(Names.GlobRef.Set.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t
diff --git a/src/coq/logicutils/typesandequality/convertibility.ml b/src/coq/logicutils/typesandequality/convertibility.ml
index 8b1a854..c50b46e 100644
--- a/src/coq/logicutils/typesandequality/convertibility.ml
+++ b/src/coq/logicutils/typesandequality/convertibility.ml
@@ -4,7 +4,6 @@
 
 open Constr
 open Contextutils
-open Utilities
 open Environ
 open Evd
 open Inference
diff --git a/src/coq/logicutils/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml
index 31af8fe..f01f546 100644
--- a/src/coq/logicutils/typesandequality/inference.ml
+++ b/src/coq/logicutils/typesandequality/inference.ml
@@ -2,25 +2,19 @@
  * Type inference
  *)
 
-open Environ
-open Evd
 open Constr
 open Declarations
              
 (* Safely infer the WHNF type of a term, updating the evar map *)
 let infer_type env sigma term =
-  let sigma_ref = ref sigma in
   let eterm = EConstr.of_constr term in
-  let typ = Typing.e_type_of ~refresh:true env sigma_ref eterm in
-  let sigma = ! sigma_ref in
+  let (sigma, typ) = Typing.type_of ~refresh:true env sigma eterm in
   sigma, EConstr.to_constr sigma typ
 
 (* Safely infer the sort of a type, updating the evar map *)
 let infer_sort env sigma term =
-  let sigma_ref = ref sigma in
   let eterm = EConstr.of_constr term in
-  let sort = Typing.e_sort_of env sigma_ref eterm in
-  let sigma = ! sigma_ref in
+  let (sigma, sort) = Typing.sort_of env sigma eterm in
   sigma, Sorts.family sort
 
 (* Get the type of an inductive type (TODO do we need evar_map here?) *)
diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index a18b343..f19548a 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -2,11 +2,8 @@
  * Utilities for defining terms
  *)
 
-open Constr
 open Names
 open Evd
-open Decl_kinds
-open Recordops
 open Constrexpr
 open Constrextern
 
@@ -15,7 +12,7 @@ open Constrextern
 (* https://github.com/ybertot/plugin_tutorials/blob/master/tuto1/src/simple_declare.ml 
 
 TODO do we need to return the updated evar_map? *)
-let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook refresh =
+let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
   let open EConstr in
   (* XXX: "Standard" term construction combinators such as `mkApp`
      don't add any universe constraints that may be needed later for
@@ -45,36 +42,32 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re
     else
       sigma
   in
-  let sigma = Evd.minimize_universes sigma in
-  let body = to_constr sigma body in
-  let tyopt = Option.map (to_constr sigma) tyopt in
-  let uvars_fold uvars c =
-    Univ.LSet.union uvars (Univops.universes_of_constr c) in
-  let uvars = List.fold_left uvars_fold Univ.LSet.empty
-    (Option.List.cons tyopt [body]) in
-  let sigma = Evd.restrict_universe_context sigma uvars in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *)
+  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:true ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let ubinders = Evd.universe_binders sigma in
-  let ce = Declare.definition_entry ?types:tyopt ~univs body in
-  DeclareDef.declare_definition ident k ce ubinders imps hook
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind = Decls.(IsDefinition Definition) in
+  DeclareDef.declare_definition ~name:ident ~scope ~kind ?hook_data:hook ubinders ce imps
 
 (* Define a new Coq term *)
-let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) =
-  let k = (Global, Flags.is_universe_polymorphism(), Definition) in
+let define_term ?typ (n : Id.t) (evm : evar_map) (trm : Constr.types) (refresh : bool) =
+  (* let k = (Global, Flags.is_universe_polymorphism(), Definition) in *)
+  let poly = Attributes.is_universe_polymorphism() in
   let udecl = UState.default_univ_decl in
-  let nohook = Lemmas.mk_hook (fun _ x -> x) in
+  (* let nohook = DeclareDef.Hook.make (fun x -> x) in *)
   let etrm = EConstr.of_constr trm in
   let etyp = Option.map EConstr.of_constr typ in
-  edeclare n k ~opaque:false evm udecl etrm etyp [] nohook refresh
+  edeclare n poly ~opaque:false evm udecl etrm etyp [] None refresh
 
 (* Define a Canonical Structure *)
-let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) =
-  let k = (Global, Flags.is_universe_polymorphism (), CanonicalStructure) in
+let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : Constr.types) (refresh : bool) =
+  (* let k = (Global, Flags.is_universe_polymorphism(), Definition) in *)
+  let poly = Attributes.is_universe_polymorphism() in
   let udecl = UState.default_univ_decl in
-  let hook = Lemmas.mk_hook (fun _ x -> declare_canonical_structure x; x) in
+  let hook = DeclareDef.Hook.make (fun x -> let open DeclareDef.Hook.S in Canonical.declare_canonical_structure x.dref) in
   let etrm = EConstr.of_constr trm in
   let etyp = Option.map EConstr.of_constr typ in
-  edeclare n k ~opaque:false evm udecl etrm etyp [] hook refresh
+  edeclare n poly ~opaque:false evm udecl etrm etyp [] (Some (hook, Evd.evar_universe_context evm, [])) refresh (* todo: check if last empty list is correct to pass *)
 
 (* --- Converting between representations --- *)
 
@@ -83,7 +76,7 @@ let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : b
  *)
 
 (* Intern a term (for now, ignore the resulting evar_map) *)
-let intern env sigma t : evar_map * types =
+let intern env sigma t : evar_map * Constr.types =
   let (sigma, trm) = Constrintern.interp_constr_evars env sigma t in
   sigma, EConstr.to_constr sigma trm
 
@@ -92,30 +85,31 @@ let extern env sigma t : constr_expr =
   Constrextern.extern_constr true env sigma (EConstr.of_constr t)
 
 (* Construct the external expression for a definition *)
-let expr_of_global (g : global_reference) : constr_expr =
+let expr_of_global (g : Globnames.global_reference) : constr_expr =
   let r = extern_reference Id.Set.empty g in
   CAst.make @@ (CAppExpl ((None, r, None), []))
 
 (* Convert a term into a global reference with universes (or raise Not_found) *)
 let pglobal_of_constr term =
-  match Constr.kind term with
-  | Const (const, univs) -> Globnames.ConstRef const, univs
-  | Ind (ind, univs) -> IndRef ind, univs
-  | Construct (cons, univs) -> ConstructRef cons, univs
-  | Var id -> VarRef id, Univ.Instance.empty
-  | _ -> raise Not_found
+  let open Constr in 
+    match Constr.kind term with
+    | Const (const, univs) -> Globnames.ConstRef const, univs
+    | Ind (ind, univs) ->  Names.GlobRef.IndRef ind, univs
+    | Construct (cons, univs) -> Names.GlobRef.ConstructRef cons, univs
+    | Var id -> Names.GlobRef.VarRef id, Univ.Instance.empty
+    | _ -> raise Not_found
 
 (* Convert a global reference with universes into a term *)
 let constr_of_pglobal (glob, univs) =
   match glob with
-  | Globnames.ConstRef const -> mkConstU (const, univs)
-  | IndRef ind -> mkIndU (ind, univs)
-  | ConstructRef cons -> mkConstructU (cons, univs)
-  | VarRef id -> mkVar id
+  | Globnames.ConstRef const -> Constr.mkConstU (const, univs)
+  | Names.GlobRef.IndRef ind -> Constr.mkIndU (ind, univs)
+  | Names.GlobRef.ConstructRef cons -> Constr.mkConstructU (cons, univs)
+  | Names.GlobRef.VarRef id -> Constr.mkVar id
 
 (* Safely instantiate a global reference, with proper universe handling *)
 let new_global sigma gref =
   let sigma_ref = ref sigma in
-  let glob =  Evarutil.e_new_global sigma_ref gref in
+  let (_, glob) = Evarutil.new_global sigma gref in
   let sigma = ! sigma_ref in
   sigma, EConstr.to_constr sigma glob
diff --git a/src/coq/representationutils/defutils.mli b/src/coq/representationutils/defutils.mli
index 84cfc2e..1035648 100644
--- a/src/coq/representationutils/defutils.mli
+++ b/src/coq/representationutils/defutils.mli
@@ -7,6 +7,7 @@ open Names
 open Evd
 open Environ
 open Constrexpr
+open Globnames
 
 (* --- Defining Coq terms --- *)
 
diff --git a/src/coq/representationutils/nameutils.ml b/src/coq/representationutils/nameutils.ml
index 9432148..cf72370 100644
--- a/src/coq/representationutils/nameutils.ml
+++ b/src/coq/representationutils/nameutils.ml
@@ -2,7 +2,6 @@
  * Utilities for names, references, and identifiers
  *)
 
-open Constr
 open Names
 open Util
 
diff --git a/src/coq/termutils/constutils.ml b/src/coq/termutils/constutils.ml
index 4a8e384..9886f2d 100644
--- a/src/coq/termutils/constutils.ml
+++ b/src/coq/termutils/constutils.ml
@@ -3,7 +3,6 @@
  *)
 
 open Constr
-open Environ
 open Names
 
 (* --- Constructing constants --- *)
@@ -18,8 +17,10 @@ let make_constant id =
  * Safely extract the body of a constant, instantiating any universe variables 
  *)
 let open_constant env const =
-  let (Some (term, auctx)) = Global.body_of_constant const in
-  let uctx = Universes.fresh_instance_from_context auctx |> Univ.UContext.make in
-  let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in
-  let env = Environ.push_context uctx env in
-  env, term
+  match Global.body_of_constant Library.indirect_accessor const with 
+    | (Some (term, _, auctx)) -> 
+      let (uinst, uctxset) = UnivGen.fresh_instance auctx in 
+      let uctx = Univ.UContext.make (uinst, (Univ.ContextSet.constraints uctxset)) in
+      let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in
+      let env = Environ.push_context uctx env in env, term
+    | None -> failwith "Constant extraction failed"
diff --git a/src/plib.mlpack b/src/plib.mlpack
index 2d376a0..35ddd3a 100644
--- a/src/plib.mlpack
+++ b/src/plib.mlpack
@@ -18,8 +18,8 @@ Idutils
 Proputils
 
 Stateutils
-Envutils
 Contextutils
+Envutils
 
 Hofs
 Debruijn
diff --git a/src/plibrary.ml4 b/src/plibrary.mlg
similarity index 100%
rename from src/plibrary.ml4
rename to src/plibrary.mlg
diff --git a/src/utilities/utilities.ml b/src/utilities/utilities.ml
index 2d54096..5bff4bc 100644
--- a/src/utilities/utilities.ml
+++ b/src/utilities/utilities.ml
@@ -140,6 +140,9 @@ let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list =
   match (l1, l2, l3) with
   | ([], [], []) ->
      []
+  | ([], _, _) -> failwith "Mismatched sized lists passed to map3"
+  | (_, [], _) -> failwith "Mismatched sized lists passed to map3"
+  | (_, _, []) -> failwith "Mismatched sized lists passed to map3"
   | (h1 :: t1, h2 :: t2, h3 :: t3) ->
      let r = f h1 h2 h3 in r :: map3 f t1 t2 t3