update to preserve backward compatibility with v8.4

15 files changed, 222 insertions, 37 deletions

diff --git a/mathcomp/Makefile b/mathcomp/Makefile
index 11419d3..c5a0a3b 100644
--- a/mathcomp/Makefile
+++ b/mathcomp/Makefile
@@ -17,6 +17,12 @@ else
 V=$(BRANCH_coq)
 endif
 
+ifeq "$V" "v8.4"
+COQDEP=../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -24,10 +30,10 @@ MAKEFLAGS+=-B
 
 %:
 	$(H)[ -e Makefile.coq ] || $(call coqmakefile)
-	# Override COQDEP to find only the "right" copy of .ml files
+	# Override COQDEP to find only the "right" copy .ml files
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
 		-f Makefile.coq $* \
-		COQDEP='$(COQBIN)/coqdep -exclude-dir "plugin" -c'
+		COQDEP='$(COQDEP) -exclude-dir plugin -c'
 
 define coqmakefile
 	(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
index e872352..8f03823 100644
--- a/mathcomp/algebra/Makefile
+++ b/mathcomp/algebra/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/basic/Make b/mathcomp/basic/Make
index cd88088..8acef84 100644
--- a/mathcomp/basic/Make
+++ b/mathcomp/basic/Make
@@ -12,4 +12,4 @@ path.v
 prime.v
 tuple.v
 
--R . mathcomp.discrete
+-R . mathcomp.basic
\ No newline at end of file
diff --git a/mathcomp/basic/Makefile b/mathcomp/basic/Makefile
index e872352..8f03823 100644
--- a/mathcomp/basic/Makefile
+++ b/mathcomp/basic/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/character/Makefile b/mathcomp/character/Makefile
index e872352..8f03823 100644
--- a/mathcomp/character/Makefile
+++ b/mathcomp/character/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
index e872352..8f03823 100644
--- a/mathcomp/field/Makefile
+++ b/mathcomp/field/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
index e872352..8f03823 100644
--- a/mathcomp/fingroup/Makefile
+++ b/mathcomp/fingroup/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/odd_order/Makefile b/mathcomp/odd_order/Makefile
index e872352..8f03823 100644
--- a/mathcomp/odd_order/Makefile
+++ b/mathcomp/odd_order/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/real_closed/Makefile b/mathcomp/real_closed/Makefile
index e872352..8f03823 100644
--- a/mathcomp/real_closed/Makefile
+++ b/mathcomp/real_closed/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile
index e872352..8f03823 100644
--- a/mathcomp/solvable/Makefile
+++ b/mathcomp/solvable/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
index b24b0a6..eb28351 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
@@ -1025,6 +1025,10 @@ let interp_pattern ist gl red redty =
 let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;;
 let interp_rpattern ist gl red = interp_pattern ist gl red None;;
 
+let id_of_pattern = function
+  | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None)
+  | _ -> None
+
 (* The full occurrence set *)
 let noindex = Some(false,[])
 
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli
index 4c6bfac..53d2cff 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli
@@ -2,6 +2,7 @@
 
 open Genarg
 open Environ
+open Tacmach
 open Evd
 open Proof_type
 open Term
@@ -63,7 +64,7 @@ val redex_of_pattern : ?resolve_typeclasses:bool -> env -> pattern -> constr
 (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
 val interp_rpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   rpattern ->
     pattern
 
@@ -71,7 +72,7 @@ val interp_rpattern :
     in the current [Ltac] interpretation signature [ise] and tactic input [gl].
     [ty] is an optional type for the redex of [cpat] *)
 val interp_cpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   cpattern -> glob_constr_and_expr option ->
     pattern
 
@@ -208,8 +209,7 @@ val mk_tpattern_matcher :
 (* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns
  * the conclusion of [gl] where [occ] occurrences of [t] have been replaced
  * by [Rel 1] and the instance of [t] *)
-val pf_fill_occ_term :
-  goal Tacmach.sigma -> occ -> evar_map * constr -> constr * constr
+val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr
 
 (* It may be handy to inject a simple term into the first form of cpattern *)
 val cpattern_of_term : char * glob_constr_and_expr -> cpattern
@@ -232,13 +232,13 @@ val assert_done : 'a option ref -> 'a
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map
-val pf_unify_HO : goal Tacmach.sigma -> constr -> constr -> goal Tacmach.sigma
+val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma
 
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
 val tag_of_cpattern : cpattern -> char
 val loc_of_cpattern : cpattern -> Util.loc
-val id_of_cpattern : cpattern -> Names.variable option
+val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
 val rawltacctx : ltacctx
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 705c4ec..815a0fb 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -1,6 +1,6 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import Bool. (* For bool_scope delimiter 'bool'. *)
-Require Import mathcomp.ssreflect.ssrmatching.
+Require Import ssrmatching.
 Declare ML Module "ssreflect".
 Set SsrAstVersion.
 
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index 6b82548..721d34b 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -1,6 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import mathcomp.ssreflect.ssreflect.
-
+Require Import ssreflect.
 
 (******************************************************************************)
 (* This file contains the basic definitions and notations for working with    *)
diff --git a/mathcomp/ssrtest/Makefile b/mathcomp/ssrtest/Makefile
index 4bcf4fb..8f03823 100644
--- a/mathcomp/ssrtest/Makefile
+++ b/mathcomp/ssrtest/Makefile
@@ -1,26 +1,42 @@
-MAKEFLAGS := -r
+H=@
 
-.SUFFIXES:
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
 
-.PHONY: clean all config tags install
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
 
-COQMAKEFILE := Makefile.coq
-COQMAKE := +$(MAKE) -f $(COQMAKEFILE)
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
 
-all: $(COQMAKEFILE)
-	$(COQMAKE) all
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
 
-$(COQMAKEFILE) config:
-	$(COQBIN)coq_makefile -f Make  -o $(COQMAKEFILE)
 
-clean: $(COQMAKEFILE)
-	$(COQMAKE) clean
-	$(RM) -rf $(COQMAKEFILE)
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
 
-tags:
-	$(COQBIN)coqtags `find . -name \*.v`
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
 
-install:
+OLD_MAKEFLAGS:=$(MAKEFLAGS)
+MAKEFLAGS+=-B
+
+.DEFAULT_GOAL := all
+
+%:
+	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
+
+.PHONY: clean
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
 
-%: Makefile.coq
-	$(COQMAKE) $@