Ajout option Local à Hint, Hints et HintDestruct

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

11 files changed, 102 insertions, 62 deletions

diff --git a/CHANGES b/CHANGES
index 9b7d2f7a2..6298e9bb9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Vernacular commands
    (TODO : doc).
 - "Implicit Variables Type x,y:t" assigns default types for binding variables.
 - "Set Implicits Printing" disable printing of implicit arguments
+- Declaration of Hints and Notation now accept a "Local" flag not to
+  be exported outside the current file even if not in section
 
 Gallina
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 54f22c646..c6baa0ecf 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1361,7 +1361,8 @@ let xlate_vernac =
 	  (fst::rest) -> CT_formula_ne_list(fst,rest)
 	| _ -> assert false in
       CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
-  | VernacHints (dbnames,h) ->
+  | VernacHints (local,dbnames,h) ->
+      (* TODO: locality flag *)
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
 	| HintsResolve [Some id_name, c] -> (* = Old HintResolve *)
@@ -1668,7 +1669,7 @@ let xlate_vernac =
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
      VernacSetOption (_, _)|VernacUnsetOption _|
-     VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _|
+     VernacHintDestruct (_, _, _, _, _, _)|VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
      VernacImport (_, _)|VernacExactProof _|VernacDistfix _|
      VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5acc694aa..5b2e165ac 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -87,17 +87,20 @@ GEXTEND Gram
 (* Hints for Auto and EAuto *)
 
       | IDENT "HintDestruct"; 
+	  local = locality;
           dloc = destruct_location;
           id  = base_ident;
           hyptyp = Constr.constr_pattern;
           pri = natural;
           "["; tac = tactic; "]" -> 
-	    VernacHintDestruct (id,dloc,hyptyp,pri,tac)
+	    VernacHintDestruct (local,id,dloc,hyptyp,pri,tac)
 
-      | IDENT "Hint"; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint
-          -> VernacHints (dbnames, h hintname)
+      | IDENT "Hint"; local = locality; hintname = base_ident; 
+	  dbnames = opt_hintbases; ":="; h = hint
+          -> VernacHints (local,dbnames, h hintname)
 	  
-      | IDENT "Hints"; (dbnames,h) = hints -> VernacHints (dbnames, h)
+      | IDENT "Hints"; local = locality; 
+	  (dbnames,h) = hints -> VernacHints (local,dbnames, h)
 	  
 
 (*This entry is not commented, only for debug*)
@@ -106,6 +109,9 @@ GEXTEND Gram
 	    [Genarg.in_gen Genarg.rawwit_constr c])
       ] ];
 
+  locality:
+    [ [ IDENT "Local" -> true | -> false ] ]
+  ;
   hint:
     [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c]
       | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index db8da7101..8cd36df1e 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -84,6 +84,7 @@ GEXTEND Gram
 (* Hints for Auto and EAuto *)
 
       | IDENT "HintDestruct"; 
+	  local = locality;
           dloc = destruct_location;
           id  = base_ident;
           hyptyp = Constr.constr_pattern;
@@ -91,10 +92,12 @@ GEXTEND Gram
           "["; tac = tactic; "]" -> 
 	    VernacHintDestruct (id,dloc,hyptyp,pri,tac)
 
-      | IDENT "Hint"; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint
-          -> VernacHints (dbnames, h hintname)
+      | IDENT "Hint"; local = locality; hintname = base_ident; 
+	  dbnames = opt_hintbases; ":="; h = hint ->
+            VernacHints (dbnames, h hintname)
 	  
-      | IDENT "Hints"; (dbnames,h) = hints -> VernacHints (dbnames, h)
+      | IDENT "Hints"; local = locality; (dbnames,h) = hints ->
+	  VernacHints (dbnames, h)
 	  
 
 (*This entry is not commented, only for debug*)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 638f6d727..c7186e412 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -278,7 +278,7 @@ let add_hint dbname hintlist =
     let db = Hint_db.add_list hintlist Hint_db.empty in
     searchtable_add (dbname,db)
 
-let cache_autohint (_,(name,hintlist)) = add_hint name hintlist
+let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist
 
 (*  let recalc_hints hintlist =
     let env = Global.env() and sigma = Evd.empty in
@@ -317,7 +317,7 @@ let forward_subst_tactic =
 
 let set_extern_subst_tactic f = forward_subst_tactic := f
 
-let subst_autohint (_,subst,(name,hintlist as obj)) = 
+let subst_autohint (_,subst,(local,name,hintlist as obj)) = 
   let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in
   let trans_data data code = 	      
     { data with
@@ -359,14 +359,13 @@ let subst_autohint (_,subst,(name,hintlist as obj)) =
   in
   let hintlist' = list_smartmap subst_hint hintlist in
     if hintlist' == hintlist then obj else
-      (name,hintlist')
+      (local,name,hintlist')
 
-let classify_autohint (_,((name,hintlist) as obj)) =
-  match hintlist with
-      [] -> Dispose   
-    | _ -> Substitute obj
+let classify_autohint (_,((local,name,hintlist) as obj)) =
+  if local or hintlist = [] then Dispose else Substitute obj
 
-let export_autohint x = Some x
+let export_autohint ((local,name,hintlist) as obj) =
+  if local then None else Some obj
 
 let (inAutoHint,outAutoHint) =
   declare_object {(default_object "AUTOHINT") with
@@ -380,12 +379,12 @@ let (inAutoHint,outAutoHint) =
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
-let add_resolves env sigma clist dbnames =
+let add_resolves env sigma clist local dbnames =
   List.iter 
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (dbname,
+	    (local,dbname,
      	     List.flatten
 	       (List.map
 		  (fun (name,c) -> 
@@ -397,14 +396,14 @@ let add_resolves env sigma clist dbnames =
     dbnames
 
 
-let add_unfolds l dbnames =
+let add_unfolds l local dbnames =
   List.iter 
     (fun dbname -> Lib.add_anonymous_leaf 
-       (inAutoHint (dbname, List.map make_unfold l)))
+       (inAutoHint (local,dbname, List.map make_unfold l)))
     dbnames
 
 
-let add_extern name pri (patmetas,pat) tacast dbname =
+let add_extern name pri (patmetas,pat) tacast local dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
 (* TODO
@@ -417,16 +416,16 @@ let add_extern name pri (patmetas,pat) tacast dbname =
 	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
+	  (inAutoHint(local,dbname, [make_extern name pri pat tacast]))
 
-let add_externs name pri pat tacast dbnames = 
-  List.iter (add_extern name pri pat tacast) dbnames
+let add_externs name pri pat tacast local dbnames = 
+  List.iter (add_extern name pri pat tacast local) dbnames
 
-let add_trivials env sigma l dbnames =
+let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(dbname, List.map (make_trivial env sigma) l)))
+	 inAutoHint(local,dbname, List.map (make_trivial env sigma) l)))
     dbnames
 
 let forward_intern_tac = 
@@ -434,7 +433,7 @@ let forward_intern_tac =
 
 let set_extern_intern_tac f = forward_intern_tac := f
 
-let add_hints dbnames h =
+let add_hints local dbnames h =
   let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
   | HintsResolve lhints ->	
       let env = Global.env() and sigma = Evd.empty in
@@ -444,7 +443,7 @@ let add_hints dbnames h =
 	  | None -> id_of_global (reference_of_constr c)
 	  | Some n -> n in
 	(n,c) in
-      add_resolves env sigma (List.map f lhints) dbnames
+      add_resolves env sigma (List.map f lhints) local dbnames
   | HintsImmediate lhints ->
       let env = Global.env() and sigma = Evd.empty in
       let f (n,c) = 
@@ -453,7 +452,7 @@ let add_hints dbnames h =
 	  | None -> id_of_global (reference_of_constr c)
 	  | Some n -> n in
 	(n,c) in
-      add_trivials env sigma (List.map f lhints) dbnames
+      add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
       let f (n,locqid) =
 	let r = Nametab.global locqid in
@@ -461,18 +460,18 @@ let add_hints dbnames h =
 	  | None -> id_of_global r
 	  | Some n -> n in
 	(n,r) in
-      add_unfolds (List.map f lhints) dbnames
+      add_unfolds (List.map f lhints) local dbnames
   | HintsConstructors (hintname, qid) ->
       let env = Global.env() and sigma = Evd.empty in
       let isp = global_inductive qid in
       let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
       let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in
       let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in
-      add_resolves env sigma lcons dbnames
+      add_resolves env sigma lcons local dbnames
   | HintsExtern (hintname, pri, patcom, tacexp) ->
       let pat =	Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in
       let tacexp = !forward_intern_tac (fst pat) tacexp in
-      add_externs hintname pri pat tacexp dbnames
+      add_externs hintname pri pat tacexp local dbnames
 
 (**************************************************************************)
 (*                    Functions for printing the hints                    *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a8d8cf1df..ef2571baa 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -20,6 +20,7 @@ open Pattern
 open Environ
 open Evd
 open Libnames
+open Vernacexpr
 (*i*)
   
 type auto_tactic = 
@@ -61,7 +62,7 @@ type hint_db_table = Hint_db.t Stringmap.t ref
 
 type hint_db_name = string
 
-val add_hints : hint_db_name list -> Vernacexpr.hints -> unit
+val add_hints : locality_flag -> hint_db_name list -> hints -> unit
 
 val print_searchtable : unit -> unit
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 313ddabcf..252e302c2 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -138,15 +138,25 @@ open Libnames
 type destructor_pattern = {
   d_typ: constr_pattern; 
   d_sort: constr_pattern }
-    
+
+let subst_destructor_pattern subst { d_typ = t; d_sort = s } =
+  { d_typ = subst_pattern subst t; d_sort = subst_pattern subst s }
+
 (* hypothesis patterns might need to do matching on the conclusion, too.
  * conclusion-patterns only need to do matching on the hypothesis *)
 type located_destructor_pattern =
-   (* discadable , pattern for hyp, pattern for concl *)
+   (* discardable, pattern for hyp, pattern for concl *)
    (bool * destructor_pattern * destructor_pattern,
    (* pattern for concl *)
    destructor_pattern) location
 
+let subst_located_destructor_pattern subst = function
+  | HypLocation (b,d,d') -> 
+      HypLocation
+        (b,subst_destructor_pattern subst d, subst_destructor_pattern subst d')
+  | ConclLocation d ->
+      ConclLocation (subst_destructor_pattern subst d)
+
 type destructor_data = {
   d_pat : located_destructor_pattern;
   d_pri : int;
@@ -186,9 +196,14 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_section = true }
+      Summary.survive_section = false }
 
-let cache_dd (_,(na,dd)) =
+let forward_subst_tactic = 
+  ref (fun _ -> failwith "subst_tactic is not installed for DHyp")
+
+let set_extern_subst_tactic f = forward_subst_tactic := f
+
+let cache_dd (_,(_,na,dd)) =
   try 
     add (na,dd)
   with _ -> 
@@ -196,16 +211,23 @@ let cache_dd (_,(na,dd)) =
       (str"The code which adds destructor hints broke;" ++ spc () ++ 
 	 str"this is not supposed to happen")
 
-let export_dd x = Some x
+let classify_dd (_,(local,_,_ as o)) =
+  if local then Dispose else Substitute o
+
+let export_dd (local,_,_ as x) = if local then None else Some x
 
-type destructor_data_object = identifier * destructor_data
+let subst_dd (_,subst,(local,na,dd)) =
+  (local,na,
+  { d_pat = subst_located_destructor_pattern subst dd.d_pat;
+    d_pri = dd.d_pri; 
+    d_code = !forward_subst_tactic subst dd.d_code })
 
-let ((inDD : destructor_data_object->obj),
-     (outDD : obj->destructor_data_object)) =
+let (inDD,outDD) =
   declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                     cache_function = cache_dd;
 		    open_function = (fun i o -> if i=1 then cache_dd o);
-                    (* TODO: substitution *)
+                    subst_function = subst_dd;
+		    classify_function = classify_dd;
                     export_function = export_dd }
 
 let forward_intern_tac = 
@@ -216,7 +238,7 @@ let set_extern_intern_tac f = forward_intern_tac := f
 let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
 let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
     
-let add_destructor_hint na loc pat pri code =
+let add_destructor_hint local na loc pat pri code =
   let code = !forward_intern_tac code in
   let code =
     begin match loc, code with
@@ -236,7 +258,7 @@ let add_destructor_hint na loc pat pri code =
     | ConclLocation () ->
 	ConclLocation({d_typ=pat;d_sort=catch_all_sort_pattern}) in
   Lib.add_anonymous_leaf
-    (inDD (na,{ d_pat = pat; d_pri=pri; d_code=code }))
+    (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
 
 let match_dpat dp cls gls =
   let cltyp = clause_type cls gls in
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index b4ecfeac8..9a46136f9 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -28,5 +28,5 @@ val h_destructConcl : tactic
 val h_auto_tdb : int option -> tactic
 
 val add_destructor_hint :
-  identifier -> (bool,unit) Tacexpr.location ->
+  Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
     Topconstr.constr_expr -> int -> raw_tactic_expr -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8d21c4d76..1d2ccecbb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1202,8 +1202,9 @@ let interp c = match c with
 
   (* Commands *)
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
-  | VernacHints (dbnames,hints) -> vernac_hints dbnames hints
-  | VernacHintDestruct (id,l,p,n,tac) -> Dhyp.add_destructor_hint id l p n tac
+  | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
+  | VernacHintDestruct (local,id,l,p,n,tac) -> 
+      Dhyp.add_destructor_hint local id l p n tac
   | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n
   | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 22478b880..e03658cfd 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -227,8 +227,8 @@ type vernac_expr =
   (* Commands *)
   | VernacDeclareTacticDefinition of
       rec_flag * (identifier located * raw_tactic_expr) list
-  | VernacHints of string list * hints
-  | VernacHintDestruct of
+  | VernacHints of locality_flag * string list * hints
+  | VernacHintDestruct of locality_flag *
       identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
   | VernacSyntacticDefinition of identifier * constr_expr * int option
   | VernacDeclareImplicits of reference * int list option
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index f6577dc14..7f8497457 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -155,7 +155,7 @@ let pr_opt_hintbases l = match l with
   | [] -> mt()
   | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
 
-let pr_hints db h pr_c = 
+let pr_hints local db h pr_c = 
   let db_name = function
     | [] -> (false , mt())
     | c1::c2 -> match c1 with
@@ -169,38 +169,42 @@ let pr_hints db h pr_c =
     | HintsResolve l ->
         let (f,dbn) = db_name l in
         if f then
-          hov 1 (str"Hint " ++ dbn ++ spc() ++ opth ++
+          hov 1 (str"Hint " ++ pr_locality local ++ dbn ++ spc() ++ opth ++
                  str" :=" ++ spc() ++ str"Resolve" ++ spc() ++
                  prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l))
         else hov 1
-          (str"Hints Resolve " ++
+          (str"Hints " ++ pr_locality local ++ str "Resolve " ++
           prlist_with_sep sep pr_aux
             (List.map (fun (_,y) -> y) l) ++ spc() ++ opth)
     | HintsImmediate l ->
         let (f,dbn) = db_name l in
         if f then
-          hov 1 (str"Hint " ++ dbn ++ spc() ++ opth ++
+          hov 1 (str"Hint " ++ pr_locality local ++ dbn ++ spc() ++ opth ++
                  str" :=" ++ spc() ++ str"Immediate" ++ spc() ++
                  prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l))
         else hov 1
-          (str"Hints Immediate " ++
+          (str"Hints " ++ pr_locality local ++ str "Immediate " ++
            prlist_with_sep sep pr_aux
             (List.map (fun (_,y) -> y) l) ++ spc() ++ opth)
     | HintsUnfold l ->
         let (f,dbn) = db_name l in
         if f then
-          hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++
+          hov 1 (str"Hint" ++ spc() ++ pr_locality local ++ 
+	         dbn ++ spc() ++ opth ++
                  str" :=" ++ spc() ++ str"Unfold" ++ spc() ++
                  prlist_with_sep sep pr_reference
                    (List.map snd l))
         else hov 1
-          (str"Hints Unfold " ++ prlist_with_sep sep pr_reference
+          (str"Hints " ++ pr_locality local ++ str "Unfold " ++
+	    prlist_with_sep sep pr_reference
             (List.map snd l) ++ spc() ++ opth)
     | HintsConstructors (n,c) ->
-        hov 1 (str"Hint " ++ pr_id n ++ spc() ++ opth ++ str" :=" ++
+        hov 1 (str"Hint " ++ pr_locality local ++ 
+	       pr_id n ++ spc() ++ opth ++ str" :=" ++
                spc() ++ str"Constructors" ++ spc() ++ pr_reference c) 
     | HintsExtern (name,n,c,tac) ->
-        hov 1 (str"Hint " ++ pr_id name ++ spc() ++ opth ++ str" :=" ++
+        hov 1 (str"Hint " ++ pr_locality local ++ 
+	       pr_id name ++ spc() ++ opth ++ str" :=" ++
                spc() ++ str"Extern " ++ int n ++ spc() ++ pr_c c ++
                spc() ++ pr_raw_tactic tac)
  
@@ -818,9 +822,10 @@ let rec pr_vernac = function
 	  str "Tactic Definition " else
 	    (* Rec by default *) str "Ltac ") ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
-  | VernacHints (dbnames,h) -> pr_hints dbnames h pr_constr
-  | VernacHintDestruct (id,loc,c,i,tac) ->
-      hov 2 (str"HintDestruct " ++ pr_destruct_location loc ++ spc() ++
+  | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr
+  | VernacHintDestruct (local,id,loc,c,i,tac) ->
+      hov 2 (str"HintDestruct " ++ pr_locality local ++ 
+      pr_destruct_location loc ++ spc() ++
       pr_id id ++ pr_constrarg c ++ pr_intarg i ++ spc() ++
       str"[" ++ pr_raw_tactic tac ++ str"]")
   | VernacSyntacticDefinition (id,c,None) ->