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 eb410b1e3..11d8a3061 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 a55daff36..93f4eedff 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 0d28eccad..8f02eb765 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 e1a71ff23..52cb3d898 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 76098e4fb..8a8248bf4 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 b4e0e69bb..627cd517c 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 e87482d84..bafbac3f1 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 78e66d374..cc8d79c03 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 8c6161036..5efa4fa8f 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 76da120e0..ac455415e 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 0d6130263..cc3cae4da 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 ef115b2ed..3789bb66f 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 33d98548d..995b37185 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 32e75adae..33b4350f8 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 c40e37e24..669be8b0f 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 22c838c26..18f3181b6 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 2ba969217..bd99198f4 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 fdb1ccc24..c72d3a79d 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 486c8804f..31af75fee 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 754f58a9c..70feb6ceb 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 25642bdc7..2e73767c5 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