Add a new vernacular command for controling implicit generalization of

variables with syntax:
[Local?|Global] Generalizable Variable(s)? [all|none|id1 idn].
By default no variable is generalizable, so this patch breaks backward
compatibility with files that used implicit generalization (through
Instance declarations for example). To get back the old behavior, one
just needs to use [Global Generalizable Variables all].
Make coq_makefile more robust using [mkdir -p].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 20 insertions, 0 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index e87482d84c..bafbac3f1f 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -26,6 +26,8 @@ Require Import Coq.Bool.Bool.
 Require Import Coq.Arith.Peano_dec.
 Require Import Coq.Program.Program.
 
+Generalizable Variables A B R.
+
 Open Scope equiv_scope.
 
 Class DecidableEquivalence `(equiv : Equivalence A) :=
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 78e66d3740..cc8d79c03e 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -25,6 +25,8 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables A R eqA B S eqB.
+
 Open Local Scope signature_scope.
 
 Definition equiv `{Equivalence A R} : relation A := R.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 8c61610361..5efa4fa8f5 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -17,6 +17,8 @@
 Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Classes.Morphisms.
 
+Generalizable Variables A B eqA eqB RA RB f.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 76da120e05..ac455415ea 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -20,6 +20,8 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
+Generalizable Variables all.
+
 (** * Morphisms.
 
    We now turn to the definition of [Proper] and declare standard instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0d61302636..cc3cae4dab 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -74,6 +74,8 @@ Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
 
+Generalizable Variables A B C D R S T U eqA eqB eqC eqD.
+
 Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
 Proof. tauto. Qed.
 
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index ef115b2ed3..3789bb66f9 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -19,6 +19,8 @@ Require Import Coq.Program.Program.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables a.
+
 Require Export Coq.Classes.SetoidClass.
 
 (** Application of the extensionality axiom to turn a goal on
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 33d98548db..995b371853 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -17,6 +17,8 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables A.
+
 Require Import Coq.Program.Program.
 
 Require Import Relation_Definitions.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 32e75adae7..33b4350f83 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -18,6 +18,8 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables A B .
+
 (** Export notations. *)
 
 Require Export Coq.Classes.SetoidClass.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index c40e37e24c..669be8b0ff 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -18,6 +18,8 @@ Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
 Require Import Coq.Classes.Equivalence Coq.Program.Basics.
 
+Generalizable Variables A R.
+
 Export ProperNotations.
 
 Set Implicit Arguments.
@@ -177,3 +179,5 @@ Ltac default_add_morphism_tactic :=
 Ltac add_morphism_tactic := default_add_morphism_tactic.
 
 Obligation Tactic := program_simpl.
+
+(* Notation "'Morphism' s t " := (@Proper _ (s%signature) t) (at level 10, s at next level, t at next level). *)