Merge remote-tracking branch 'upstream/trunk' into trunk

16 files changed, 15 insertions, 103 deletions

diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 3d7ef01fb1..cfe0e08edb 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -305,9 +305,7 @@ Section Binary.
     fun x y => sum (R x y) (R' x y).
   
   (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-  
-  Set Automatic Introduction.
-  
+
   Global Instance relation_equivalence_equivalence :
     Equivalence relation_equivalence.
   Proof. split; red; unfold relation_equivalence, iffT. firstorder. 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 11c204dae5..57728d305d 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -433,9 +433,7 @@ Section Binary.
     @predicate_union (A::A::Tnil) R R'.
   
   (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-  
-  Set Automatic Introduction.
-  
+
   Global Instance relation_equivalence_equivalence :
     Equivalence relation_equivalence.
   Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
deleted file mode 100644
index a3e23f91c9..0000000000
--- a/theories/Compat/Coq84.v
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v8.4 *)
-
-(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *)
-Require Export Coq.Compat.Coq85.
-
-(** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *)
-(** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available.  But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *)
-Require Coq.omega.Omega.
-Ltac omega := Coq.omega.Omega.omega.
-
-(** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
-Global Set Asymmetric Patterns.
-
-(** The automatic elimination schemes for records were dropped by default in 8.5.  This restores the default behavior of Coq 8.4. *)
-Global Set Nonrecursive Elimination Schemes.
-
-(** See bug 3545 *)
-Global Set Universal Lemma Under Conjunction.
-
-(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *)
-Global Unset Refolding Reduction.
-
-(** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
-Ltac constructor_84_n n := constructor n.
-Ltac constructor_84_tac tac := once (constructor; tac).
-
-Tactic Notation "constructor" := Coq.Init.Notations.constructor.
-Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
-Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
-
-(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *)
-Ltac econstructor_84_n n := econstructor n.
-Ltac econstructor_84_tac tac := once (econstructor; tac).
-
-Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
-Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
-Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.
-
-(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
-Tactic Notation "reflexivity" := reflexivity.
-Tactic Notation "assumption" := assumption.
-Tactic Notation "etransitivity" := etransitivity.
-Tactic Notation "cut" constr(c) := cut c.
-Tactic Notation "exact_no_check" constr(c) := exact_no_check c.
-Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c.
-Tactic Notation "casetype" constr(c) := casetype c.
-Tactic Notation "elimtype" constr(c) := elimtype c.
-Tactic Notation "lapply" constr(c) := lapply c.
-Tactic Notation "transitivity" constr(c) := transitivity c.
-Tactic Notation "left" := left.
-Tactic Notation "eleft" := eleft.
-Tactic Notation "right" := right.
-Tactic Notation "eright" := eright.
-Tactic Notation "symmetry" := symmetry.
-Tactic Notation "split" := split.
-Tactic Notation "esplit" := esplit.
-
-(** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
-Require Coq.Numbers.Natural.Peano.NPeano.
-
-(** The following coercions were declared by default in Specif.v. *)
-Coercion sig_of_sig2 : sig2 >-> sig.
-Coercion sigT_of_sigT2 : sigT2 >-> sigT.
-Coercion sigT_of_sig : sig >-> sigT.
-Coercion sig_of_sigT : sigT >-> sig.
-Coercion sigT2_of_sig2 : sig2 >-> sigT2.
-Coercion sig2_of_sigT2 : sigT2 >-> sig2.
-
-(** In 8.4, the statement of admitted lemmas did not depend on the section
-    variables. *)
-Unset Keep Admitted Variables.
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v
index 6952fdf199..4a511d6c48 100644
--- a/theories/Compat/Coq86.v
+++ b/theories/Compat/Coq86.v
@@ -6,4 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Compatibility file for making Coq act similar to Coq v8.6 *)
\ No newline at end of file
+(** Compatibility file for making Coq act similar to Coq v8.6 *)
+Require Export Coq.extraction.Extraction.
+Require Export Coq.funind.FunInd.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index c9e5b8dd20..4a790296bb 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -16,7 +16,7 @@
     See the comments at the beginning of FSetAVL for more details.
 *)
 
-Require Import FMapInterface FMapList ZArith Int.
+Require Import FunInd FMapInterface FMapList ZArith Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index a7be32328d..b8e362f159 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -25,7 +25,7 @@
 
 *)
 
-Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
+Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 5acdb7eb7e..aadef476d7 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -12,7 +12,7 @@
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
-Require Import FMapInterface.
+Require Import FunInd FMapInterface.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 130cbee871..8124097020 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -11,7 +11,7 @@
 (** This file proposes an implementation of the non-dependent interface
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
-Require Import FMapInterface.
+Require Import FunInd FMapInterface.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index edcd53005e..2b0fe13620 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -89,11 +89,5 @@ Open Scope type_scope.
 (** ML Tactic Notations *)
 
 Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
-Declare ML Module "extratactics".
-Declare ML Module "g_auto".
-Declare ML Module "g_class".
-Declare ML Module "g_eqdecide".
-Declare ML Module "g_rewrite".
 
 Global Set Default Proof Mode "Classic".
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e71a8774ed..28049e9ee5 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -18,9 +18,7 @@ Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
 (* Initially available plugins
    (+ nat_syntax_plugin loaded in Datatypes) *)
-Declare ML Module "extraction_plugin".
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
-Declare ML Module "recdef_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 1e409607ae..886533586f 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -2,7 +2,7 @@ Require Import Notations.
 Require Import Datatypes.
 Require Import Logic.
 
-Local Declare ML Module "tauto".
+Declare ML Module "tauto_plugin".
 
 Local Ltac not_dep_intros :=
   repeat match goal with
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index a3c265a21f..b30cb6b565 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -31,7 +31,7 @@
     code after extraction.
 *)
 
-Require Import MSetInterface MSetGenTree BinInt Int.
+Require Import FunInd MSetInterface MSetGenTree BinInt Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 154c2384c8..036ff1aa4b 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -27,7 +27,7 @@
      - min_elt max_elt choose
 *)
 
-Require Import Orders OrdersFacts MSetInterface PeanoNat.
+Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat.
 Local Open Scope list_scope.
 Local Open Scope lazy_bool_scope.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index c490ea5166..6e51f61873 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -69,6 +69,7 @@ Section Well_founded.
 
 End Well_founded.
 
+Require Coq.extraction.Extraction.
 Extraction Inline Fix_F_sub Fix_sub.
 
 Set Implicit Arguments.
diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v
index c0ababfff5..e433ecffa1 100644
--- a/theories/QArith/Qcabs.v
+++ b/theories/QArith/Qcabs.v
@@ -22,7 +22,7 @@ Lemma Qcabs_canon (x : Q) : Qred x = x -> Qred (Qabs x) = Qabs x.
 Proof. intros H; now rewrite (Qred_abs x), H. Qed.
 
 Definition Qcabs (x:Qc) : Qc := {| canon := Qcabs_canon x (canon x) |}.
-Notation "[ q ]" := (Qcabs q) (q at next level, format "[ q ]") : Qc_scope.
+Notation "[ q ]" := (Qcabs q) : Qc_scope.
 
 Ltac Qc_unfolds :=
   unfold Qcabs, Qcminus, Qcopp, Qcplus, Qcmult, Qcle, Q2Qc, this.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 3697999f70..6a5233b643 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -150,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un)
 (* Compatibility *)
 Notation sequence_majorant := sequence_ub (only parsing).
 Notation sequence_minorant := sequence_lb (only parsing).
-Unset Standard Proposition Elimination Names.
+
 Lemma Wn_decreasing :
   forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
 Proof.