Port the Coq part

4 files changed, 26 insertions, 20 deletions

diff --git a/src/Makefile b/src/Makefile
index dfcbd38..95955bb 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.12.1
+## GNUMakefile for Coq 8.13.1
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -104,7 +104,7 @@ BEFORE ?=
 AFTER ?=
 
 # FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=num,str,unix,dynlink,threads
+CAMLDONTLINK=str,unix,dynlink,threads,zarith
 
 # OCaml binaries
 CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
@@ -146,6 +146,21 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
 
 TGTS ?=
 
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+# Substitution of the path by appending $(DESTDIR) if needed.
+# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
+windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1))
+destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
+
+# Installation paths of libraries and documentation.
+COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
+COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
+COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
+
 ########## End of parameters ##################################################
 # What follows may be relevant to you only if you need to
 # extend this Makefile.  If so, look for 'Extension point' here and
@@ -203,7 +218,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.12.1
+COQMAKEFILE_VERSION:=8.13.1
 
 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
@@ -227,17 +242,6 @@ else
 TIMING_ARG=
 endif
 
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
-
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -463,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok)
 .PHONY: vok
 
 validate: $(VOFILES)
-	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
 .PHONY: validate
 
 only: $(TGTS)
@@ -577,7 +581,7 @@ uninstall::
 	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf" &&\
-	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+	 (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
 	done
 .PHONY: uninstall
 
@@ -797,7 +801,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
 # projects. Note that extra options might be on the command line.
 VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
 
-$(VDFILE): $(VFILES)
+$(VDFILE): _CoqProject $(VFILES)
 	$(SHOW)'COQDEP VFILES'
 	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
diff --git a/src/QInst.v b/src/QInst.v
index b2dd836..e78a2fe 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -27,7 +27,7 @@ Proof.
    installed when we compile SMTCoq. *)
 Qed.
 
-Hint Resolve impl_split : smtcoq_core.
+#[export] Hint Resolve impl_split : smtcoq_core.
 
 (** verit silently transforms an <implb (a || b) c> into a <or (not a) c>
    or into a <or (not b) c> when instantiating such a quantified theorem *)
diff --git a/src/array/FArray.v b/src/array/FArray.v
index 69e56f9..e45abb4 100644
--- a/src/array/FArray.v
+++ b/src/array/FArray.v
@@ -130,7 +130,7 @@ Module Raw.
   Qed.
 
   Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''.
-  Proof. unfold ltk; eauto. Qed.
+  Proof. unfold ltk; eauto with typeclass_ordtype. Qed.
 
   Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
   Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed.
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 49729db..be16138 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -98,6 +98,8 @@ Class OrdType T := {
   lt_not_eq : forall x y : T, lt x y -> x <> y
 }.
 
+#[export] Hint Resolve lt_not_eq lt_trans : typeclass_ordtype.
+
 
 Global Instance StrictOrder_OrdType T `(OrdType T) :
   StrictOrder (lt : T -> T -> Prop).
@@ -182,7 +184,7 @@ Proof.
   intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
-Hint Resolve
+#[export] Hint Resolve
      ord_of_compdec
      inh_of_compdec
      comp_of_compdec