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

21 files changed, 102 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index eb410b1e32..11d8a3061f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -274,6 +274,7 @@ let rec attribute_of_vernac_command = function
   | VernacSyntacticDefinition _ -> []
   | VernacDeclareImplicits _ -> []
   | VernacReserve _ -> []
+  | VernacGeneralizable _ -> []
   | VernacSetOpacity _ -> []
   | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
   | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a55daff364..93f4eedff2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -24,8 +24,49 @@ open Libnames
 open Typeclasses
 open Typeclasses_errors
 open Pp
+open Libobject
+open Nameops
 (*i*)
 
+let generalizable_table = ref Idpred.empty
+
+let _ =
+  Summary.declare_summary "generalizable-ident"
+    { Summary.freeze_function = (fun () -> !generalizable_table);
+      Summary.unfreeze_function = (fun r -> generalizable_table := r);
+      Summary.init_function = (fun () -> generalizable_table := Idpred.empty) }
+
+let declare_generalizable_ident table (loc,id) =
+  if id <> root_of_id id then
+    user_err_loc(loc,"declare_generalizable_ident",
+    (pr_id id ++ str
+      " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
+  if Idpred.mem id table then
+    user_err_loc(loc,"declare_generalizable_ident",
+		(pr_id id++str" is already declared as a generalizable identifier"))
+  else Idpred.add id table
+
+let add_generalizable gen table =
+  match gen with
+  | None -> Idpred.empty
+  | Some [] -> Idpred.full
+  | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid)
+      table l
+
+let cache_generalizable_type (_,(local,cmd)) =
+  generalizable_table := add_generalizable cmd !generalizable_table
+    
+let (in_generalizable, _) =
+  declare_object {(default_object "GENERALIZED-IDENT") with
+    cache_function = cache_generalizable_type;
+    classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
+  }
+    
+let declare_generalizable local gen =
+ Lib.add_anonymous_leaf (in_generalizable (local, gen))
+
+let find_generalizable_ident id = Idpred.mem (root_of_id id) !generalizable_table
+
 let ids_of_list l =
   List.fold_right Idset.add l Idset.empty
 
@@ -51,13 +92,16 @@ let is_freevar ids env x =
 (* Auxilliary functions for the inference of implicitly quantified variables. *)
 
 let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
-  let found id bdvars l =
+  let found loc id bdvars l =
     if List.mem id l then l
-    else if not (is_freevar bdvars (Global.env ()) id)
-    then l else id :: l
+    else if is_freevar bdvars (Global.env ()) id
+    then
+      if find_generalizable_ident id then id :: l
+      else user_err_loc (loc, "Generalization", str "Unbound and ungeneralizable variable " ++ pr_id id)
+    else l
   in
   let rec aux bdvars l c = match c with
-    | CRef (Ident (_,id)) -> found id bdvars l
+    | CRef (Ident (loc,id)) -> found loc id bdvars l
     | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
 	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
@@ -204,14 +248,14 @@ let combine_params_freevar =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
+    | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l
     | CAppExpl (loc, (None, ref), l) -> loc, ref, l
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None,CRef ref), l) -> loc, ref, l
+    | CApp (loc, (None, CRef ref), l) -> loc, ref, l
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 0d28eccad6..8f02eb7658 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -24,6 +24,8 @@ open Libnames
 open Typeclasses
 (*i*)
 
+val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
+
 val ids_of_list : identifier list -> Idset.t
 val destClassApp : constr_expr -> loc * reference * constr_expr list
 val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e1a71ff23f..52cb3d8989 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -518,7 +518,7 @@ GEXTEND Gram
 	 pri = OPT [ "|"; i = natural -> i ] ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> r |
 	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
-	   VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
+	   VernacInstance (not (use_section_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
 
       | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
@@ -545,7 +545,12 @@ GEXTEND Gram
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
-	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
+	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c)
+
+      | IDENT "Generalizable"; ["Variable" | IDENT "Variables"];
+           gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | 
+	       idl = LIST1 identref -> Some idl ] ->
+	     VernacGeneralizable (use_section_locality (), gen) ] ]
   ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 76098e4fb1..8a8248bf4c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -831,7 +831,8 @@ let rec pr_vernac = function
         (pr_locality local ++ str "Ltac " ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacCreateHintDb (local,dbname,b) ->
-      hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
+      hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ 
+		str dbname ++ (if b then str" discriminated" else mt ()))
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_constr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
@@ -851,6 +852,14 @@ let rec pr_vernac = function
         str (if List.length idl > 1 then "s " else " ") ++
         prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++
         pr_lconstr c)
+  | VernacGeneralizable (local, g) ->
+      hov 1 (pr_locality local ++ str"Generalizable Variable" ++
+		match g with
+		| None -> str "s none"
+		| Some [] -> str "s all"
+		| Some idl ->
+		    str (if List.length idl > 1 then "s " else " ") ++
+		      prlist_with_sep spc pr_lident idl)
   | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
       hov 1 (str"Transparent" ++ pr_non_locality b ++
              spc() ++ prlist_with_sep sep pr_smart_global l)
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index b4e0e69bbf..627cd517c3 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -2183,6 +2183,7 @@ let rec xlate_vernac =
 			       List.map (fun (_,x) -> xlate_ident x) l),
 		 xlate_formula f)
   | VernacReserve([], _) -> assert false
+  | VernacGeneralizable (_, _) -> xlate_error "TODO: Generalizable"
   | VernacLocate(LocateTerm id) -> CT_locate(loc_smart_global_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
   | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module"
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). *)
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 22c838c267..18f3181b66 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -39,7 +39,7 @@
    [Bell93] John L. Bell, Hilbert's epsilon operator and classical
    logic, Journal of Philosophical Logic, 22: 1-18, 1993
 
-   [Carlström04] Jesper Carlström, [EM + Ext_ + AC_int <-> AC_ext],
+   [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
    Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
 *)
 
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index 2ba9692174..bd99198f4b 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -489,6 +489,8 @@ Qed.
 (* [fold], [filter], [for_all], [exists_] and [partition] requires
   some knowledge on [f] in order to be known as morphisms. *)
 
+Generalizable Variables f.
+
 Instance filter_equal `(Proper _ (E.eq==>Logic.eq) f) :
  Proper (Equal==>Equal) (filter f).
 Proof.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index fdb1ccc24e..c72d3a79dc 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -270,6 +270,8 @@ Definition FstRel {A B}(R:relation A) : relation (A*B) :=
 Definition SndRel {A B}(R:relation B) : relation (A*B) :=
  fun p p' => R (snd p) (snd p').
 
+Generalizable Variables A B RA RB Ri Ro.
+
 Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) :
  Equivalence (ProdRel RA RB).
 Proof. firstorder. Qed.
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 486c8804f4..31af75fee0 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -402,10 +402,10 @@ let main_targets vfiles mlfiles other_targets inc =
 	print "spec: $(VIFILES)\n\n";
 	print "gallina: $(GFILES)\n\n";
 	print "html: $(GLOBFILES) $(VFILES)\n";
-	print "\t- mkdir html\n";
+	print "\t- mkdir -p html\n";
 	print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
 	print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
-	print "\t- mkdir html\n";
+	print "\t- mkdir -p html\n";
 	print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
 	print "all.ps: $(VFILES)\n";
 	print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 754f58a9ca..70feb6ceb7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -771,6 +771,8 @@ let vernac_reserve idl c =
   let t = Detyping.detype false [] [] t in
   List.iter (fun id -> Reserve.declare_reserved_type id t) idl
 
+let vernac_generalizable = Implicit_quantifiers.declare_generalizable
+
 let make_silent_if_not_pcoq b =
   if !pcoq <> None then
     error "Turning on/off silent flag is not supported in Pcoq mode."
@@ -1375,6 +1377,7 @@ let interp c = match c with
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
+  | VernacGeneralizable (local,gen) -> vernac_generalizable local gen
   | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
   | VernacSetOption (locality,key,v) -> vernac_set_option locality key v
   | VernacUnsetOption (locality,key) -> vernac_unset_option locality key
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 25642bdc71..2e73767c58 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -301,6 +301,7 @@ type vernac_expr =
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
       (explicitation * bool * bool) list option
   | VernacReserve of lident list * constr_expr
+  | VernacGeneralizable of locality_flag * (lident list) option
   | VernacSetOpacity of
       locality_flag * (Conv_oracle.level * reference or_by_notation list) list
   | VernacUnsetOption of full_locality_flag * Goptions.option_name