137 files changed, 1106 insertions, 687 deletions

diff --git a/.gitignore b/.gitignore
index adbf9dd189..0c7a8f70f6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -121,14 +121,14 @@ doc/unreleased.rst
 
 coqpp/coqpp_lex.ml
 dev/ocamlweb-doc/lex.ml
-ide/coq_lex.ml
-ide/config_lexer.ml
-ide/utf8_convert.ml
+ide/coqide/coq_lex.ml
+ide/coqide/config_lexer.ml
+ide/coqide/utf8_convert.ml
 tools/coqwc.ml
 tools/coqdep_lexer.ml
 tools/ocamllibdep.ml
 tools/coqdoc/cpretty.ml
-ide/protocol/xml_lexer.ml
+ide/coqide/protocol/xml_lexer.ml
 
 # .mly files
 
@@ -143,7 +143,7 @@ plugins/ltac/coretactics.ml
 plugins/ltac/extratactics.ml
 plugins/ltac/extraargs.ml
 plugins/ltac/profile_ltac_tactics.ml
-ide/coqide_os_specific.ml
+ide/coqide/coqide_os_specific.ml
 plugins/ssrmatching/ssrmatching.ml
 plugins/ssr/ssrparser.ml
 plugins/ssr/ssrvernac.ml
@@ -155,9 +155,9 @@ kernel/byterun/coq_jumptbl.h
 kernel/genOpcodeFiles.exe
 kernel/copcodes.ml
 kernel/uint63.ml
-ide/default.bindings
-ide/default_bindings_src.exe
-ide/index_urls.txt
+ide/coqide/default.bindings
+ide/coqide/default_bindings_src.exe
+ide/coqide/index_urls.txt
 .lia.cache
 .nia.cache
 
@@ -187,4 +187,4 @@ META.coq
 *.install
 !Makefile.install
 
-ide/coqide.keys
+ide/coqide/coqide.keys
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6c9725f047..a6ed9be58d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-05-19-V33"
+  CACHEKEY: "bionic_coq-V2020-05-24-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/Makefile.build b/Makefile.build
index 3140df4cee..7806dce79c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -254,7 +254,7 @@ OCAMLOPT = $(TIMER) $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
-DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/% user-contrib/%,$@),, -I ide -I ide/protocol)
+DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/% user-contrib/%,$@),, -I ide/coqide -I ide/coqide/protocol)
 
 # On MacOS, the binaries are signed, except our private ones
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
@@ -555,15 +555,15 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqidetop
 
-FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
+FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/coqide/protocol/ideprotocol.cma ide/coqide/document.cmo ide/coqide/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPEXE)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
+	$(HIDE)$(call bestocaml, -I ide/coqide -I ide/coqide/protocol -package str -package dynlink)
 
 $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(call ocamlbyte, -I ide -package str,unix,threads)
+	$(HIDE)$(call ocamlbyte, -I ide/coqide -package str,unix,threads)
 
 # votour: a small vo explorer (based on the checker)
 
@@ -692,7 +692,7 @@ kernel/kernel.cmxa: kernel/kernel.mllib
 	$(SHOW)'OCAMLOPT -pack -o $@'
 	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
-COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
+COND_IDEFLAGS=$(if $(filter ide/coqide/fake_ide% tools/coq_makefile%,$<), -I ide/coqide -I ide/coqide/protocol,)
 COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
 
 COND_GRAMFLAGS=$(if $(filter gramlib/.pack/%,$<),-no-alias-deps -w -49,) $(if $(filter gramlib/.pack/gramlib__%,$<),-open Gramlib,)
diff --git a/Makefile.ide b/Makefile.ide
index ef9d67d4ec..640ee7b188 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -13,13 +13,13 @@
 ## NB: For the moment, the build system of CoqIDE is part of
 ## the one of Coq. In particular, this Makefile.ide is included in
 ## Makefile.build. Please ensure that the rules define here are
-## indeed specific to files of the form ide/*
+## indeed specific to files of the form ide/coqide/*
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
 #HASCOQIDE : opt / byte / no
 #IDEFLAGS : some extra cma, for instance
-#IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
+#IDEOPTCDEPS : on windows, ide/coqide/ide_win32_stubs.o ide/coqide/coq_icon.o
 #IDECDEPS
 #IDECDEPSFLAGS
 #IDEINT : X11 / QUARTZ / WIN32
@@ -34,11 +34,11 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 ## CoqIDE source directory and files
 
 # Note : for just building bin/coqide, we could only consider
-# config, lib, ide and ide/utils. But the coqidetop plugin (the
+# config, lib, ide/coqide and ide/coqide/utils. But the coqidetop plugin (the
 # one that will be loaded by coqidetop) refers to some
 # core modules of coq, for instance printing/*.
 
-IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
+IDESRCDIRS:= $(CORESRCDIRS) ide/coqide ide/coqide/protocol
 
 ifeq ($(HASCOQIDE),no)
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS))
@@ -46,20 +46,20 @@ else
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) -package lablgtk3-sourceview3
 endif
 
-IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
-IDECMA:=ide/ide.cma
+IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/coqide/protocol/ideprotocol.cma
+IDECMA:=ide/coqide/ide.cma
 IDETOPEXE=bin/coqidetop$(EXE)
 IDETOP=bin/coqidetop.opt$(EXE)
 IDETOPBYTE=bin/coqidetop.byte$(EXE)
 
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide/coqide_os_specific.cmo ide/coqide/coqide_main.mli ide/coqide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide/coqide_os_specific.cmx ide/coqide/coqide_main.mli ide/coqide/coqide_main.ml
 
-IDEBINDINGS:=ide/default.bindings
-IDEBINDINGSSRC:=ide/default_bindings_src.ml
-IDEBINDINGSEXE:=ide/default_bindings_src.exe
+IDEBINDINGS:=ide/coqide/default.bindings
+IDEBINDINGSSRC:=ide/coqide/default_bindings_src.ml
+IDEBINDINGSEXE:=ide/coqide/default_bindings_src.exe
 
-IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png $(IDEBINDINGS)
+IDEFILES=$(wildcard ide/coqide/*.lang) ide/coqide/coq_style.xml ide/coqide/coq.png $(IDEBINDINGS)
 
 ## GTK for Coqide MacOS bundle
 
@@ -118,49 +118,49 @@ $(COQIDEBYTE): $(LINKIDE)
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
 	       -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
-ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
+ide/coqide/coqide_os_specific.ml: ide/coqide/coqide_$(IDEINT).ml.in config/Makefile
 	rm -f $@ && cp $< $@ && chmod a-w $@
 
-ide/%.cmi: ide/%.mli
+ide/coqide/%.cmi: ide/coqide/%.mli
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
-ide/%.cmo: ide/%.ml
+ide/coqide/%.cmo: ide/coqide/%.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
-ide/%.cmx: ide/%.ml
+ide/coqide/%.cmx: ide/coqide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
 # We need to compile this file without -safe-string due mess with
 # lablgtk API. Other option is to require lablgtk >= 3.0.0
-ide/ideutils.cmo: ide/ideutils.ml
+ide/coqide/ideutils.cmo: ide/coqide/ideutils.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLC)) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
-ide/ideutils.cmx: ide/ideutils.ml
+ide/coqide/ideutils.cmx: ide/coqide/ideutils.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $<
 
-IDETOPCMA:=ide/ide_common.cma
+IDETOPCMA:=ide/coqide/ide_common.cma
 IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa)
 
 # Special rule for coqidetop
 $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
 	rm -f $@ && cp $< $@
 
-$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
+$(IDETOP): ide/coqide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide/coqide -I ide/coqide/protocol/ \
 			   $(SYSMOD) \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP_HIDE) $@
 	$(CODESIGN_HIDE) $@
 
-$(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
+$(IDETOPBYTE): ide/coqide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
+	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide/coqide -I ide/coqide/protocol/ \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) \
 			 $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@
@@ -219,12 +219,12 @@ endif
 
 install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
 	$(MKDIR) $(FULLDATADIR)
-	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR)
+	$(INSTALLLIB) ide/coqide/coq.png ide/coqide/*.lang ide/coqide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR)
 	$(MKDIR) $(FULLCONFIGDIR)
 
 install-ide-info:
 	$(MKDIR) $(FULLDOCDIR)
-	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
+	$(INSTALLLIB) ide/coqide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
 
 ###########################################################################
 # CoqIde MacOS special targets
@@ -235,10 +235,10 @@ install-ide-info:
 $(COQIDEAPP)/Contents:
 	rm -rdf $@
 	$(MKDIR) $@
-	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
+	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/coqide/MacOS/Info.plist.template > $@/Info.plist
 	$(MKDIR) "$@/MacOS"
 
-$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
+$(COQIDEINAPP): ide/coqide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
 	        -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
@@ -246,7 +246,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(MKDIR) $@/coq/
-	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $@/coq/
+	$(INSTALLLIB) ide/coqide/coq.png ide/coqide/*.lang ide/coqide/coq_style.xml $(IDEBINDINGS) $@/coq/
 	$(MKDIR) $@/gtksourceview-3.0/{language-specs,styles}
 	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-3.0/language-specs/
 	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/
@@ -287,7 +287,7 @@ $(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $
 	done
 
 $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
-	$(INSTALLLIB) ide/MacOS/*.icns $@
+	$(INSTALLLIB) ide/coqide/MacOS/*.icns $@
 
 $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
 	$(CODESIGN_HIDE) $@
diff --git a/Makefile.install b/Makefile.install
index cc0888d8e4..4977bb38e1 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -91,12 +91,12 @@ install-tools:
 # - the ones corresponding to packed plugins
 
 INSTALLCMI = $(sort \
-	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
+	$(filter-out checker/% ide/coqide/% tools/%, $(MLIFILES:.mli=.cmi)) \
 	$(GRAMMLIFILES:.mli=.cmi) gramlib/.pack/gramlib.cmi \
 	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
 	$(PLUGINS:.cmo=.cmi)
 
-INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
+INSTALLCMX = $(sort $(filter-out checker/% ide/coqide/% tools/% dev/% \
 	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
 	$(GRAMMLFILES:.ml=.cmx) $(MLFILES:.ml=.cmx)))
 
diff --git a/Makefile.make b/Makefile.make
index 2a0a58756c..7191738612 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES))
 GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES?
 
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
 GENMLIFILES:=$(GRAMMLIFILES)
 GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe
@@ -262,10 +262,10 @@ optclean:
 
 clean-ide:
 	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
-	rm -f ide/input_method_lexer.ml
-	rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
-	rm -f ide/utf8_convert.ml
-	rm -f ide/default.bindings ide/default_bindings_src.exe
+	rm -f ide/coqide/input_method_lexer.ml
+	rm -f ide/coqide/highlight.ml ide/coqide/config_lexer.ml ide/coqide/config_parser.mli ide/coqide/config_parser.ml
+	rm -f ide/coqide/utf8_convert.ml
+	rm -f ide/coqide/default.bindings ide/coqide/default_bindings_src.exe
 	rm -rf $(COQIDEAPP)
 
 mlgclean:
diff --git a/configure.ml b/configure.ml
index 9cfa9d409e..c05844198b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -81,7 +81,7 @@ let read_lines_and_close fd =
 (** Run some unix command and read the first line of its output.
     We avoid Unix.open_process and its non-fully-portable /bin/sh,
     especially when it comes to quoting the filenames.
-    See open_process_pid in ide/coq.ml for more details.
+    See open_process_pid in ide/coqide/coq.ml for more details.
     Error messages:
      - if err=StdErr, any error message goes in the stderr of our script.
      - if err=StdOut, we merge stderr and stdout (just as 2>&1).
@@ -784,7 +784,7 @@ let coqide_flags () =
         idearchdef := "QUARTZ"
       end
     | "opt", "win32" ->
-      idearchfile := "ide/ide_win32_stubs.o ide/coq_icon.o";
+      idearchfile := "ide/coqide/ide_win32_stubs.o ide/coqide/coq_icon.o";
       idecdepsflags := "-custom";
       idearchflags := "-ccopt '-subsystem windows'";
       idearchdef := "WIN32"
@@ -847,9 +847,9 @@ let install = [
   "COQLIBINSTALL", "the Coq library", !prefs.libdir,
     Relative "lib", Relative "lib/coq", Relative "";
   "CONFIGDIR", "the Coqide configuration files", !prefs.configdir,
-    Relative "config", Absolute "/etc/xdg/coq", Relative "ide";
+    Relative "config", Absolute "/etc/xdg/coq", Relative "ide/coqide";
   "DATADIR", "the Coqide data files", !prefs.datadir,
-    Relative "share", Relative "share/coq", Relative "ide";
+    Relative "share", Relative "share/coq", Relative "ide/coqide";
   "MANDIR", "the Coq man pages", !prefs.mandir,
     Relative "man", Relative "share/man", Relative "man";
   "DOCDIR", "the Coq documentation", !prefs.docdir,
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 052014824f..f34bbea4e9 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -423,7 +423,7 @@ Binary file ./bin/ocpp5.exe matches
 Binary file ./lib/config/coq_config.cmo matches
 Binary file ./lib/config/coq_config.o matches
 Binary file ./lib/grammar/grammar.cma matches
-Binary file ./lib/ide/ide_win32_stubs.o matches
+Binary file ./lib/ide/coqide/ide_win32_stubs.o matches
 Binary file ./lib/lib/clib.a matches
 Binary file ./lib/lib/clib.cma matches
 Binary file ./lib/libcoqrun.a matches
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 963b0e6387..ba552ab302 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1303,11 +1303,11 @@ function copy_coq_gtk {
     install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled"        "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
 
     install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*'      "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
-    install -D -T "ide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
-    install -D -T "ide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+    install -D -T "ide/coqide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+    install -D -T "ide/coqide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
 
     install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*'              "$PREFIXCOQ/share/gtksourceview-3.0/styles"
-    install -D -T "ide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+    install -D -T "ide/coqide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
 
     install_rec   "$PREFIXMINGW/share/themes" '*'                                "$PREFIXCOQ/share/themes"
 
@@ -1340,8 +1340,8 @@ function copy_coq_gtk {
     #   COQSHARE="$PREFIXCOQ/share/"
     # fi
 
-    # mkdir -p "$PREFIXCOQ/ide"
-    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
+    # mkdir -p "$PREFIXCOQ/ide/coqide"
+    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide/coqide"
     # rmdir "$PREFIXCOQ/share/coq" || true
   fi
 }
@@ -1598,7 +1598,7 @@ function make_coq_installer {
     cp ../patches/ReplaceInFile.nsh dev/nsis
     VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
     cd dev/nsis
-    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coqide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
 
     build_post
   fi
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0d2f1dfbc7..8c5696f4f9 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-19-V33"
+# CACHEKEY: "bionic_coq-V2020-05-24-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -13,8 +13,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         libgtksourceview-3.0-dev \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
-        xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
-        fonts-freefont-otf \
+        python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
         # Dependencies of source-doc and coq-makefile
         texlive-science tipa
 
diff --git a/dev/include_printers b/dev/include_printers
index d077075eeb..30529b5fd6 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -27,7 +27,6 @@
 #install_printer  (* id set *) ppidset;;
 #install_printer  (* int set *) ppintset;;
 
-#install_printer  (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
 #install_printer  (* Reductionops machine stack *) pp_stack_t;;
 
 (*#install_printer  (* hint_db *)  print_hint_db;;*)
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 06db787488..63071bba72 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -46,7 +46,6 @@ install_printer Top_printers.pp_idpred
 install_printer Top_printers.pp_cpred
 install_printer Top_printers.pp_transparent_state
 install_printer Top_printers.pp_stack_t
-install_printer Top_printers.pp_cst_stack_t
 install_printer Top_printers.pp_state_t
 install_printer Top_printers.ppmetas
 install_printer Top_printers.ppevm
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 00050a89e1..bca1eb5754 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -169,7 +169,6 @@ let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
 let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
 let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 
 (* proof printers *)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c826391cac..65eab8daa3 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -106,7 +106,6 @@ val pp_cpred : Names.Cpred.t -> unit
 val pp_transparent_state : TransparentState.t -> unit
 
 val pp_stack_t : Constr.t Reductionops.Stack.t -> unit
-val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit
 val pp_state_t : Reductionops.state -> unit
 
 val ppmetas : Evd.Metaset.t -> unit
diff --git a/doc/README.md b/doc/README.md
index 8e1bc85c49..e3ab5ae4d2 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -58,7 +58,6 @@ additional tools are required:
   - makeindex
   - xelatex
   - latexmk
-  - xindy
 
 All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
 install them with:
@@ -68,7 +67,7 @@ install them with:
 Or if you want to use less disk space:
 
     apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
-                latexmk xindy fonts-freefont-otf
+                latexmk fonts-freefont-otf
 
 Compilation
 -----------
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index fabf7a519f..99762c7a0e 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -214,11 +214,12 @@ html_context = {
     'conf_py_path': '/doc/sphinx/',
     # Versions and downloads listed in the versions menu (see _templates/versions.html)
     'versions': [
-        ("master", "https://coq.github.io/doc/master/refman/"),
+        ("dev", "https://coq.github.io/doc/master/refman/"),
         ("stable", "https://coq.inria.fr/distrib/current/refman/"),
-        ("v8.11", "https://coq.github.io/doc/v8.11/refman/"),
-        ("v8.10", "https://coq.github.io/doc/v8.10/refman/"),
-        ("v8.9", "https://coq.github.io/doc/v8.9/refman/"),
+        ("v8.12", "https://coq.github.io/doc/v8.12/refman/"),
+        ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"),
+        ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"),
+        ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"),
         ("8.8", "https://coq.inria.fr/distrib/V8.8.2/refman/"),
         ("8.7", "https://coq.inria.fr/distrib/V8.7.2/refman/"),
         ("8.6", "https://coq.inria.fr/distrib/V8.6.1/refman/"),
@@ -356,6 +357,9 @@ latex_elements = {
 
 latex_engine = "xelatex"
 
+# Cf. https://github.com/sphinx-doc/sphinx/issues/7015
+latex_use_xindy = False
+
 ########
 # done #
 ########
diff --git a/doc/sphinx/dune b/doc/sphinx/dune
index b788fbbeed..31f28635fe 100644
--- a/doc/sphinx/dune
+++ b/doc/sphinx/dune
@@ -1,4 +1,4 @@
-(dirs :standard _static)
+(dirs :standard _static _templates)
 
 (rule
  (targets README.gen.rst)
diff --git a/ide/coq_icon.rc b/ide/coq_icon.rc
deleted file mode 100644
index f873e7de11..0000000000
--- a/ide/coq_icon.rc
+++ /dev/null
@@ -1 +0,0 @@
-large   ICON    ide/coq.ico
diff --git a/ide/FAQ b/ide/coqide/FAQ
index c8b0a5d328..c8b0a5d328 100644
--- a/ide/FAQ
+++ b/ide/coqide/FAQ
diff --git a/ide/MacOS/Info.plist.template b/ide/coqide/MacOS/Info.plist.template
index e4fb0e5980..e4fb0e5980 100644
--- a/ide/MacOS/Info.plist.template
+++ b/ide/coqide/MacOS/Info.plist.template
diff --git a/ide/MacOS/coqfile.icns b/ide/coqide/MacOS/coqfile.icns
index 107e70431d..107e70431d 100644
--- a/ide/MacOS/coqfile.icns
+++ b/ide/coqide/MacOS/coqfile.icns
diff --git a/ide/MacOS/coqide.icns b/ide/coqide/MacOS/coqide.icns
index 92bdfe773f..92bdfe773f 100644
--- a/ide/MacOS/coqide.icns
+++ b/ide/coqide/MacOS/coqide.icns
diff --git a/ide/Make b/ide/coqide/Make
index c0881ca392..c0881ca392 100644
--- a/ide/Make
+++ b/ide/coqide/Make
diff --git a/ide/config_lexer.mli b/ide/coqide/config_lexer.mli
index 196192d5be..196192d5be 100644
--- a/ide/config_lexer.mli
+++ b/ide/coqide/config_lexer.mli
diff --git a/ide/config_lexer.mll b/ide/coqide/config_lexer.mll
index 4ef9a1fafd..4ef9a1fafd 100644
--- a/ide/config_lexer.mll
+++ b/ide/coqide/config_lexer.mll
diff --git a/ide/configwin.ml b/ide/coqide/configwin.ml
index 79a1eae880..79a1eae880 100644
--- a/ide/configwin.ml
+++ b/ide/coqide/configwin.ml
diff --git a/ide/configwin.mli b/ide/coqide/configwin.mli
index b5c3e74aec..b5c3e74aec 100644
--- a/ide/configwin.mli
+++ b/ide/coqide/configwin.mli
diff --git a/ide/configwin_ihm.ml b/ide/coqide/configwin_ihm.ml
index e768131dcf..e768131dcf 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/coqide/configwin_ihm.ml
diff --git a/ide/configwin_ihm.mli b/ide/coqide/configwin_ihm.mli
index ce6cd4d7c1..ce6cd4d7c1 100644
--- a/ide/configwin_ihm.mli
+++ b/ide/coqide/configwin_ihm.mli
diff --git a/ide/configwin_messages.ml b/ide/coqide/configwin_messages.ml
index de1b4721d0..de1b4721d0 100644
--- a/ide/configwin_messages.ml
+++ b/ide/coqide/configwin_messages.ml
diff --git a/ide/configwin_types.ml b/ide/coqide/configwin_types.ml
index 711eccd08e..711eccd08e 100644
--- a/ide/configwin_types.ml
+++ b/ide/coqide/configwin_types.ml
diff --git a/ide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang
index fc7bc64a68..fc7bc64a68 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coqide/coq-ssreflect.lang
diff --git a/ide/coq.ico b/ide/coqide/coq.ico
index 94ce897d17..94ce897d17 100644
--- a/ide/coq.ico
+++ b/ide/coqide/coq.ico
diff --git a/ide/coq.lang b/ide/coqide/coq.lang
index e9eab48de7..e9eab48de7 100644
--- a/ide/coq.lang
+++ b/ide/coqide/coq.lang
diff --git a/ide/coq.ml b/ide/coqide/coq.ml
index 57cdccce6d..57cdccce6d 100644
--- a/ide/coq.ml
+++ b/ide/coqide/coq.ml
diff --git a/ide/coq.mli b/ide/coqide/coq.mli
index 82df36c91c..82df36c91c 100644
--- a/ide/coq.mli
+++ b/ide/coqide/coq.mli
diff --git a/ide/coq.png b/ide/coqide/coq.png
index 136bfdd5fe..136bfdd5fe 100644
--- a/ide/coq.png
+++ b/ide/coqide/coq.png
diff --git a/ide/coq2.ico b/ide/coqide/coq2.ico
index bc1732fd99..bc1732fd99 100644
--- a/ide/coq2.ico
+++ b/ide/coqide/coq2.ico
diff --git a/ide/coqOps.ml b/ide/coqide/coqOps.ml
index 29ea3ce9ea..29ea3ce9ea 100644
--- a/ide/coqOps.ml
+++ b/ide/coqide/coqOps.ml
diff --git a/ide/coqOps.mli b/ide/coqide/coqOps.mli
index 3a4678ae9c..3a4678ae9c 100644
--- a/ide/coqOps.mli
+++ b/ide/coqide/coqOps.mli
diff --git a/ide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 711986c2b2..711986c2b2 100644
--- a/ide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
diff --git a/ide/coq_commands.mli b/ide/coqide/coq_commands.mli
index 4fa30bbe46..4fa30bbe46 100644
--- a/ide/coq_commands.mli
+++ b/ide/coqide/coq_commands.mli
diff --git a/ide/coqide/coq_icon.rc b/ide/coqide/coq_icon.rc
new file mode 100644
index 0000000000..3e8b8aaecc
--- /dev/null
+++ b/ide/coqide/coq_icon.rc
@@ -0,0 +1 @@
+large   ICON    ide/coqide/coq.ico
diff --git a/ide/coq_lex.mli b/ide/coqide/coq_lex.mli
index 142dd6e92c..142dd6e92c 100644
--- a/ide/coq_lex.mli
+++ b/ide/coqide/coq_lex.mli
diff --git a/ide/coq_lex.mll b/ide/coqide/coq_lex.mll
index fe9f108a94..fe9f108a94 100644
--- a/ide/coq_lex.mll
+++ b/ide/coqide/coq_lex.mll
diff --git a/ide/coq_style.xml b/ide/coqide/coq_style.xml
index 67631d3462..67631d3462 100644
--- a/ide/coq_style.xml
+++ b/ide/coqide/coq_style.xml
diff --git a/ide/coqide.ml b/ide/coqide/coqide.ml
index ab2a17798e..ab2a17798e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide/coqide.ml
diff --git a/ide/coqide.mli b/ide/coqide/coqide.mli
index ac92afed1f..ac92afed1f 100644
--- a/ide/coqide.mli
+++ b/ide/coqide/coqide.mli
diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide/coqide_QUARTZ.ml.in
index fe35906bdc..fe35906bdc 100644
--- a/ide/coqide_QUARTZ.ml.in
+++ b/ide/coqide/coqide_QUARTZ.ml.in
diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide/coqide_WIN32.ml.in
index be8aab9e49..be8aab9e49 100644
--- a/ide/coqide_WIN32.ml.in
+++ b/ide/coqide/coqide_WIN32.ml.in
diff --git a/ide/coqide_X11.ml.in b/ide/coqide/coqide_X11.ml.in
index 76cd880ddc..76cd880ddc 100644
--- a/ide/coqide_X11.ml.in
+++ b/ide/coqide/coqide_X11.ml.in
diff --git a/ide/coqide_main.ml b/ide/coqide/coqide_main.ml
index 0812e00960..0812e00960 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide/coqide_main.ml
diff --git a/ide/coqide_main.mli b/ide/coqide/coqide_main.mli
index eeb4eb64bd..eeb4eb64bd 100644
--- a/ide/coqide_main.mli
+++ b/ide/coqide/coqide_main.mli
diff --git a/ide/coqide_os_specific.mli b/ide/coqide/coqide_os_specific.mli
index b86800dd50..b86800dd50 100644
--- a/ide/coqide_os_specific.mli
+++ b/ide/coqide/coqide_os_specific.mli
diff --git a/ide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
index e9ff1bbba1..e9ff1bbba1 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide/coqide_ui.ml
diff --git a/ide/coqide_ui.mli b/ide/coqide/coqide_ui.mli
index 9e4606072d..9e4606072d 100644
--- a/ide/coqide_ui.mli
+++ b/ide/coqide/coqide_ui.mli
diff --git a/ide/default_bindings_src.ml b/ide/coqide/default_bindings_src.ml
index a69a7c2aba..a69a7c2aba 100644
--- a/ide/default_bindings_src.ml
+++ b/ide/coqide/default_bindings_src.ml
diff --git a/ide/document.ml b/ide/coqide/document.ml
index 096c4940fa..096c4940fa 100644
--- a/ide/document.ml
+++ b/ide/coqide/document.ml
diff --git a/ide/document.mli b/ide/coqide/document.mli
index b7f23115f6..b7f23115f6 100644
--- a/ide/document.mli
+++ b/ide/coqide/document.mli
diff --git a/ide/dune b/ide/coqide/dune
index 12bad7ebc4..12bad7ebc4 100644
--- a/ide/dune
+++ b/ide/coqide/dune
diff --git a/ide/fake_ide.ml b/ide/coqide/fake_ide.ml
index e1736a5fe0..e1736a5fe0 100644
--- a/ide/fake_ide.ml
+++ b/ide/coqide/fake_ide.ml
diff --git a/ide/fileOps.ml b/ide/coqide/fileOps.ml
index 0ac14167e5..0ac14167e5 100644
--- a/ide/fileOps.ml
+++ b/ide/coqide/fileOps.ml
diff --git a/ide/fileOps.mli b/ide/coqide/fileOps.mli
index cf8084af5c..cf8084af5c 100644
--- a/ide/fileOps.mli
+++ b/ide/coqide/fileOps.mli
diff --git a/ide/gtk_parsing.ml b/ide/coqide/gtk_parsing.ml
index decd24d407..decd24d407 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/coqide/gtk_parsing.ml
diff --git a/ide/gtk_parsing.mli b/ide/coqide/gtk_parsing.mli
index 501afde8ac..501afde8ac 100644
--- a/ide/gtk_parsing.mli
+++ b/ide/coqide/gtk_parsing.mli
diff --git a/ide/ide.mllib b/ide/coqide/ide.mllib
index f8e8ff48d6..f8e8ff48d6 100644
--- a/ide/ide.mllib
+++ b/ide/coqide/ide.mllib
diff --git a/ide/ide_common.mllib b/ide/coqide/ide_common.mllib
index 050c282ef6..050c282ef6 100644
--- a/ide/ide_common.mllib
+++ b/ide/coqide/ide_common.mllib
diff --git a/ide/ide_win32_stubs.c b/ide/coqide/ide_win32_stubs.c
index f430c9f2b6..f430c9f2b6 100644
--- a/ide/ide_win32_stubs.c
+++ b/ide/coqide/ide_win32_stubs.c
diff --git a/ide/idetop.ml b/ide/coqide/idetop.ml
index bd99cbed1b..bd99cbed1b 100644
--- a/ide/idetop.ml
+++ b/ide/coqide/idetop.ml
diff --git a/ide/ideutils.ml b/ide/coqide/ideutils.ml
index 482cecc1f8..482cecc1f8 100644
--- a/ide/ideutils.ml
+++ b/ide/coqide/ideutils.ml
diff --git a/ide/ideutils.mli b/ide/coqide/ideutils.mli
index 9a17eb1402..9a17eb1402 100644
--- a/ide/ideutils.mli
+++ b/ide/coqide/ideutils.mli
diff --git a/ide/macos_prehook.ml b/ide/coqide/macos_prehook.ml
index dc8fd0e85d..dc8fd0e85d 100644
--- a/ide/macos_prehook.ml
+++ b/ide/coqide/macos_prehook.ml
diff --git a/ide/macos_prehook.mli b/ide/coqide/macos_prehook.mli
index eeb4eb64bd..eeb4eb64bd 100644
--- a/ide/macos_prehook.mli
+++ b/ide/coqide/macos_prehook.mli
diff --git a/ide/microPG.ml b/ide/coqide/microPG.ml
index 5a4871b70a..5a4871b70a 100644
--- a/ide/microPG.ml
+++ b/ide/coqide/microPG.ml
diff --git a/ide/microPG.mli b/ide/coqide/microPG.mli
index f79a52f0ef..f79a52f0ef 100644
--- a/ide/microPG.mli
+++ b/ide/coqide/microPG.mli
diff --git a/ide/minilib.ml b/ide/coqide/minilib.ml
index cb7a590bd6..cb7a590bd6 100644
--- a/ide/minilib.ml
+++ b/ide/coqide/minilib.ml
diff --git a/ide/minilib.mli b/ide/coqide/minilib.mli
index 1c3be00817..1c3be00817 100644
--- a/ide/minilib.mli
+++ b/ide/coqide/minilib.mli
diff --git a/ide/preferences.ml b/ide/coqide/preferences.ml
index 5a77f4ebcf..5a77f4ebcf 100644
--- a/ide/preferences.ml
+++ b/ide/coqide/preferences.ml
diff --git a/ide/preferences.mli b/ide/coqide/preferences.mli
index 895d7a7876..895d7a7876 100644
--- a/ide/preferences.mli
+++ b/ide/coqide/preferences.mli
diff --git a/ide/protocol/dune b/ide/coqide/protocol/dune
index 801ceb20ec..801ceb20ec 100644
--- a/ide/protocol/dune
+++ b/ide/coqide/protocol/dune
diff --git a/ide/protocol/ideprotocol.mllib b/ide/coqide/protocol/ideprotocol.mllib
index 8317a08681..8317a08681 100644
--- a/ide/protocol/ideprotocol.mllib
+++ b/ide/coqide/protocol/ideprotocol.mllib
diff --git a/ide/protocol/interface.ml b/ide/coqide/protocol/interface.ml
index 646012dcaa..646012dcaa 100644
--- a/ide/protocol/interface.ml
+++ b/ide/coqide/protocol/interface.ml
diff --git a/ide/protocol/richpp.ml b/ide/coqide/protocol/richpp.ml
index 7aa38792fc..7aa38792fc 100644
--- a/ide/protocol/richpp.ml
+++ b/ide/coqide/protocol/richpp.ml
diff --git a/ide/protocol/richpp.mli b/ide/coqide/protocol/richpp.mli
index 3b83e7b15c..3b83e7b15c 100644
--- a/ide/protocol/richpp.mli
+++ b/ide/coqide/protocol/richpp.mli
diff --git a/ide/protocol/serialize.ml b/ide/coqide/protocol/serialize.ml
index bdbec5b30f..bdbec5b30f 100644
--- a/ide/protocol/serialize.ml
+++ b/ide/coqide/protocol/serialize.ml
diff --git a/ide/protocol/serialize.mli b/ide/coqide/protocol/serialize.mli
index 5d88defe55..5d88defe55 100644
--- a/ide/protocol/serialize.mli
+++ b/ide/coqide/protocol/serialize.mli
diff --git a/ide/protocol/xml_lexer.mli b/ide/coqide/protocol/xml_lexer.mli
index 920de9f9c3..920de9f9c3 100644
--- a/ide/protocol/xml_lexer.mli
+++ b/ide/coqide/protocol/xml_lexer.mli
diff --git a/ide/protocol/xml_lexer.mll b/ide/coqide/protocol/xml_lexer.mll
index e8bf7e16ae..e8bf7e16ae 100644
--- a/ide/protocol/xml_lexer.mll
+++ b/ide/coqide/protocol/xml_lexer.mll
diff --git a/ide/protocol/xml_parser.ml b/ide/coqide/protocol/xml_parser.ml
index 8db3f9e8ba..8db3f9e8ba 100644
--- a/ide/protocol/xml_parser.ml
+++ b/ide/coqide/protocol/xml_parser.ml
diff --git a/ide/protocol/xml_parser.mli b/ide/coqide/protocol/xml_parser.mli
index ac2eab352f..ac2eab352f 100644
--- a/ide/protocol/xml_parser.mli
+++ b/ide/coqide/protocol/xml_parser.mli
diff --git a/ide/protocol/xml_printer.ml b/ide/coqide/protocol/xml_printer.ml
index f526618a6e..f526618a6e 100644
--- a/ide/protocol/xml_printer.ml
+++ b/ide/coqide/protocol/xml_printer.ml
diff --git a/ide/protocol/xml_printer.mli b/ide/coqide/protocol/xml_printer.mli
index e60e3392ed..e60e3392ed 100644
--- a/ide/protocol/xml_printer.mli
+++ b/ide/coqide/protocol/xml_printer.mli
diff --git a/ide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 6cb0cec008..6cb0cec008 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
diff --git a/ide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli
index 44584d44d7..44584d44d7 100644
--- a/ide/protocol/xmlprotocol.mli
+++ b/ide/coqide/protocol/xmlprotocol.mli
diff --git a/ide/sentence.ml b/ide/coqide/sentence.ml
index 2e00342473..2e00342473 100644
--- a/ide/sentence.ml
+++ b/ide/coqide/sentence.ml
diff --git a/ide/sentence.mli b/ide/coqide/sentence.mli
index adaa7c5d2f..adaa7c5d2f 100644
--- a/ide/sentence.mli
+++ b/ide/coqide/sentence.mli
diff --git a/ide/session.ml b/ide/coqide/session.ml
index 09391b7f50..09391b7f50 100644
--- a/ide/session.ml
+++ b/ide/coqide/session.ml
diff --git a/ide/session.mli b/ide/coqide/session.mli
index 9c0a8760c3..9c0a8760c3 100644
--- a/ide/session.mli
+++ b/ide/coqide/session.mli
diff --git a/ide/tags.ml b/ide/coqide/tags.ml
index 82e63e84a5..82e63e84a5 100644
--- a/ide/tags.ml
+++ b/ide/coqide/tags.ml
diff --git a/ide/tags.mli b/ide/coqide/tags.mli
index 61109c6d60..61109c6d60 100644
--- a/ide/tags.mli
+++ b/ide/coqide/tags.mli
diff --git a/ide/unicode_bindings.ml b/ide/coqide/unicode_bindings.ml
index 39d58825df..39d58825df 100644
--- a/ide/unicode_bindings.ml
+++ b/ide/coqide/unicode_bindings.ml
diff --git a/ide/unicode_bindings.mli b/ide/coqide/unicode_bindings.mli
index 30c6d91fa0..30c6d91fa0 100644
--- a/ide/unicode_bindings.mli
+++ b/ide/coqide/unicode_bindings.mli
diff --git a/ide/utf8_convert.mli b/ide/coqide/utf8_convert.mli
index f1d8aedecb..f1d8aedecb 100644
--- a/ide/utf8_convert.mli
+++ b/ide/coqide/utf8_convert.mli
diff --git a/ide/utf8_convert.mll b/ide/coqide/utf8_convert.mll
index db02bd8116..db02bd8116 100644
--- a/ide/utf8_convert.mll
+++ b/ide/coqide/utf8_convert.mll
diff --git a/ide/wg_Command.ml b/ide/coqide/wg_Command.ml
index 30924adc4a..30924adc4a 100644
--- a/ide/wg_Command.ml
+++ b/ide/coqide/wg_Command.ml
diff --git a/ide/wg_Command.mli b/ide/coqide/wg_Command.mli
index e2854cc6d5..e2854cc6d5 100644
--- a/ide/wg_Command.mli
+++ b/ide/coqide/wg_Command.mli
diff --git a/ide/wg_Completion.ml b/ide/coqide/wg_Completion.ml
index cc24e71386..cc24e71386 100644
--- a/ide/wg_Completion.ml
+++ b/ide/coqide/wg_Completion.ml
diff --git a/ide/wg_Completion.mli b/ide/coqide/wg_Completion.mli
index 8bb34fbbca..8bb34fbbca 100644
--- a/ide/wg_Completion.mli
+++ b/ide/coqide/wg_Completion.mli
diff --git a/ide/wg_Detachable.ml b/ide/coqide/wg_Detachable.ml
index efb10293bd..efb10293bd 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/coqide/wg_Detachable.ml
diff --git a/ide/wg_Detachable.mli b/ide/coqide/wg_Detachable.mli
index 09b4ac732d..09b4ac732d 100644
--- a/ide/wg_Detachable.mli
+++ b/ide/coqide/wg_Detachable.mli
diff --git a/ide/wg_Find.ml b/ide/coqide/wg_Find.ml
index 7e89191bd1..7e89191bd1 100644
--- a/ide/wg_Find.ml
+++ b/ide/coqide/wg_Find.ml
diff --git a/ide/wg_Find.mli b/ide/coqide/wg_Find.mli
index 2a26230a6a..2a26230a6a 100644
--- a/ide/wg_Find.mli
+++ b/ide/coqide/wg_Find.mli
diff --git a/ide/wg_MessageView.ml b/ide/coqide/wg_MessageView.ml
index 6e22172d05..6e22172d05 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/coqide/wg_MessageView.ml
diff --git a/ide/wg_MessageView.mli b/ide/coqide/wg_MessageView.mli
index 054dd0e571..054dd0e571 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/coqide/wg_MessageView.mli
diff --git a/ide/wg_Notebook.ml b/ide/coqide/wg_Notebook.ml
index 9662880210..9662880210 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/coqide/wg_Notebook.ml
diff --git a/ide/wg_Notebook.mli b/ide/coqide/wg_Notebook.mli
index d3907f43ad..d3907f43ad 100644
--- a/ide/wg_Notebook.mli
+++ b/ide/coqide/wg_Notebook.mli
diff --git a/ide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml
index 1de63953af..1de63953af 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/coqide/wg_ProofView.ml
diff --git a/ide/wg_ProofView.mli b/ide/coqide/wg_ProofView.mli
index 8217f72066..8217f72066 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/coqide/wg_ProofView.mli
diff --git a/ide/wg_RoutedMessageViews.ml b/ide/coqide/wg_RoutedMessageViews.ml
index f141343c5d..f141343c5d 100644
--- a/ide/wg_RoutedMessageViews.ml
+++ b/ide/coqide/wg_RoutedMessageViews.ml
diff --git a/ide/wg_RoutedMessageViews.mli b/ide/coqide/wg_RoutedMessageViews.mli
index bf9893852a..bf9893852a 100644
--- a/ide/wg_RoutedMessageViews.mli
+++ b/ide/coqide/wg_RoutedMessageViews.mli
diff --git a/ide/wg_ScriptView.ml b/ide/coqide/wg_ScriptView.ml
index 62d58a5f23..62d58a5f23 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/coqide/wg_ScriptView.ml
diff --git a/ide/wg_ScriptView.mli b/ide/coqide/wg_ScriptView.mli
index 849c308941..849c308941 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/coqide/wg_ScriptView.mli
diff --git a/ide/wg_Segment.ml b/ide/coqide/wg_Segment.ml
index f115da662e..f115da662e 100644
--- a/ide/wg_Segment.ml
+++ b/ide/coqide/wg_Segment.ml
diff --git a/ide/wg_Segment.mli b/ide/coqide/wg_Segment.mli
index 9464b596e5..9464b596e5 100644
--- a/ide/wg_Segment.mli
+++ b/ide/coqide/wg_Segment.mli
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 36dc01e272..366203faeb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -382,19 +382,19 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else None, x in
     match sk1, sk2 with
     | [], [] -> None, Success i
-    | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
+    | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
       (match f env i CONV t1 t2 with
       | Success i' ->
         (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
         | Success i'' -> ise_stack2 true i'' q1 q2
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
-    | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 ->
+    | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
        if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
-    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
-      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
+    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
+      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
       if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
         match ise_and i [
           (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
@@ -417,13 +417,13 @@ let exact_ise_stack2 env evd f sk1 sk2 =
   let rec ise_stack2 i sk1 sk2 =
     match sk1, sk2 with
     | [], [] -> Success i
-    | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
+    | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
       ise_and i [
       (fun i -> ise_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
       (fun i -> f env i CONV t1 t2)]
-    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
-      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
+    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
+      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
       if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
         ise_and i [
           (fun i -> ise_stack2 i q1 q2);
@@ -431,7 +431,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
           (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
           (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
-    | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 ->
+    | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
        if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
@@ -556,9 +556,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       flags.open_ts env' evd (c'1, Stack.empty) in
-    let out2, _ = whd_nored_state env' evd
-      (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
-      Cst_stack.empty in
+    let out2 = whd_nored_state env' evd
+      (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty) in
     if onleft then evar_eqappr_x flags env' evd CONV out1 out2
     else evar_eqappr_x flags env' evd CONV out2 out1
   in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 15bf9667b3..8ab040b3b1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -24,11 +24,7 @@ open Context.Rel.Declaration
 exception Elimconst
 
 (** This module implements a call by name reduction used by (at
-    least) evarconv unification and cbn tactic.
-
-    It has an ability to "refold" constants by storing constants and
-    their parameters in its stack.
-*)
+    least) evarconv unification. *)
 
 (** Support for reduction effects *)
 
@@ -174,71 +170,6 @@ module ReductionBehaviour = struct
 
 end
 
-(** Machinery about stack of unfolded constants *)
-module Cst_stack = struct
-  open EConstr
-
-(** constant * params * args
-
-- constant applied to params = term in head applied to args
-- there is at most one arguments with an empty list of args, it must be the first.
-- in args, the int represents the indice of the first arg to consider *)
-  type t = (constr * constr list * (int * constr array) list)  list
-
-  let empty = []
-  let is_empty = CList.is_empty
-
-  let drop_useless = function
-    | _ :: ((_,_,[])::_ as q) -> q
-    | l -> l
-
-  let add_param h cst_l =
-    let append2cst = function
-      | (c,params,[]) -> (c, h::params, [])
-      | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
-        (c, params, q)
-      | (c,params,(i,t)::q) ->
-        (c, params, (succ i,t)::q)
-    in
-      drop_useless (List.map append2cst cst_l)
-
-  let add_args cl =
-    List.map (fun (a,b,args) -> (a,b,(0,cl)::args))
-
-  let add_cst cst = function
-    | (_,_,[]) :: q as l -> l
-    | l -> (cst,[],[])::l
-
-  let best_cst = function
-    | (cst,params,[])::_ -> Some(cst,params)
-    | _ -> None
-
-  let reference sigma t = match best_cst t with
-    | Some (c, _) when isConst sigma c -> Some (fst (destConst sigma c))
-    | _ -> None
-
-  (** [best_replace d cst_l c] makes the best replacement for [d]
-      by [cst_l] in [c] *)
-  let best_replace sigma d cst_l c =
-    let reconstruct_head = List.fold_left
-      (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
-    List.fold_right
-      (fun (cst,params,args) t -> Termops.replace_term sigma
-        (reconstruct_head d args)
-        (applist (cst, List.rev params))
-        t) cst_l c
-
-  let pr env sigma l =
-    let open Pp in
-    let p_c c = Termops.Internal.print_constr_env env sigma c in
-    prlist_with_sep pr_semicolon
-      (fun (c,params,args) ->
-        hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
-                 pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++
-                 str ")")) l
-end
-
-
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 module Stack :
 sig
@@ -246,17 +177,12 @@ sig
   type 'a app_node
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
-  type cst_member =
-    | Cst_const of pconstant
-    | Cst_proj of Projection.t
-
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of Projection.t * Cst_stack.t
-  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
-  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
-  | Cst of cst_member * int * int list * 'a t * Cst_stack.t
+  | Case of case_info * 'a * 'a array
+  | Proj of Projection.t
+  | Fix of ('a, 'a) pfixpoint * 'a t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
 
   and 'a t = 'a member list
 
@@ -268,8 +194,6 @@ sig
   val append_app : 'a array -> 'a t -> 'a t
   val decomp : 'a t -> ('a * 'a t) option
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
-  val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
-    -> 'a t -> 'a t -> bool
   val compare_shape : 'a t -> 'a t -> bool
   val map : ('a -> 'a) -> 'a t -> 'a t
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
@@ -278,14 +202,12 @@ sig
   val strip_app : 'a t -> 'a t * 'a t
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
   val not_purely_applicative : 'a t -> bool
-  val will_expose_iota : 'a t -> bool
   val list_of_app_stack : constr t -> constr list option
   val assign : 'a t -> int -> 'a -> 'a t
   val args_size : 'a t -> int
   val tail : int -> 'a t -> 'a t
   val nth : 'a t -> int -> 'a
-  val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
-  val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
+  val zip : evar_map -> constr * constr t -> constr
   val check_native_args : CPrimitives.t -> 'a t -> bool
   val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option
 end =
@@ -307,17 +229,12 @@ struct
                      )
 
 
-  type cst_member =
-    | Cst_const of pconstant
-    | Cst_proj of Projection.t
-
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of Projection.t * Cst_stack.t
-  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
-  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
-  | Cst of cst_member * int * int list * 'a t * Cst_stack.t
+  | Case of case_info * 'a * 'a array
+  | Proj of Projection.t
+  | Fix of ('a, 'a) pfixpoint * 'a t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
 
   and 'a t = 'a member list
 
@@ -327,37 +244,22 @@ struct
     let pr_c x = hov 1 (pr_c x) in
     match member with
     | App app -> str "ZApp" ++ pr_app_node pr_c app
-    | Case (_,_,br,cst) ->
+    | Case (_,_,br) ->
        str "ZCase(" ++
          prvect_with_sep (pr_bar) pr_c br
        ++ str ")"
-    | Proj (p,cst) ->
+    | Proj p  ->
       str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
-    | Fix (f,args,cst) ->
+    | Fix (f,args) ->
        str "ZFix(" ++ Constr.debug_print_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
-    | Primitive (p,c,args,kargs,cst_l) ->
+    | Primitive (p,c,args,kargs) ->
       str "ZPrimitive(" ++ str (CPrimitives.to_string p)
       ++ pr_comma () ++ pr pr_c args ++ str ")"
-    | Cst (mem,curr,remains,params,cst_l) ->
-      str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
-      ++ pr_comma () ++
-        prlist_with_sep pr_semicolon int remains ++
-        pr_comma () ++ pr pr_c params ++ str ")"
   and pr pr_c l =
     let open Pp in
     prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
 
-  and pr_cst_member pr_c c =
-    let open Pp in
-      match c with
-      | Cst_const (c, u) ->
-        if Univ.Instance.is_empty u then Constant.debug_print c
-        else str"(" ++ Constant.debug_print c ++ str ", " ++
-          Univ.Instance.pr Univ.Level.pr u ++ str")"
-      | Cst_proj p ->
-        str".(" ++ Constant.debug_print (Projection.constant p) ++ str")"
-
   let empty = []
   let is_empty = CList.is_empty
 
@@ -377,54 +279,21 @@ struct
     if i < j then (l.(j), App (i,l,pred j) :: sk)
     else (l.(j), sk)
 
-  let equal f f_fix sk1 sk2 =
-    let equal_cst_member x y =
-      match x, y with
-      | Cst_const (c1,u1), Cst_const (c2, u2) ->
-        Constant.equal c1 c2 && Univ.Instance.equal u1 u2
-      | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
-      | _, _ -> false
-    in
-    let rec equal_rec sk1 sk2 =
-      match sk1,sk2 with
-      | [],[] -> true
-      | App a1 :: s1, App a2 :: s2 ->
-        let t1,s1' = decomp_node_last a1 s1 in
-        let t2,s2' = decomp_node_last a2 s2 in
-        (f t1 t2) && (equal_rec s1' s2')
-      | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 ->
-        f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
-      | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
-        Projection.Repr.equal (Projection.repr p) (Projection.repr p2)
-        && equal_rec s1 s2
-      | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
-        f_fix f1 f2
-          && equal_rec (List.rev s1) (List.rev s2)
-          && equal_rec s1' s2'
-      | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' ->
-        equal_cst_member c1 c2
-          && equal_rec (List.rev params1) (List.rev params2)
-          && equal_rec s1' s2'
-      | ((App _|Case _|Proj _|Fix _|Cst _|Primitive _)::_|[]), _ -> false
-    in equal_rec (List.rev sk1) (List.rev sk2)
-
   let compare_shape stk1 stk2 =
     let rec compare_rec bal stk1 stk2 =
       match (stk1,stk2) with
         ([],[]) -> Int.equal bal 0
       | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
-      | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
+      | (Case(c1,_,_)::s1, Case(c2,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
-      | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
+      | (Proj (p)::s1, Proj(p2)::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
-      | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) ->
+      | (Fix(_,a1)::s1, Fix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-      | (Primitive(_,_,a1,_,_)::s1, Primitive(_,_,a2,_,_)::s2) ->
+      | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-      | (Cst (_,_,_,p1,_)::s1, Cst (_,_,_,p2,_)::s2) ->
-        Int.equal bal 0 && compare_rec 0 p1 p2 && compare_rec 0 s1 s2
-      | ((Case _|Proj _|Fix _|Cst _|Primitive _) :: _ | []) ,_ -> false in
+      | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in
     compare_rec 0 stk1 stk2
 
   exception IncompatibleFold2
@@ -436,32 +305,27 @@ struct
         let t1,l1 = decomp_node_last n1 q1 in
         let t2,l2 = decomp_node_last n2 q2 in
         aux (f o t1 t2) l1 l2
-      | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 ->
+      | Case (_,t1,a1) :: q1, Case (_,t2,a2) :: q2 ->
         aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
-      | Proj (p1,_) :: q1, Proj (p2,_) :: q2 ->
+      | Proj (p1) :: q1, Proj (p2) :: q2 ->
         aux o q1 q2
-      | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 ->
+      | Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 ->
         let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in
         aux o' q1 q2
-      | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 ->
-        let o' = aux o (List.rev params1) (List.rev params2) in
-        aux o' q1 q2
-      | (((App _|Case _|Proj _|Fix _|Cst _|Primitive _) :: _|[]), _) ->
+      | (((App _|Case _|Proj _|Fix _|Primitive _) :: _|[]), _) ->
               raise IncompatibleFold2
     in aux o (List.rev sk1) (List.rev sk2)
 
   let rec map f x = List.map (function
-                               | (Proj (_,_)) as e -> e
+                               | (Proj (_)) as e -> e
                                | App (i,a,j) ->
                                   let le = j - i + 1 in
                                   App (0,Array.map f (Array.sub a i le), le-1)
-                               | Case (info,ty,br,alt) -> Case (info, f ty, Array.map f br, alt)
-                               | Fix ((r,(na,ty,bo)),arg,alt) ->
-                                  Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt)
-                               | Cst (cst,curr,remains,params,alt) ->
-                                 Cst (cst,curr,remains,map f params,alt)
-                               | Primitive (p,c,args,kargs,cst_l) ->
-                                 Primitive(p,c, map f args, kargs, cst_l)
+                               | Case (info,ty,br) -> Case (info, f ty, Array.map f br)
+                               | Fix ((r,(na,ty,bo)),arg) ->
+                                  Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg)
+                               | Primitive (p,c,args,kargs) ->
+                                 Primitive(p,c, map f args, kargs)
     ) x
 
   let append_app_list l s =
@@ -470,7 +334,7 @@ struct
 
   let rec args_size = function
     | App (i,_,j)::s -> j + 1 - i + args_size s
-    | (Case _|Fix _|Proj _|Cst _|Primitive _)::_ | [] -> 0
+    | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0
 
   let strip_app s =
     let rec aux out = function
@@ -493,13 +357,8 @@ struct
     in aux n [] s
 
   let not_purely_applicative args =
-    List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true
+    List.exists (function (Fix _ | Case _ | Proj _ ) -> true
                           | App _ | Primitive _ -> false) args
-  let will_expose_iota args =
-    List.exists
-      (function (Fix (_,_,l) | Case (_,_,_,l) |
-                 Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
-      args
 
   let list_of_app_stack s =
     let rec aux = function
@@ -536,27 +395,7 @@ struct
     | Some (_,el,_) -> el
     | None -> raise Not_found
 
-  (** This function breaks the abstraction of Cst_stack ! *)
-  let best_state sigma (_,sk as s) l =
-    let rec aux sk def = function
-      |(cst, params, []) -> (cst, append_app_list (List.rev params) sk)
-      |(cst, params, (i,t)::q) -> match decomp sk with
-        | Some (el,sk') when EConstr.eq_constr sigma el t.(i) ->
-          if i = pred (Array.length t)
-          then aux sk' def (cst, params, q)
-          else aux sk' def (cst, params, (succ i,t)::q)
-        | _ -> def
-    in List.fold_left (aux sk) s l
-
-  let constr_of_cst_member f sk =
-    match f with
-    | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk
-    | Cst_proj p ->
-      match decomp sk with
-      | Some (hd, sk) -> mkProj (p, hd), sk
-      | None -> assert false
-
-  let zip ?(refold=false) sigma s =
+  let zip sigma s =
   let rec zip = function
     | f, [] -> f
     | f, (App (i,a,j) :: s) ->
@@ -564,21 +403,11 @@ struct
                 then a
                 else Array.sub a i (j - i + 1) in
        zip (mkApp (f, a'), s)
-    | f, (Case (ci,rt,br,cst_l)::s) when refold ->
-      zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l)
-    | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s)
-    | f, (Fix (fix,st,cst_l)::s) when refold ->
-      zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
-  | f, (Fix (fix,st,_)::s) -> zip
+    | f, (Case (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s)
+  | f, (Fix (fix,st)::s) -> zip
     (mkFix fix, st @ (append_app [|f|] s))
-  | f, (Cst (cst,_,_,params,cst_l)::s) when refold ->
-    zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
-  | f, (Cst (cst,_,_,params,_)::s) ->
-    zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
-  | f, (Proj (p,cst_l)::s) when refold ->
-    zip (best_state sigma (mkProj (p,f),s) cst_l)
-  | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s)
-  | f, (Primitive (p,c,args,kargs,cst_l)::s) ->
+  | f, (Proj (p)::s) -> zip (mkProj (p,f),s)
+  | f, (Primitive (p,c,args,kargs)::s) ->
       zip (mkConstU c, args @ append_app [|f|] s)
   in
   zip s
@@ -656,17 +485,16 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA]
 
 (* Beta Reduction tools *)
 
-let apply_subst recfun env sigma refold cst_l t stack =
-  let rec aux env cst_l t stack =
+let apply_subst recfun env sigma t stack =
+  let rec aux env t stack =
     match (Stack.decomp stack, EConstr.kind sigma t) with
     | Some (h,stacktl), Lambda (_,_,c) ->
-       let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
-       aux (h::env) cst_l' c stacktl
-    | _ -> recfun sigma cst_l (substl env t, stack)
-  in aux env cst_l t stack
+       aux (h::env) c stacktl
+    | _ -> recfun sigma (substl env t, stack)
+  in aux env t stack
 
 let stacklam recfun env sigma t stack =
-  apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
+  apply_subst (fun _ s -> recfun s) env sigma t stack
 
 let beta_applist sigma (c,l) =
   let zip s = Stack.zip sigma s in
@@ -685,73 +513,25 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
   | Construct _ | CoFix _ -> true
   | _  -> false
 
-(** @return c if there is a constant c whose body is bd
-    @return bd else.
-
-    It has only a meaning because internal representation of "Fixpoint f x
-    := t" is Definition f := fix f x => t
-
-    Even more fragile that we could hope because do Module M. Fixpoint
-    f x := t. End M. Definition f := u. and say goodbye to any hope
-    of refolding M.f this way ...
-*)
-let magically_constant_of_fixbody env sigma reference bd = function
-  | Name.Anonymous -> bd
-  | Name.Name id ->
-    let open UnivProblem in
-    let (cst_mod,_) = Constant.repr2 reference in
-    let cst = Constant.make2 cst_mod (Label.of_id id) in
-    if not (Environ.mem_constant cst env) then bd
-    else
-      let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
-      match constant_opt_value_in env (cst,u) with
-      | None -> bd
-      | Some t ->
-        let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
-        begin match csts with
-          | Some csts ->
-            let subst = Set.fold (fun cst acc ->
-                let l, r = match cst with
-                  | ULub (u, v) | UWeak (u, v) -> u, v
-                  | UEq (u, v) | ULe (u, v) ->
-                    let get u = Option.get (Universe.level u) in
-                    get u, get v
-                in
-                Univ.LMap.add l r acc)
-                csts Univ.LMap.empty
-            in
-            let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-            mkConstU (cst, EInstance.make inst)
-          | None -> bd
-        end
-
-let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j =
     let ind = nbodies-j-1 in
     if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
     else
       let bd = mkCoFix (ind,typedbodies) in
-      match env with
-      | None -> bd
-      | Some e ->
-        match reference with
-        | None -> bd
-        | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+      bd
+  in
   let closure = List.init nbodies make_Fi in
   substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
+let reduce_and_refold_cofix recfun env sigma cofix sk =
   let raw_answer =
-    let env = if refold then Some env else None in
-    contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
+    contract_cofix sigma cofix in
   apply_subst
-    (fun sigma x (t,sk') ->
-      let t' =
-        if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
-      recfun x (t',sk'))
-    [] sigma refold Cst_stack.empty raw_answer sk
+    (fun _ (t,sk') -> recfun (t,sk'))
+    [] sigma raw_answer sk
 
 let reduce_mind_case sigma mia =
   match EConstr.kind sigma mia.mconstr with
@@ -767,19 +547,15 @@ let reduce_mind_case sigma mia =
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies)) =
     let nbodies = Array.length recindices in
     let make_Fi j =
       let ind = nbodies-j-1 in
       if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
       else
         let bd = mkFix ((recindices,ind),typedbodies) in
-        match env with
-        | None -> bd
-        | Some e ->
-          match reference with
-          | None -> bd
-          | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+        bd
+    in
     let closure = List.init nbodies make_Fi in
     substl closure bodies.(bodynum)
 
@@ -787,18 +563,12 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
-let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
+let reduce_and_refold_fix recfun env sigma fix sk =
   let raw_answer =
-    let env = if refold then Some env else None in
-    contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
+    contract_fix sigma fix in
   apply_subst
-    (fun sigma x (t,sk') ->
-      let t' =
-        if refold then
-          Cst_stack.best_replace sigma (mkFix fix) cst_l t
-        else t
-      in recfun x (t',sk'))
-    [] sigma refold Cst_stack.empty raw_answer sk
+    (fun _ (t,sk') -> recfun (t,sk'))
+    [] sigma raw_answer sk
 
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum && bodynum < Array.length recindices);
@@ -952,21 +722,14 @@ let debug_RAKAM =
     ~key:["Debug";"RAKAM"]
     ~value:false
 
-let equal_stacks sigma (x, l) (y, l') =
-  let f_equal x y = eq_constr sigma x y in
-  let eq_fix a b = f_equal (mkFix a) (mkFix b) in
-  Stack.equal f_equal eq_fix l l' && f_equal x y
-
-let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
+let rec whd_state_gen flags env sigma =
   let open Context.Named.Declaration in
-  let open ReductionBehaviour in
-  let rec whrec cst_l (x, stack) =
+  let rec whrec (x, stack) : state =
     let () = if debug_RAKAM () then
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
         Feedback.msg_debug
              (h 0 (str "<<" ++ pr x ++
-                   str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
                    str ">>"))
     in
@@ -974,22 +737,22 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     let fold () =
       let () = if debug_RAKAM () then
           let open Pp in Feedback.msg_debug (str "<><><><><>") in
-      ((EConstr.of_kind c0, stack),cst_l)
+      ((EConstr.of_kind c0, stack))
     in
     match c0 with
     | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
+      | LocalDef (_,body,_) -> whrec (lift n body, stack)
       | _ -> fold ())
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) ->
-        whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
+        whrec (body, stack)
       | _ -> fold ())
     | Evar ev -> fold ()
     | Meta ev ->
       (match safe_meta_value sigma ev with
-      | Some body -> whrec cst_l (body, stack)
+      | Some body -> whrec (body, stack)
       | None -> fold ())
     | Const (c,u as const) ->
       reduction_effect_hook env sigma c
@@ -1000,175 +763,70 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
        | body ->
          begin
           let body = EConstr.of_constr body in
-          if not tactic_mode
-          then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
-              (body, stack)
-          else (* Looks for ReductionBehaviour *)
-            match ReductionBehaviour.get (GlobRef.ConstRef c) with
-            | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
-            | Some behavior ->
-              begin match behavior with
-              | NeverUnfold -> fold ()
-              | (UnfoldWhen { nargs = Some n } |
-                 UnfoldWhenNoMatch { nargs = Some n } )
-                when Stack.args_size stack < n ->
-                fold ()
-              | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *)
-                  let app_sk,sk = Stack.strip_app stack in
-                  let (tm',sk'),cst_l' =
-                    whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
-                  in
-                  let rec is_case x = match EConstr.kind sigma x with
-                    | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
-                    | App (hd, _) -> is_case hd
-                    | Case _ -> true
-                    | _ -> false in
-                  if equal_stacks sigma (x, app_sk) (tm', sk')
-                  || Stack.will_expose_iota sk'
-                  || is_case tm'
-                  then fold ()
-                  else whrec cst_l' (tm', sk' @ sk)
-              | UnfoldWhen { recargs } -> (* maybe unfolds *)
-                begin match recargs with
-                  |[] -> (* if nargs has been specified *)
-                    (* CAUTION : the constant is NEVER refold
-                                            (even when it hides a (co)fix) *)
-                    whrec cst_l (body, stack)
-                  |curr::remains -> match Stack.strip_n_app curr stack with
-                    | None -> fold ()
-                    | Some (bef,arg,s') ->
-                      whrec Cst_stack.empty
-                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
-                end
-              end
-        end
+          whrec (body, stack)
+          end
        | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
           let kargs = CPrimitives.kind p in
           let (kargs,o) = Stack.get_next_primitive_args kargs stack in
           (* Should not fail thanks to [check_native_args] *)
           let (before,a,after) = Option.get o in
-          whrec Cst_stack.empty (a,Stack.Primitive(p,const,before,kargs,cst_l)::after)
+          whrec (a,Stack.Primitive(p,const,before,kargs)::after)
        | exception NotEvaluableConst _ -> fold ()
       else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
-      (let npars = Projection.npars p in
-       if not tactic_mode then
-         let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
-         whrec Cst_stack.empty stack'
-       else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
-         | None ->
-           let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
-           let stack'', csts = whrec Cst_stack.empty stack' in
-           if equal_stacks sigma stack' stack'' then fold ()
-           else stack'', csts
-         | Some behavior ->
-           begin match behavior with
-             | NeverUnfold -> fold ()
-             | (UnfoldWhen { nargs = Some n }
-               | UnfoldWhenNoMatch { nargs = Some n })
-               when Stack.args_size stack < n - (npars + 1) -> fold ()
-             | UnfoldWhen { recargs }
-             | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *)
-               let recargs = List.map_filter (fun x ->
-                   let idx = x - npars in
-                   if idx < 0 then None else Some idx) recargs
-               in
-               match recargs with
-               |[] -> (* if nargs has been specified *)
-                 (* CAUTION : the constant is NEVER refold
-                                  (even when it hides a (co)fix) *)
-                 let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
-                 whrec Cst_stack.empty(* cst_l *) stack'
-               | curr::remains ->
-                 if curr == 0 then (* Try to reduce the record argument *)
-                   whrec Cst_stack.empty
-                     (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack)
-                 else
-                   match Stack.strip_n_app curr stack with
-                   | None -> fold ()
-                   | Some (bef,arg,s') ->
-                     whrec Cst_stack.empty
-                       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
-                                      Stack.append_app [|c|] bef,cst_l)::s')
-           end)
+      let stack' = (c, Stack.Proj (p) :: stack) in
+      whrec stack'
 
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
-      apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
-    | Cast (c,_,_) -> whrec cst_l (c, stack)
+      apply_subst (fun _ -> whrec) [b] sigma c stack
+    | Cast (c,_,_) -> whrec (c, stack)
     | App (f,cl)  ->
       whrec
-        (if refold then Cst_stack.add_args cl cst_l else cst_l)
         (f, Stack.append_app cl stack)
     | Lambda (na,t,c) ->
       (match Stack.decomp stack with
       | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
-        apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
+        apply_subst (fun _ -> whrec) [] sigma x stack
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
         let env' = push_rel (LocalAssum (na, t)) env in
-        let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
-        (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
+        let whrec' = whd_state_gen flags env' sigma in
+        (match EConstr.kind sigma (Stack.zip sigma (whrec' (c, Stack.empty))) with
         | App (f,cl) ->
           let napp = Array.length cl in
           if napp > 0 then
-            let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
+            let (x', l') = whrec' (Array.last cl, Stack.empty) in
             match EConstr.kind sigma x', l' with
             | Rel 1, [] ->
               let lc = Array.sub cl 0 (napp-1) in
               let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-              if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold ()
+              if noccurn sigma 1 u then (pop u,Stack.empty) else fold ()
             | _ -> fold ()
           else fold ()
         | _ -> fold ())
       | _ -> fold ())
 
     | Case (ci,p,d,lf) ->
-      whrec Cst_stack.empty (d, Stack.Case (ci,p,lf,cst_l) :: stack)
+      whrec (d, Stack.Case (ci,p,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
       |None -> fold ()
       |Some (bef,arg,s') ->
-        whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
+        whrec (arg, Stack.Fix(f,bef)::s'))
 
     | Construct ((ind,c),u) ->
       let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
-          whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-        |args, (Stack.Proj (p,_)::s') when use_match ->
-          whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
-        |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
+        |args, (Stack.Case(ci, _, lf)::s') when use_match ->
+          whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Proj (p)::s') when use_match ->
+          whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
+        |args, (Stack.Fix (f,s')::s'') when use_fix ->
           let x' = Stack.zip sigma (x, args) in
           let out_sk = s' @ (Stack.append_app [|x'|] s'') in
-          reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
-        |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
-          let x' = Stack.zip sigma (x, args) in
-          begin match remains with
-          | [] ->
-            (match const with
-            | Stack.Cst_const const ->
-              (match constant_opt_value_in env const with
-              | None -> fold ()
-              | Some body ->
-                let const = (fst const, EInstance.make (snd const)) in
-                let body = EConstr.of_constr body in
-                whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
-                  (body, s' @ (Stack.append_app [|x'|] s'')))
-            | Stack.Cst_proj p ->
-              let stack = s' @ (Stack.append_app [|x'|] s'') in
-                match Stack.strip_n_app 0 stack with
-                | None -> assert false
-                | Some (_,arg,s'') ->
-                  whrec Cst_stack.empty (arg, Stack.Proj (p,cst_l) :: s''))
-          | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
-            | None -> fold ()
-            | Some (bef,arg,s''') ->
-              whrec Cst_stack.empty
-                (arg,
-                 Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''')
-          end
+          reduce_and_refold_fix whrec env sigma f out_sk
         |_, (Stack.App _)::_ -> assert false
         |_, _ -> fold ()
       else fold ()
@@ -1177,19 +835,19 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
         match Stack.strip_app stack with
         |args, ((Stack.Case _ |Stack.Proj _)::s') ->
-          reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack
+          reduce_and_refold_cofix whrec env sigma cofix stack
         |_ -> fold ()
       else fold ()
 
     | Int _ | Float _ ->
       begin match Stack.strip_app stack with
-       | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) ->
+       | (_, Stack.Primitive(p,kn,rargs,kargs)::s) ->
          let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
          if more_to_reduce then
            let (kargs,o) = Stack.get_next_primitive_args kargs s in
            (* Should not fail because Primitive is put on the stack only if fully applied *)
            let (before,a,after) = Option.get o in
-           whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after)
+           whrec (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs)::after)
          else
            let n = List.length kargs in
            let (args,s) = Stack.strip_app s in
@@ -1199,8 +857,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
            in
            let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in
              begin match CredNative.red_prim env sigma p args with
-               | Some t -> whrec cst_l' (t,s)
-               | None -> ((mkApp (mkConstU kn, args), s), cst_l)
+               | Some t -> whrec (t,s)
+               | None -> ((mkApp (mkConstU kn, args), s))
              end
        | _ -> fold ()
       end
@@ -1208,9 +866,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     | Rel _ | Var _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
-  fun xs ->
-  let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
-  if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
+  whrec
 
 (** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags _env sigma =
@@ -1243,15 +899,15 @@ let local_whd_state_gen flags _env sigma =
       | _ -> s)
 
     | Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
-      (whrec (c, Stack.Proj (p, Cst_stack.empty) :: stack))
+      (whrec (c, Stack.Proj (p) :: stack))
 
     | Case (ci,p,d,lf) ->
-      whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: stack)
+      whrec (d, Stack.Case (ci,p,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
       |None -> s
-      |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,Cst_stack.empty)::s'))
+      |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef)::s'))
 
     | Evar ev -> s
     | Meta ev ->
@@ -1264,14 +920,14 @@ let local_whd_state_gen flags _env sigma =
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
+        |args, (Stack.Case(ci, _, lf)::s') when use_match ->
           whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-        |args, (Stack.Proj (p,_) :: s') when use_match ->
+        |args, (Stack.Proj (p) :: s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
-        |args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
+        |args, (Stack.Fix (f,s')::s'') when use_fix ->
           let x' = Stack.zip sigma (x,args) in
           whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s''))
-        |_, (Stack.App _|Stack.Cst _)::_ -> assert false
+        |_, (Stack.App _)::_ -> assert false
         |_, _ -> s
       else s
 
@@ -1290,9 +946,7 @@ let local_whd_state_gen flags _env sigma =
   whrec
 
 let raw_whd_state_gen flags env =
-  let f sigma s = fst (whd_state_gen ~refold:false
-                         ~tactic_mode:false
-                         flags env sigma s) in
+  let f sigma s = whd_state_gen flags env sigma s in
   f
 
 let stack_red_of_state_red f =
@@ -1300,11 +954,11 @@ let stack_red_of_state_red f =
   f
 
 (* Drops the Cst_stack *)
-let iterate_whd_gen refold flags env sigma s =
+let iterate_whd_gen flags env sigma s =
   let rec aux t =
-  let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in
+  let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in
   let whd_sk = Stack.map aux sk in
-  Stack.zip sigma ~refold (hd,whd_sk)
+  Stack.zip sigma (hd,whd_sk)
   in aux s
 
 let red_of_state_red f env sigma x =
@@ -1717,8 +1371,6 @@ let is_sort env sigma t =
    of case/fix (heuristic used by evar_conv) *)
 
 let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
-  let refold = false in
-  let tactic_mode = false in
   let all' = CClosure.RedFlags.red_add_transparent CClosure.all ts in
   (* Unset the sharing flag to get a call-by-name reduction. This matters for
      the shape of the generated term. *)
@@ -1738,7 +1390,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
     | _ -> None
   in
   let rec whrec s =
-    let (t, stack as s), _ = whd_state_gen ~refold ~tactic_mode CClosure.betaiota env sigma s in
+    let (t, stack as s) = whd_state_gen CClosure.betaiota env sigma s in
     match Stack.strip_app stack with
       |args, (Stack.Case _ :: _ as stack') ->
         begin match whd_opt (t, args) with
@@ -1750,13 +1402,13 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
         | Some (t_o, args) when isConstruct sigma t_o -> whrec (t_o, Stack.append_app args stack')
         | (Some _ | None) -> s
         end
-      |args, (Stack.Proj (p,_) :: stack'') ->
+      |args, (Stack.Proj p :: stack'') ->
         begin match whd_opt (t, args) with
         | Some (t_o, args) when isConstruct sigma t_o ->
           whrec (args.(Projection.npars p + Projection.arg p), stack'')
         | (Some _ | None) -> s
         end
-      |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s
+      |_, ((Stack.App _|Stack.Primitive _) :: _|[]) -> s
   in
   whrec s
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index be91f688e7..a0cbd8ccf7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -19,6 +19,11 @@ open Environ
 
 exception Elimconst
 
+val debug_RAKAM : unit -> bool
+
+module CredNative : Primred.RedNative with
+  type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map
+
 (** Machinery to customize the behavior of the reduction *)
 module ReductionBehaviour : sig
 
@@ -46,41 +51,17 @@ val set_reduction_effect : Constant.t -> effect_name -> unit
 val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t ->
   Constr.constr Lazy.t -> unit
 
-(** {6 Machinery about a stack of unfolded constant }
-
-    cst applied to params must convertible to term of the state applied to args
-*)
-module Cst_stack : sig
-  type t
-  val empty : t
-  val add_param : constr -> t -> t
-  val add_args : constr array -> t -> t
-  val add_cst : constr -> t -> t
-  val best_cst : t -> (constr * constr list) option
-  val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
-  val reference : Evd.evar_map -> t -> Constant.t option
-  val pr : env -> Evd.evar_map -> t -> Pp.t
-end
-
 module Stack : sig
   type 'a app_node
 
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
-  type cst_member =
-    | Cst_const of pconstant
-    | Cst_proj of Projection.t
-
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of Projection.t * Cst_stack.t
-  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
-  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
-  | Cst of cst_member
-           * int (* current foccussed arg *)
-           * int list (* remaining args *)
-    * 'a t * Cst_stack.t
+  | Case of case_info * 'a * 'a array
+  | Proj of Projection.t
+  | Fix of ('a, 'a) pfixpoint * 'a t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
   and 'a t = 'a member list
 
   val pr : ('a -> Pp.t) -> 'a t -> Pp.t
@@ -119,8 +100,7 @@ module Stack : sig
   val tail : int -> 'a t -> 'a t
   val nth : 'a t -> int -> 'a
 
-  val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
-  val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
+  val zip : evar_map -> constr * constr t -> constr
 end
 
 (************************************************************************)
@@ -155,10 +135,10 @@ val stack_reduction_of_reduction :
 i*)
 val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a
 
-val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool ->
-  CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
+val whd_state_gen :
+  CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state
 
-val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
+val iterate_whd_gen : CClosure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> constr -> constr
 
 (** {6 Generic Optimized Reduction Function using Closures } *)
@@ -260,7 +240,7 @@ val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EI
 val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
-val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixpoint -> constr
+val contract_fix : evar_map -> fixpoint -> constr
 val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 88eec5ea01..95b07e227e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -487,7 +487,7 @@ let expand_table_key env = function
   | RelKey _ -> None
 
 let unfold_projection env p stk =
-  let s = Stack.Proj (p, Cst_stack.empty) in
+  let s = Stack.Proj p in
   s :: stk
 
 let expand_key ts env sigma = function
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
new file mode 100644
index 0000000000..21e38df6db
--- /dev/null
+++ b/tactics/cbn.ml
@@ -0,0 +1,797 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+open Constr
+open Context
+open Termops
+open Univ
+open Evd
+open Environ
+open EConstr
+open Vars
+open Context.Rel.Declaration
+
+(** This module implements a call by name reduction used by the cbn tactic.
+
+    It has an ability to "refold" constants by storing constants and
+    their parameters in its stack.
+*)
+
+(** Machinery to custom the behavior of the reduction *)
+module ReductionBehaviour = Reductionops.ReductionBehaviour
+
+(** Machinery about stack of unfolded constants *)
+module Cst_stack = struct
+  open EConstr
+
+(** constant * params * args
+
+- constant applied to params = term in head applied to args
+- there is at most one arguments with an empty list of args, it must be the first.
+- in args, the int represents the indice of the first arg to consider *)
+  type t = (constr * constr list * (int * constr array) list)  list
+
+  let empty = []
+  let is_empty = CList.is_empty
+
+  let drop_useless = function
+    | _ :: ((_,_,[])::_ as q) -> q
+    | l -> l
+
+  let add_param h cst_l =
+    let append2cst = function
+      | (c,params,[]) -> (c, h::params, [])
+      | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
+        (c, params, q)
+      | (c,params,(i,t)::q) ->
+        (c, params, (succ i,t)::q)
+    in
+      drop_useless (List.map append2cst cst_l)
+
+  let add_args cl =
+    List.map (fun (a,b,args) -> (a,b,(0,cl)::args))
+
+  let add_cst cst = function
+    | (_,_,[]) :: q as l -> l
+    | l -> (cst,[],[])::l
+
+  let best_cst = function
+    | (cst,params,[])::_ -> Some(cst,params)
+    | _ -> None
+
+  let reference sigma t = match best_cst t with
+    | Some (c, _) when isConst sigma c -> Some (fst (destConst sigma c))
+    | _ -> None
+
+  (** [best_replace d cst_l c] makes the best replacement for [d]
+      by [cst_l] in [c] *)
+  let best_replace sigma d cst_l c =
+    let reconstruct_head = List.fold_left
+      (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
+    List.fold_right
+      (fun (cst,params,args) t -> Termops.replace_term sigma
+        (reconstruct_head d args)
+        (applist (cst, List.rev params))
+        t) cst_l c
+
+  let pr env sigma l =
+    let open Pp in
+    let p_c c = Termops.Internal.print_constr_env env sigma c in
+    prlist_with_sep pr_semicolon
+      (fun (c,params,args) ->
+        hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
+                 pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++
+                 str ")")) l
+end
+
+
+(** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
+module Stack :
+sig
+  open EConstr
+  type 'a app_node
+
+  type cst_member =
+    | Cst_const of pconstant
+    | Cst_proj of Projection.t
+
+  type 'a member =
+  | App of 'a app_node
+  | Case of case_info * 'a * 'a array * Cst_stack.t
+  | Proj of Projection.t * Cst_stack.t
+  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
+  | Cst of cst_member * int * int list * 'a t * Cst_stack.t
+
+  and 'a t = 'a member list
+
+  exception IncompatibleFold2
+
+  val pr : ('a -> Pp.t) -> 'a t -> Pp.t
+  val empty : 'a t
+  val append_app : 'a array -> 'a t -> 'a t
+  val decomp : 'a t -> ('a * 'a t) option
+  val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
+    -> 'a t -> 'a t -> bool
+  val strip_app : 'a t -> 'a t * 'a t
+  val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
+  val will_expose_iota : 'a t -> bool
+  val list_of_app_stack : constr t -> constr list option
+  val args_size : 'a t -> int
+  val tail : int -> 'a t -> 'a t
+  val nth : 'a t -> int -> 'a
+  val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
+  val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
+  val check_native_args : CPrimitives.t -> 'a t -> bool
+  val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option
+end =
+struct
+  open EConstr
+  type 'a app_node = int * 'a array * int
+  (* first releavnt position, arguments, last relevant position *)
+
+  (*
+     Invariant that this module must ensure :
+     (behare of direct access to app_node by the rest of Reductionops)
+     - in app_node (i,_,j) i <= j
+     - There is no array realocation (outside of debug printing)
+   *)
+
+  let pr_app_node pr (i,a,j) =
+    let open Pp in surround (
+                     prvect_with_sep pr_comma pr (Array.sub a i (j - i + 1))
+                     )
+
+
+  type cst_member =
+    | Cst_const of pconstant
+    | Cst_proj of Projection.t
+
+  type 'a member =
+  | App of 'a app_node
+  | Case of case_info * 'a * 'a array * Cst_stack.t
+  | Proj of Projection.t * Cst_stack.t
+  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
+  | Cst of cst_member * int * int list * 'a t * Cst_stack.t
+
+  and 'a t = 'a member list
+
+  (* Debugging printer *)
+  let rec pr_member pr_c member =
+    let open Pp in
+    let pr_c x = hov 1 (pr_c x) in
+    match member with
+    | App app -> str "ZApp" ++ pr_app_node pr_c app
+    | Case (_,_,br,cst) ->
+       str "ZCase(" ++
+         prvect_with_sep (pr_bar) pr_c br
+       ++ str ")"
+    | Proj (p,cst) ->
+      str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
+    | Fix (f,args,cst) ->
+       str "ZFix(" ++ Constr.debug_print_fix pr_c f
+       ++ pr_comma () ++ pr pr_c args ++ str ")"
+    | Primitive (p,c,args,kargs,cst_l) ->
+      str "ZPrimitive(" ++ str (CPrimitives.to_string p)
+      ++ pr_comma () ++ pr pr_c args ++ str ")"
+    | Cst (mem,curr,remains,params,cst_l) ->
+      str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
+      ++ pr_comma () ++
+        prlist_with_sep pr_semicolon int remains ++
+        pr_comma () ++ pr pr_c params ++ str ")"
+  and pr pr_c l =
+    let open Pp in
+    prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
+
+  and pr_cst_member pr_c c =
+    let open Pp in
+      match c with
+      | Cst_const (c, u) ->
+        if Univ.Instance.is_empty u then Constant.debug_print c
+        else str"(" ++ Constant.debug_print c ++ str ", " ++
+          Univ.Instance.pr Univ.Level.pr u ++ str")"
+      | Cst_proj p ->
+        str".(" ++ Constant.debug_print (Projection.constant p) ++ str")"
+
+  let empty = []
+
+  let append_app v s =
+    let le = Array.length v in
+    if Int.equal le 0 then s else App (0,v,pred le) :: s
+
+  let decomp_node (i,l,j) sk =
+    if i < j then (l.(i), App (succ i,l,j) :: sk)
+    else (l.(i), sk)
+
+  let decomp = function
+    | App node::s -> Some (decomp_node node s)
+    | _ -> None
+
+  let decomp_node_last (i,l,j) sk =
+    if i < j then (l.(j), App (i,l,pred j) :: sk)
+    else (l.(j), sk)
+
+  let equal f f_fix sk1 sk2 =
+    let equal_cst_member x y =
+      match x, y with
+      | Cst_const (c1,u1), Cst_const (c2, u2) ->
+        Constant.equal c1 c2 && Univ.Instance.equal u1 u2
+      | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
+      | _, _ -> false
+    in
+    let rec equal_rec sk1 sk2 =
+      match sk1,sk2 with
+      | [],[] -> true
+      | App a1 :: s1, App a2 :: s2 ->
+        let t1,s1' = decomp_node_last a1 s1 in
+        let t2,s2' = decomp_node_last a2 s2 in
+        (f t1 t2) && (equal_rec s1' s2')
+      | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 ->
+        f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
+      | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
+        Projection.Repr.equal (Projection.repr p) (Projection.repr p2)
+        && equal_rec s1 s2
+      | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
+        f_fix f1 f2
+          && equal_rec (List.rev s1) (List.rev s2)
+          && equal_rec s1' s2'
+      | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' ->
+        equal_cst_member c1 c2
+          && equal_rec (List.rev params1) (List.rev params2)
+          && equal_rec s1' s2'
+      | ((App _|Case _|Proj _|Fix _|Cst _|Primitive _)::_|[]), _ -> false
+    in equal_rec (List.rev sk1) (List.rev sk2)
+
+  exception IncompatibleFold2
+
+  let append_app_list l s =
+    let a = Array.of_list l in
+    append_app a s
+
+  let rec args_size = function
+    | App (i,_,j)::s -> j + 1 - i + args_size s
+    | (Case _|Fix _|Proj _|Cst _|Primitive _)::_ | [] -> 0
+
+  let strip_app s =
+    let rec aux out = function
+      | ( App _ as e) :: s -> aux (e :: out) s
+      | s -> List.rev out,s
+    in aux [] s
+  let strip_n_app n s =
+    let rec aux n out = function
+      | App (i,a,j) as e :: s ->
+         let nb = j  - i + 1 in
+         if n >= nb then
+           aux (n - nb) (e::out) s
+         else
+           let p = i+n in
+           Some (CList.rev
+              (if Int.equal n 0 then out else App (i,a,p-1) :: out),
+            a.(p),
+            if j > p then App(succ p,a,j)::s else s)
+      | s -> None
+    in aux n [] s
+
+  let will_expose_iota args =
+    List.exists
+      (function (Fix (_,_,l) | Case (_,_,_,l) |
+                 Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
+      args
+
+  let list_of_app_stack s =
+    let rec aux = function
+      | App (i,a,j) :: s ->
+        let (args',s') = aux s in
+        let a' = Array.sub a i (j - i + 1) in
+        (Array.fold_right (fun x y -> x::y) a' args', s')
+      | s -> ([],s) in
+    let (out,s') = aux s in
+    let init = match s' with [] -> true | _ -> false in
+    Option.init init out
+
+  let tail n0 s0 =
+    let rec aux n s =
+      if Int.equal n 0 then s else
+        match s with
+      | App (i,a,j) :: s ->
+         let nb = j  - i + 1 in
+         if n >= nb then
+           aux (n - nb) s
+         else
+           let p = i+n in
+           if j >= p then App(p,a,j)::s else s
+        | _ -> raise (Invalid_argument "Reductionops.Stack.tail")
+    in aux n0 s0
+
+  let nth s p =
+    match strip_n_app p s with
+    | Some (_,el,_) -> el
+    | None -> raise Not_found
+
+  (** This function breaks the abstraction of Cst_stack ! *)
+  let best_state sigma (_,sk as s) l =
+    let rec aux sk def = function
+      |(cst, params, []) -> (cst, append_app_list (List.rev params) sk)
+      |(cst, params, (i,t)::q) -> match decomp sk with
+        | Some (el,sk') when EConstr.eq_constr sigma el t.(i) ->
+          if i = pred (Array.length t)
+          then aux sk' def (cst, params, q)
+          else aux sk' def (cst, params, (succ i,t)::q)
+        | _ -> def
+    in List.fold_left (aux sk) s l
+
+  let constr_of_cst_member f sk =
+    match f with
+    | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk
+    | Cst_proj p ->
+      match decomp sk with
+      | Some (hd, sk) -> mkProj (p, hd), sk
+      | None -> assert false
+
+  let zip ?(refold=false) sigma s =
+  let rec zip = function
+    | f, [] -> f
+    | f, (App (i,a,j) :: s) ->
+       let a' = if Int.equal i 0 && Int.equal j (Array.length a - 1)
+                then a
+                else Array.sub a i (j - i + 1) in
+       zip (mkApp (f, a'), s)
+    | f, (Case (ci,rt,br,cst_l)::s) when refold ->
+      zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l)
+    | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s)
+    | f, (Fix (fix,st,cst_l)::s) when refold ->
+      zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
+  | f, (Fix (fix,st,_)::s) -> zip
+    (mkFix fix, st @ (append_app [|f|] s))
+  | f, (Cst (cst,_,_,params,cst_l)::s) when refold ->
+    zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
+  | f, (Cst (cst,_,_,params,_)::s) ->
+    zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
+  | f, (Proj (p,cst_l)::s) when refold ->
+    zip (best_state sigma (mkProj (p,f),s) cst_l)
+  | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s)
+  | f, (Primitive (p,c,args,kargs,cst_l)::s) ->
+      zip (mkConstU c, args @ append_app [|f|] s)
+  in
+  zip s
+
+  (* Check if there is enough arguments on [stk] w.r.t. arity of [op] *)
+  let check_native_args op stk =
+    let nargs = CPrimitives.arity op in
+    let rargs = args_size stk in
+    nargs <= rargs
+
+  let get_next_primitive_args kargs stk =
+    let rec nargs = function
+      | [] -> 0
+      | CPrimitives.Kwhnf :: _ -> 0
+      | _ :: s -> 1 + nargs s
+    in
+    let n = nargs kargs in
+    (List.skipn (n+1) kargs, strip_n_app n stk)
+
+end
+
+(** The type of (machine) states (= lambda-bar-calculus' cuts) *)
+
+(*************************************)
+(*** Reduction Functions Operators ***)
+(*************************************)
+
+let safe_meta_value sigma ev =
+  try Some (Evd.meta_value sigma ev)
+  with Not_found -> None
+
+(*************************************)
+(*** Reduction using bindingss ***)
+(*************************************)
+
+(* Beta Reduction tools *)
+
+let apply_subst recfun env sigma refold cst_l t stack =
+  let rec aux env cst_l t stack =
+    match (Stack.decomp stack, EConstr.kind sigma t) with
+    | Some (h,stacktl), Lambda (_,_,c) ->
+       let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
+       aux (h::env) cst_l' c stacktl
+    | _ -> recfun sigma cst_l (substl env t, stack)
+  in aux env cst_l t stack
+
+(* Iota reduction tools *)
+
+(** @return c if there is a constant c whose body is bd
+    @return bd else.
+
+    It has only a meaning because internal representation of "Fixpoint f x
+    := t" is Definition f := fix f x => t
+
+    Even more fragile that we could hope because do Module M. Fixpoint
+    f x := t. End M. Definition f := u. and say goodbye to any hope
+    of refolding M.f this way ...
+*)
+let magically_constant_of_fixbody env sigma reference bd = function
+  | Name.Anonymous -> bd
+  | Name.Name id ->
+    let open UnivProblem in
+    let (cst_mod,_) = Constant.repr2 reference in
+    let cst = Constant.make2 cst_mod (Label.of_id id) in
+    if not (Environ.mem_constant cst env) then bd
+    else
+      let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
+      match constant_opt_value_in env (cst,u) with
+      | None -> bd
+      | Some t ->
+        let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
+        begin match csts with
+          | Some csts ->
+            let subst = Set.fold (fun cst acc ->
+                let l, r = match cst with
+                  | ULub (u, v) | UWeak (u, v) -> u, v
+                  | UEq (u, v) | ULe (u, v) ->
+                    let get u = Option.get (Universe.level u) in
+                    get u, get v
+                in
+                Univ.LMap.add l r acc)
+                csts Univ.LMap.empty
+            in
+            let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
+            mkConstU (cst, EInstance.make inst)
+          | None -> bd
+        end
+
+let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+  let nbodies = Array.length bodies in
+  let make_Fi j =
+    let ind = nbodies-j-1 in
+    if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
+    else
+      let bd = mkCoFix (ind,typedbodies) in
+      match env with
+      | None -> bd
+      | Some e ->
+        match reference with
+        | None -> bd
+        | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+  let closure = List.init nbodies make_Fi in
+  substl closure bodies.(bodynum)
+
+(** Similar to the "fix" case below *)
+let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
+  let raw_answer =
+    let env = if refold then Some env else None in
+    contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
+  apply_subst
+    (fun sigma x (t,sk') ->
+      let t' =
+        if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
+      recfun x (t',sk'))
+    [] sigma refold Cst_stack.empty raw_answer sk
+
+(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
+   Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
+
+let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+    let nbodies = Array.length recindices in
+    let make_Fi j =
+      let ind = nbodies-j-1 in
+      if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
+      else
+        let bd = mkFix ((recindices,ind),typedbodies) in
+        match env with
+        | None -> bd
+        | Some e ->
+          match reference with
+          | None -> bd
+          | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+    let closure = List.init nbodies make_Fi in
+    substl closure bodies.(bodynum)
+
+(** First we substitute the Rel bodynum by the fixpoint and then we try to
+    replace the fixpoint by the best constant from [cst_l]
+    Other rels are directly substituted by constants "magically found from the
+    context" in contract_fix *)
+let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
+  let raw_answer =
+    let env = if refold then Some env else None in
+    contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
+  apply_subst
+    (fun sigma x (t,sk') ->
+      let t' =
+        if refold then
+          Cst_stack.best_replace sigma (mkFix fix) cst_l t
+        else t
+      in recfun x (t',sk'))
+    [] sigma refold Cst_stack.empty raw_answer sk
+
+module CredNative = Reductionops.CredNative
+
+(** Generic reduction function with environment
+
+    Here is where unfolded constant are stored in order to be
+    eventually refolded.
+
+    If tactic_mode is true, it uses ReductionBehaviour, prefers
+    refold constant instead of value and tries to infer constants
+    fix and cofix came from.
+
+    It substitutes fix and cofix by the constant they come from in
+    contract_* in any case .
+*)
+
+let debug_RAKAM = Reductionops.debug_RAKAM
+
+let equal_stacks sigma (x, l) (y, l') =
+  let f_equal x y = eq_constr sigma x y in
+  let eq_fix a b = f_equal (mkFix a) (mkFix b) in
+  Stack.equal f_equal eq_fix l l' && f_equal x y
+
+let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
+  let open Context.Named.Declaration in
+  let open ReductionBehaviour in
+  let rec whrec cst_l (x, stack) =
+    let () = if debug_RAKAM () then
+        let open Pp in
+        let pr c = Termops.Internal.print_constr_env env sigma c in
+        Feedback.msg_debug
+             (h 0 (str "<<" ++ pr x ++
+                   str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
+                   str "|" ++ cut () ++ Stack.pr pr stack ++
+                   str ">>"))
+    in
+    let c0 = EConstr.kind sigma x in
+    let fold () =
+      let () = if debug_RAKAM () then
+          let open Pp in Feedback.msg_debug (str "<><><><><>") in
+      ((EConstr.of_kind c0, stack),cst_l)
+    in
+    match c0 with
+    | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
+      (match lookup_rel n env with
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
+      | _ -> fold ())
+    | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
+      (match lookup_named id env with
+      | LocalDef (_,body,_) ->
+        whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
+      | _ -> fold ())
+    | Evar ev -> fold ()
+    | Meta ev ->
+      (match safe_meta_value sigma ev with
+      | Some body -> whrec cst_l (body, stack)
+      | None -> fold ())
+    | Const (c,u as const) ->
+      Reductionops.reduction_effect_hook env sigma c
+         (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
+      if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
+       let u' = EInstance.kind sigma u in
+       match constant_value_in env (c, u') with
+       | body ->
+         begin
+          let body = EConstr.of_constr body in
+          if not tactic_mode
+          then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+              (body, stack)
+          else (* Looks for ReductionBehaviour *)
+            match ReductionBehaviour.get (GlobRef.ConstRef c) with
+            | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
+            | Some behavior ->
+              begin match behavior with
+              | NeverUnfold -> fold ()
+              | (UnfoldWhen { nargs = Some n } |
+                 UnfoldWhenNoMatch { nargs = Some n } )
+                when Stack.args_size stack < n ->
+                fold ()
+              | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *)
+                  let app_sk,sk = Stack.strip_app stack in
+                  let (tm',sk'),cst_l' =
+                    whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
+                  in
+                  let rec is_case x = match EConstr.kind sigma x with
+                    | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+                    | App (hd, _) -> is_case hd
+                    | Case _ -> true
+                    | _ -> false in
+                  if equal_stacks sigma (x, app_sk) (tm', sk')
+                  || Stack.will_expose_iota sk'
+                  || is_case tm'
+                  then fold ()
+                  else whrec cst_l' (tm', sk' @ sk)
+              | UnfoldWhen { recargs } -> (* maybe unfolds *)
+                begin match recargs with
+                  |[] -> (* if nargs has been specified *)
+                    (* CAUTION : the constant is NEVER refold
+                                            (even when it hides a (co)fix) *)
+                    whrec cst_l (body, stack)
+                  |curr::remains -> match Stack.strip_n_app curr stack with
+                    | None -> fold ()
+                    | Some (bef,arg,s') ->
+                      whrec Cst_stack.empty
+                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
+                end
+              end
+        end
+       | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
+          let kargs = CPrimitives.kind p in
+          let (kargs,o) = Stack.get_next_primitive_args kargs stack in
+          (* Should not fail thanks to [check_native_args] *)
+          let (before,a,after) = Option.get o in
+          whrec Cst_stack.empty (a,Stack.Primitive(p,const,before,kargs,cst_l)::after)
+       | exception NotEvaluableConst _ -> fold ()
+      else fold ()
+    | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
+      (let npars = Projection.npars p in
+       if not tactic_mode then
+         let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
+         whrec Cst_stack.empty stack'
+       else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
+         | None ->
+           let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
+           let stack'', csts = whrec Cst_stack.empty stack' in
+           if equal_stacks sigma stack' stack'' then fold ()
+           else stack'', csts
+         | Some behavior ->
+           begin match behavior with
+             | NeverUnfold -> fold ()
+             | (UnfoldWhen { nargs = Some n }
+               | UnfoldWhenNoMatch { nargs = Some n })
+               when Stack.args_size stack < n - (npars + 1) -> fold ()
+             | UnfoldWhen { recargs }
+             | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *)
+               let recargs = List.map_filter (fun x ->
+                   let idx = x - npars in
+                   if idx < 0 then None else Some idx) recargs
+               in
+               match recargs with
+               |[] -> (* if nargs has been specified *)
+                 (* CAUTION : the constant is NEVER refold
+                                  (even when it hides a (co)fix) *)
+                 let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
+                 whrec Cst_stack.empty(* cst_l *) stack'
+               | curr::remains ->
+                 if curr == 0 then (* Try to reduce the record argument *)
+                   whrec Cst_stack.empty
+                     (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack)
+                 else
+                   match Stack.strip_n_app curr stack with
+                   | None -> fold ()
+                   | Some (bef,arg,s') ->
+                     whrec Cst_stack.empty
+                       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
+                                      Stack.append_app [|c|] bef,cst_l)::s')
+           end)
+
+    | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
+      apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
+    | Cast (c,_,_) -> whrec cst_l (c, stack)
+    | App (f,cl)  ->
+      whrec
+        (if refold then Cst_stack.add_args cl cst_l else cst_l)
+        (f, Stack.append_app cl stack)
+    | Lambda (na,t,c) ->
+      (match Stack.decomp stack with
+      | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
+        apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
+      | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
+        let env' = push_rel (LocalAssum (na, t)) env in
+        let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
+        (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
+        | App (f,cl) ->
+          let napp = Array.length cl in
+          if napp > 0 then
+            let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
+            match EConstr.kind sigma x', l' with
+            | Rel 1, [] ->
+              let lc = Array.sub cl 0 (napp-1) in
+              let u = if Int.equal napp 1 then f else mkApp (f,lc) in
+              if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold ()
+            | _ -> fold ()
+          else fold ()
+        | _ -> fold ())
+      | _ -> fold ())
+
+    | Case (ci,p,d,lf) ->
+      whrec Cst_stack.empty (d, Stack.Case (ci,p,lf,cst_l) :: stack)
+
+    | Fix ((ri,n),_ as f) ->
+      (match Stack.strip_n_app ri.(n) stack with
+      |None -> fold ()
+      |Some (bef,arg,s') ->
+        whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
+
+    | Construct ((ind,c),u) ->
+      let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
+      let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
+      if use_match || use_fix then
+        match Stack.strip_app stack with
+        |args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
+          whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Proj (p,_)::s') when use_match ->
+          whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
+        |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
+          let x' = Stack.zip sigma (x, args) in
+          let out_sk = s' @ (Stack.append_app [|x'|] s'') in
+          reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
+        |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
+          let x' = Stack.zip sigma (x, args) in
+          begin match remains with
+          | [] ->
+            (match const with
+            | Stack.Cst_const const ->
+              (match constant_opt_value_in env const with
+              | None -> fold ()
+              | Some body ->
+                let const = (fst const, EInstance.make (snd const)) in
+                let body = EConstr.of_constr body in
+                whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+                  (body, s' @ (Stack.append_app [|x'|] s'')))
+            | Stack.Cst_proj p ->
+              let stack = s' @ (Stack.append_app [|x'|] s'') in
+                match Stack.strip_n_app 0 stack with
+                | None -> assert false
+                | Some (_,arg,s'') ->
+                  whrec Cst_stack.empty (arg, Stack.Proj (p,cst_l) :: s''))
+          | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
+            | None -> fold ()
+            | Some (bef,arg,s''') ->
+              whrec Cst_stack.empty
+                (arg,
+                 Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''')
+          end
+        |_, (Stack.App _)::_ -> assert false
+        |_, _ -> fold ()
+      else fold ()
+
+    | CoFix cofix ->
+      if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
+        match Stack.strip_app stack with
+        |args, ((Stack.Case _ |Stack.Proj _)::s') ->
+          reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack
+        |_ -> fold ()
+      else fold ()
+
+    | Int _ | Float _ ->
+      begin match Stack.strip_app stack with
+       | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) ->
+         let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
+         if more_to_reduce then
+           let (kargs,o) = Stack.get_next_primitive_args kargs s in
+           (* Should not fail because Primitive is put on the stack only if fully applied *)
+           let (before,a,after) = Option.get o in
+           whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after)
+         else
+           let n = List.length kargs in
+           let (args,s) = Stack.strip_app s in
+           let (args,extra_args) =
+             try List.chop n args
+             with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *)
+           in
+           let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in
+             begin match CredNative.red_prim env sigma p args with
+               | Some t -> whrec cst_l' (t,s)
+               | None -> ((mkApp (mkConstU kn, args), s), cst_l)
+             end
+       | _ -> fold ()
+      end
+
+    | Rel _ | Var _ | LetIn _ | Proj _ -> fold ()
+    | Sort _ | Ind _ | Prod _ -> fold ()
+  in
+  fun xs ->
+  let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
+  if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
+
+let whd_cbn flags env sigma t =
+  let (state,_) =
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty))
+  in
+  Stack.zip ~refold:true sigma state
diff --git a/tactics/cbn.mli b/tactics/cbn.mli
new file mode 100644
index 0000000000..af54771382
--- /dev/null
+++ b/tactics/cbn.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val whd_cbn :
+  CClosure.RedFlags.reds ->
+  Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7d8620468d..c2eabffd44 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -59,32 +59,12 @@ let registered_e_assumption =
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
 
-(*s Tactics handling a list of goals. *)
-
-(* first_goal : goal list sigma -> goal sigma *)
-
-let first_goal gls =
-  let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
-  if List.is_empty gl then user_err Pp.(str "first_goal");
-  { Evd.it = List.hd gl; Evd.sigma = sig_0; }
-
-(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
-
-let apply_tac_list tac glls =
-  match glls.it with
-  | (g1::rest) ->
-      let pack = tac (re_sig g1 glls.sigma) in
-      re_sig (pack.it @ rest) pack.sigma
-  | _ -> user_err Pp.(str "apply_tac_list")
-
 open Auto
 
 (***************************************************************************)
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
-
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
       let clenv', c = connect_hint_clenv ~poly c clenv gl in
@@ -94,7 +74,9 @@ let unify_e_resolve poly flags (c,clenv) =
         (Tactics.Simple.eapply c)
     end
 
-let hintmap_of sigma secvars hdc concl =
+let hintmap_of sigma secvars concl =
+  (* Warning: for computation sharing, we need to return a closure *)
+  let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in
   match hdc with
   | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
@@ -125,13 +107,13 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
+    (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))
   in
   Tacticals.New.tclSOLVE tacl
   end
 
-and e_my_find_search env sigma db_list local_db secvars hdc concl =
-  let hint_of_db = hintmap_of sigma secvars hdc concl in
+and e_my_find_search env sigma db_list local_db secvars concl =
+  let hint_of_db = hintmap_of sigma secvars concl in
   let hintl =
       List.map_append (fun db ->
         let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -143,35 +125,40 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl =
       | Unfold_nth _ -> 1
       | _ -> b
       in
-      (b,
-        let tac = function
-        | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
-        | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-        | Give_exact (c,cl) -> e_exact poly st (c,cl)
-        | Res_pf_THEN_trivial_fail (term,cl) ->
-          Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
-            (e_trivial_fail_db db_list local_db)
-        | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
-        | Extern tacast -> conclPattern concl p tacast
-       in
-       let tac = run_hint t tac in
-       (tac, lazy (pr_hint env sigma t)))
+      let tac = function
+      | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
+      | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
+      | Give_exact (c,cl) -> e_exact poly st (c,cl)
+      | Res_pf_THEN_trivial_fail (term,cl) ->
+        Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
+          (e_trivial_fail_db db_list local_db)
+      | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
+      | Extern tacast -> conclPattern concl p tacast
+      in
+      let tac = run_hint t tac in
+      (tac, b, lazy (pr_hint env sigma t))
   in
   List.map tac_of_hint hintl
 
 and e_trivial_resolve env sigma db_list local_db secvars gl =
-  let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
-  try priority (e_my_find_search env sigma db_list local_db secvars hd gl)
+  let filter (tac, pr, _) = if Int.equal pr 0 then Some tac else None in
+  try List.map_filter filter (e_my_find_search env sigma db_list local_db secvars gl)
   with Not_found -> []
 
 let e_possible_resolve env sigma db_list local_db secvars gl =
-  let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
-  try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
-               (e_my_find_search env sigma db_list local_db secvars hd gl)
+  try e_my_find_search env sigma db_list local_db secvars gl
   with Not_found -> []
 
+(*s Tactics handling a list of goals. *)
+
+(* first_goal : goal list sigma -> goal sigma *)
+
 let find_first_goal gls =
-  try first_goal gls with UserError _ -> assert false
+  let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
+  match gl with
+  | [] -> assert false
+  | (gl, db) :: _ ->
+    { Evd.it = gl; Evd.sigma = sig_0; }, db
 
 (*s The following module [SearchProblem] is used to instantiate the generic
     exploration functor [Explore.Make]. *)
@@ -179,10 +166,9 @@ let find_first_goal gls =
 type search_state = {
   priority : int;
   depth : int; (*r depth of search before failing *)
-  tacres : Goal.goal list sigma;
+  tacres : (Goal.goal * hint_db) list sigma;
   last_tactic : Pp.t Lazy.t;
   dblist : hint_db list;
-  localdb :  hint_db list;
   prev : prev_search_state;
   local_lemmas : delayed_open_constr list;
 }
@@ -200,7 +186,16 @@ module SearchProblem = struct
 
 (*   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *)
 
-  let filter_tactics glls l =
+(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
+
+  let apply_tac_list tac mkdb glls =
+    match glls.it with
+    | ((g1, db) :: rest) ->
+        let pack = tac (re_sig g1 glls.sigma) in
+        List.map (fun gl -> gl, mkdb db (re_sig gl pack.sigma)) pack.it, re_sig rest pack.sigma
+    | _ -> user_err Pp.(str "apply_tac_list")
+
+  let filter_tactics mkdb glls l =
 (*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (*     let evars = Evarutil.nf_evars (Refiner.project glls) in *)
 (*     msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
@@ -208,10 +203,10 @@ module SearchProblem = struct
       | [] -> []
       | (tac, cost, pptac) :: tacl ->
           try
-            let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in
+            let ngls, lgls = apply_tac_list (Proofview.V82.of_tactic tac) mkdb glls in
 (* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
-              (lgls, cost, pptac) :: aux tacl
+              (ngls, lgls, cost, pptac) :: aux tacl
           with e when CErrors.noncritical e ->
             let e = Exninfo.capture e in
             Refiner.catch_failerror e; aux tacl
@@ -233,63 +228,54 @@ module SearchProblem = struct
     else
       let ps = if s.prev == Unknown then Unknown else State s in
       let lg = s.tacres in
-      let nbgl = List.length (sig_it lg) in
-      assert (nbgl > 0);
-      let g = find_first_goal lg in
+      let g, db = find_first_goal lg in
       let hyps = pf_ids_of_hyps g in
       let secvars = secvars_of_hyps (pf_hyps g) in
       let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ Id.print id)) in
       let assumption_tacs =
         let tacs = List.map map_assum hyps in
-        let l = filter_tactics s.tacres tacs in
-        List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
+        let mkdb db gl = assert false in (* no goal can be generated *)
+        let l = filter_tactics mkdb s.tacres tacs in
+        List.map (fun (ngl, res, cost, pp) ->
+          let () = assert (List.is_empty ngl) in
+          { depth = s.depth; priority = cost; tacres = res;
                                     last_tactic = pp; dblist = s.dblist;
-                                    localdb = List.tl s.localdb;
                                     prev = ps; local_lemmas = s.local_lemmas}) l
       in
       let intro_tac =
-        let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
+        let mkdb db gl =
+          let hintl = make_resolve_hyp (pf_env gl) (project gl) (pf_last_hyp gl) in
+          Hint_db.add_list (pf_env gl) (project gl) hintl db
+        in
+        let l = filter_tactics mkdb s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
         List.map
-          (fun (lgls, cost, pp) ->
-             let g' = first_goal lgls in
-             let hintl =
-               make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-             in
-             let ldb = Hint_db.add_list (pf_env g') (project g')
-                  hintl (List.hd s.localdb) in
+          (fun (ngls, lgls, cost, pp) ->
+             let lgls = re_sig (ngls @ lgls.it) lgls.sigma in
              { depth = s.depth; priority = cost; tacres = lgls;
                last_tactic = pp; dblist = s.dblist;
-               localdb = ldb :: List.tl s.localdb; prev = ps;
+               prev = ps;
                local_lemmas = s.local_lemmas})
           l
       in
       let rec_tacs =
+        let hyps = pf_hyps g in
+        let mkdb db gls =
+          let hyps' = pf_hyps gls in
+            if hyps' == hyps then db
+            else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas
+        in
         let l =
           let concl = Reductionops.nf_evar (project g) (pf_concl g) in
-          filter_tactics s.tacres
-                         (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl)
+          filter_tactics mkdb s.tacres
+                         (e_possible_resolve (pf_env g) (project g) s.dblist db secvars concl)
         in
         List.map
-          (fun (lgls, cost, pp) ->
-             let nbgl' = List.length (sig_it lgls) in
-             if nbgl' < nbgl then
-               { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
-                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb;
-                  local_lemmas = s.local_lemmas }
-             else
-               let newlocal =
-                 let hyps = pf_hyps g in
-                   List.map (fun gl ->
-                     let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
-                     let hyps' = pf_hyps gls in
-                       if hyps' == hyps then List.hd s.localdb
-                       else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas)
-                     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
-               in
-                 { depth = pred s.depth; priority = cost; tacres = lgls;
-                   dblist = s.dblist; last_tactic = pp; prev = ps;
-                   localdb = newlocal @ List.tl s.localdb;
-                   local_lemmas = s.local_lemmas })
+          (fun (ngls, lgls, cost, pp) ->
+            let lgls = re_sig (ngls @ lgls.it) lgls.sigma in
+            let depth = if List.is_empty ngls then s.depth else pred s.depth in
+            { depth; priority = cost; tacres = lgls; last_tactic = pp;
+              prev = ps; dblist = s.dblist;
+              local_lemmas = s.local_lemmas })
           l
       in
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
@@ -353,15 +339,15 @@ let pr_info dbg s =
 let make_initial_state dbg n gl dblist localdb lems =
   { depth = n;
     priority = 0;
-    tacres = tclIDTAC gl;
+    tacres = re_sig [gl.it, localdb] gl.sigma;
     last_tactic = lazy (mt());
     dblist = dblist;
-    localdb = [localdb];
     prev = if dbg == Info then Init else Unknown;
     local_lemmas = lems;
   }
 
-let e_search_auto debug (in_depth,p) lems db_list gl =
+let e_search_auto debug (in_depth,p) lems db_list =
+  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
   let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TransparentState.full true lems in
   let d = mk_eauto_dbg debug in
   let tac = match in_depth,d with
@@ -374,28 +360,29 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
     pr_dbg_header d;
     let s = tac (make_initial_state d p gl db_list local_db lems) in
     pr_info d s;
-    s.tacres
+    re_sig (List.map fst s.tacres.it) s.tacres.sigma
   with Not_found ->
     pr_info_nop d;
-    user_err Pp.(str "eauto: search failed")
+    tclIDTAC gl
+  end
 
 (* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *)
 (* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
 
 let eauto_with_bases ?(debug=Off) np lems db_list =
-  Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list)))
+  Hints.wrap_hint_warning (e_search_auto debug np lems db_list)
 
 let eauto ?(debug=Off) np lems dbnames =
   let db_list = make_db_list dbnames in
-  tclTRY (e_search_auto debug np lems db_list)
+  e_search_auto debug np lems db_list
 
-let full_eauto ?(debug=Off) n lems gl =
+let full_eauto ?(debug=Off) n lems =
   let db_list = current_pure_db () in
-  tclTRY (e_search_auto debug n lems db_list) gl
+  e_search_auto debug n lems db_list
 
 let gen_eauto ?(debug=Off) np lems = function
-  | None -> Hints.wrap_hint_warning (Proofview.V82.tactic (full_eauto ~debug np lems))
-  | Some l -> Hints.wrap_hint_warning (Proofview.V82.tactic (eauto ~debug np lems l))
+  | None -> Hints.wrap_hint_warning (full_eauto ~debug np lems)
+  | Some l -> Hints.wrap_hint_warning (eauto ~debug np lems l)
 
 let make_depth = function
   | None -> !default_search_depth
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index f681e4e99e..e000ddce74 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -44,11 +44,7 @@ let cbv_native env sigma c =
     (warn_native_compute_disabled ();
      cbv_vm env sigma c)
 
-let whd_cbn flags env sigma t =
-  let (state,_) =
-    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
-  in
-  Reductionops.Stack.zip ~refold:true sigma state
+let whd_cbn = Cbn.whd_cbn
 
 let strong_cbn flags =
   strong_with_flags whd_cbn flags
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 36d61feed1..88025e3fb4 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -9,6 +9,7 @@ Eqschemes
 Elimschemes
 Genredexpr
 Redops
+Cbn
 Redexpr
 Ppred
 Tactics
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index e2ed2db728..1436da30fa 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -801,7 +801,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
 # projects. Note that extra options might be on the command line.
 VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
 
-$(VDFILE): $(VFILES)
+$(VDFILE): @PROJECT_FILE@ $(VFILES)
 	$(SHOW)'COQDEP VFILES'
 	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 023d76ce3b..44c30598aa 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -24,8 +24,7 @@ module RelDecl = Context.Rel.Declaration
 
 let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
   let kind = Decls.IsAssumption kind in
-  let decl = Declare.SectionLocalAssum {typ; impl} in
-  let () = Declare.declare_variable ~name ~kind decl in
+  let () = Declare.declare_variable ~name ~kind ~typ ~impl in
   let () = Declare.assumption_message name in
   let r = GlobRef.VarRef name in
   let () = maybe_declare_manual_implicits true r imps in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 6ed7a9e39d..7de1ff4083 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -554,7 +554,7 @@ let objVariable : unit Libobject.Dyn.tag =
 
 let inVariable v = Libobject.Dyn.Easy.inj v objVariable
 
-let declare_variable ~name ~kind d =
+let declare_variable_core ~name ~kind d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (DeclareUniv.AlreadyDeclared (None, name));
@@ -591,6 +591,9 @@ let declare_variable ~name ~kind d =
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
+let declare_variable ~name ~kind ~typ ~impl =
+  declare_variable_core ~name ~kind (SectionLocalAssum { typ; impl })
+
 (* Declaration messages *)
 
 let pr_rank i = pr_nth (i+1)
@@ -913,7 +916,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   let ubind = UState.universe_binders uctx in
   let dref = match scope with
   | Discharge ->
-    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
+    let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Global local ->
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 5339f4702b..ef4f8c4825 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -119,13 +119,6 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t
 (** XXX: This is an internal, low-level API and could become scheduled
    for removal from the public API, use higher-level declare APIs
    instead *)
-type variable_declaration =
-  | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
-
-(** XXX: This is an internal, low-level API and could become scheduled
-   for removal from the public API, use higher-level declare APIs
-   instead *)
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
@@ -134,7 +127,8 @@ type 'a constant_entry =
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
-  -> variable_declaration
+  -> typ:types
+  -> impl:Glob_term.binding_kind
   -> unit
 
 (** Declaration of global constructions