Suppression code pour hints nommés à la V7 (voire à la V6...)

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

7 files changed, 80 insertions, 130 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index e3656b1e10..128adb6073 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -470,7 +470,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
 		(true,false) 
-		hid (mkVar hid,body_of_type htyp)]
+		(mkVar hid,body_of_type htyp)]
 	   with Failure _ -> [] 
 	 in
          (free_try
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a42af9abf1..85fbea50cf 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1668,7 +1668,7 @@ let rec xlate_vernac =
   | VernacHints (local,dbnames,h) ->
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
-	| HintsConstructors (None, l) ->
+	| HintsConstructors l ->
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
@@ -1678,15 +1678,10 @@ let rec xlate_vernac =
 	   else
 	     CT_hints(CT_ident "Constructors",
 		      CT_id_ne_list(n1, names), dblist)
-	| HintsExtern (None, n, c, t) ->
+	| HintsExtern (n, c, t) ->
 	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
         | HintsResolve l | HintsImmediate l -> 
-	    let l = 
-	      List.map 
-	     	(function (None, f) -> xlate_formula f
-		   | _ -> 
-		       xlate_error "obsolete Hint Resolve not supported") l in
-	 let f1, formulas = match l  with
+	 let f1, formulas = match List.map xlate_formula l with
 	     a :: tl -> a, tl
 	   | _  -> failwith "" in
 	 let l' = CT_formula_ne_list(f1, formulas) in
@@ -1703,10 +1698,7 @@ let rec xlate_vernac =
 		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
 		| _ -> assert false)
         | HintsUnfold l -> 
-	 let l = List.map
-	   (function (None,ref) -> loc_qualid_to_ct_ID ref |
-	      _ -> xlate_error "obsolete Hint Unfold not supported") l in
-	 let n1, names = match l with
+	 let n1, names = match List.map loc_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
 	   if local then
@@ -1727,9 +1719,6 @@ let rec xlate_vernac =
 	       CT_hint_destruct
 		 (xlate_ident id, CT_int n, dl, xlate_formula f,
 		  xlate_tactic t, dblist)
-	| HintsExtern(Some _, _, _, _)
-	| HintsConstructors(Some _, _) -> 
-            xlate_error "obsolete Hint Constructors not supported"
 )
   | VernacEndProof (Proved (true,None)) ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 80dcf23e32..5d392846de 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -34,7 +34,7 @@ GEXTEND Gram
     | ":"; l = LIST1 IDENT -> l ] ]
   ;
   command:
-    [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c
+    [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" -> VernacProof (Tacexpr.TacId [])
       | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
       | IDENT "Abort" -> VernacAbort None
@@ -56,7 +56,7 @@ GEXTEND Gram
       | IDENT "Resume" -> VernacResume None
       | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
-      | IDENT "Proof"; c = Constr.lconstr -> VernacExactProof c
+      | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
       | IDENT "Focus" -> VernacFocus None
@@ -91,7 +91,7 @@ GEXTEND Gram
 	  
 
 (*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; c = Constr.constr -> 
+      | IDENT "PrintConstr"; c = constr -> 
 	  VernacExtend ("PrintConstr",
 	    [Genarg.in_gen Genarg.rawwit_constr c])
       ] ];
@@ -100,22 +100,18 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 Constr.constr ->
-          HintsResolve (List.map (fun c -> (None, c)) lc)
-      | IDENT "Immediate"; lc = LIST1 Constr.constr ->
-          HintsImmediate (List.map (fun c -> (None,c)) lc)
-      | IDENT "Unfold"; lqid = LIST1 global ->
-          HintsUnfold (List.map (fun g -> (None,g)) lqid)
-      | IDENT "Constructors"; lc = LIST1 global ->
-          HintsConstructors (None,lc)
-      | IDENT "Extern"; n = natural; c = Constr.constr_pattern ; "=>";
+    [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+      | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+      | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
+      | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
+      | IDENT "Extern"; n = natural; c = constr_pattern ; "=>";
           tac = tactic ->
-	  HintsExtern (None,n,c,tac)
-      | IDENT"Destruct"; 
+	  HintsExtern (n,c,tac)
+      | IDENT "Destruct"; 
           id = ident; ":=";
           pri = natural;
           dloc = destruct_location;
-          hyptyp = Constr.constr_pattern;
+          hyptyp = constr_pattern;
           "=>"; tac = tactic ->
             HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
     ;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 2444b1be9e..378417a124 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -184,18 +184,14 @@ let pr_hints local db h pr_c pr_pat =
   let pph =
     match h with
     | HintsResolve l ->
-        str "Resolve " ++
-        prlist_with_sep sep pr_c (List.map snd l)
+        str "Resolve " ++ prlist_with_sep sep pr_c l
     | HintsImmediate l ->
-        str"Immediate" ++ spc() ++
-        prlist_with_sep sep pr_c (List.map snd l)
+        str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
     | HintsUnfold l ->
-        str "Unfold " ++
-	prlist_with_sep sep pr_reference (List.map snd l)
-    | HintsConstructors (n,c) ->
-        str"Constructors" ++ spc() ++
-        prlist_with_sep spc pr_reference c
-    | HintsExtern (name,n,c,tac) ->
+        str "Unfold " ++ prlist_with_sep sep pr_reference l
+    | HintsConstructors c ->
+        str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
+    | HintsExtern (n,c,tac) ->
         str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++
         spc() ++ pr_raw_tactic tac
     | HintsDestruct(name,i,loc,c,tac) ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9d3a5a2881..3aaf3443ea 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -54,7 +54,6 @@ type auto_tactic =
   | Extern     of glob_tactic_expr       (* Hint Extern *) 
 
 type pri_auto_tactic = { 
-  hname : identifier;    (* name of the hint *)
   pri  : int;            (* A number between 0 and 4, 4 = lower priority *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   code : auto_tactic     (* the tactic to apply when the concl matches pat *)
@@ -183,20 +182,20 @@ let try_head_pattern c =
   try head_pattern_bound c
   with BoundPattern -> error "Bound head variable"
 
-let make_exact_entry name (c,cty) =
+let make_exact_entry (c,cty) =
   let cty = strip_outer_cast cty in
   match kind_of_term cty with
     | Prod (_,_,_) -> 
 	failwith "make_exact_entry"
     | _ ->
 	(head_of_constr_reference (List.hd (head_constr cty)),
-	   { hname=name; pri=0; pat=None; code=Give_exact c })
+	   { pri=0; pat=None; code=Give_exact c })
 
 let dummy_goal =
   {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty};
    sigma=Evd.empty}
 
-let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
+let make_apply_entry env sigma (eapply,verbose) (c,cty) =
   let cty = hnf_constr env sigma cty in
   match kind_of_term cty with
     | Prod _ ->
@@ -212,14 +211,12 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
 	    warn (str "the hint: eapply " ++ pr_lconstr c ++
 		  str " will only be used by eauto"); 
           (hd,
-           { hname = name;
-	     pri = nb_hyp cty + nmiss;
+           { pri = nb_hyp cty + nmiss;
              pat = Some pat;
              code = ERes_pf(c,{ce with templenv=empty_env}) })
         end else 
 	  (hd,
-           { hname = name;
-	     pri = nb_hyp cty;
+           { pri = nb_hyp cty;
              pat = Some pat;
              code = Res_pf(c,{ce with templenv=empty_env}) })
     | _ -> failwith "make_apply_entry"
@@ -228,49 +225,49 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
    c is a constr
    cty is the type of constr *)
 
-let make_resolves env sigma name eap (c,cty) =
+let make_resolves env sigma eap c =
+  let cty = type_of env sigma c in
   let ents = 
     map_succeed 
-      (fun f -> f name (c,cty)) 
-      [make_exact_entry; make_apply_entry env sigma eap]
+      (fun f -> f (c,cty)) 
+      [make_exact_entry; make_apply_entry env sigma (eap,Options.is_verbose())]
   in 
-  if ents = [] then 
-    errorlabstrm "Hint" (pr_lconstr c ++ spc () ++ str "cannot be used as a hint");
+  if ents = [] then
+    errorlabstrm "Hint" 
+      (pr_lconstr c ++ spc() ++ str"cannot be used as a hint");
   ents
 
+
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma (hname,_,htyp) = 
   try
-    [make_apply_entry env sigma (true, false) hname
+    [make_apply_entry env sigma (true, false)
        (mkVar hname,  htyp)]
   with 
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
 
 (* REM : in most cases hintname = id *)
-let make_unfold (hintname, ref, eref) =
+let make_unfold (ref, eref) =
   (ref,
-   { hname = hintname;
-     pri = 4;
+   { pri = 4;
      pat = None;
      code = Unfold_nth eref })
 
-let make_extern name pri pat tacast = 
+let make_extern pri pat tacast = 
   let hdconstr = try_head_pattern pat in 
   (hdconstr,
-   { hname = name;
-     pri=pri;
+   { pri=pri;
      pat = Some pat;
      code= Extern tacast })
 
-let make_trivial env sigma (name,c) =
+let make_trivial env sigma c =
   let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (List.hd (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
-  (hd, { hname = name;
-	       pri=1;
-               pat = Some (Pattern.pattern_of_constr (clenv_type ce));
-               code=Res_pf_THEN_trivial_fail(c,{ce with templenv=empty_env}) })
+  (hd, { pri=1;
+         pat = Some (Pattern.pattern_of_constr (clenv_type ce));
+         code=Res_pf_THEN_trivial_fail(c,{ce with templenv=empty_env}) })
 
 open Vernacexpr
 
@@ -362,19 +359,12 @@ let (inAutoHint,outAutoHint) =
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
 let add_resolves env sigma clist local dbnames =
-  List.iter 
+  List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (local,dbname,
-     	     List.flatten
-	       (List.map
-		  (fun (name,c) -> 
-		     let ty = type_of env sigma c in
-		     let verbose = Options.is_verbose() in
-		       make_resolves env sigma name (true,verbose) (c,ty)) clist
-	       )
-	    )))
+     	     List.flatten (List.map (make_resolves env sigma true) clist))))
     dbnames
 
 
@@ -385,7 +375,7 @@ let add_unfolds l local dbnames =
     dbnames
 
 
-let add_extern name pri (patmetas,pat) tacast local dbname =
+let add_extern 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 *)
   let tacmetas = [] in
@@ -395,10 +385,10 @@ let add_extern name pri (patmetas,pat) tacast local dbname =
 	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(local,dbname, [make_extern name pri pat tacast]))
+	  (inAutoHint(local,dbname, [make_extern pri pat tacast]))
 
-let add_externs name pri pat tacast local dbnames = 
-  List.iter (add_extern name pri pat tacast local) dbnames
+let add_externs pri pat tacast local dbnames = 
+  List.iter (add_extern pri pat tacast local) dbnames
 
 let add_trivials env sigma l local dbnames =
   List.iter
@@ -414,33 +404,16 @@ let set_extern_intern_tac f = forward_intern_tac := f
 
 let add_hints local dbnames0 h =
   let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
+  let env = Global.env() and sigma = Evd.empty in
+  let f = Constrintern.interp_constr sigma env in
   match h with
   | HintsResolve lhints ->	
-      let env = Global.env() and sigma = Evd.empty in
-      let f (n,c) =
-	let c = Constrintern.interp_constr sigma env c in
-	let n = match n with
-	  | None -> (*id_of_global (global_of_constr c)*)
-              id_of_string "<anonymous hint>"
-	  | Some n -> n in
-	(n,c) in
       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) = 
-	let c = Constrintern.interp_constr sigma env c in
-	let n = match n with
-	  | None -> (*id_of_global (global_of_constr c)*)
-              id_of_string "<anonymous hint>"
-	  | Some n -> n in
-	(n,c) in
       add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
-      let f (n,locqid) =
-	let r = Nametab.global locqid in
-	let n = match n with
-	  | None -> id_of_global r
-	  | Some n -> n in
+      let f qid =
+	let r = Nametab.global qid in
         let r' = match r with
          | ConstRef c -> EvalConstRef c
          | VarRef c -> EvalVarRef c
@@ -449,26 +422,21 @@ let add_hints local dbnames0 h =
             (str "Cannot coerce" ++ spc () ++ pr_global r ++ spc () ++
              str "to an evaluable reference")
         in
-	 (n,r,r') in
+	 (r,r') in
       add_unfolds (List.map f lhints) local dbnames
-  | HintsConstructors (hintname, lqid) ->
+  | HintsConstructors lqid ->
       let add_one 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 local dbnames in
       List.iter add_one lqid
-  | HintsExtern (hintname, pri, patcom, tacexp) ->
-      let hintname = match hintname with
-          Some h -> h
-        | _ -> id_of_string "<anonymous hint>" in
+  | HintsExtern (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 local dbnames
+      add_externs pri pat tacexp local dbnames
   | HintsDestruct(na,pri,loc,pat,code) ->
       if dbnames0<>[] then
         warn (str"Database selection not implemented for destruct hints");
@@ -760,7 +728,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
 		(true,false) 
-		hid (mkVar hid, htyp)]
+		(mkVar hid, htyp)]
 	   with Failure _ -> [] 
 	 in
          search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d] g') 
@@ -846,6 +814,14 @@ let h_dauto (n,p) =
 (*** A new formulation of Auto *********)
 (***************************************)
 
+let make_resolve_any_hyp env sigma (id,_,ty) =
+  let ents = 
+    map_succeed
+      (fun f -> f (mkVar id,ty)) 
+      [make_exact_entry; make_apply_entry env sigma (true,false)]
+  in 
+  ents
+
 type autoArguments =
   | UsingTDB       
   | Destructing   
@@ -885,10 +861,7 @@ let rec super_search n db_list local_db argl goal =
      ::
      (tclTHEN intro 
         (fun g -> 
-	   let (hid,_,htyp) = pf_last_hyp g in
-	   let hintl =
-	     make_resolves (pf_env g) (project g)
-	       hid (true,false) (mkVar hid, htyp) in
+	   let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in
 	   super_search n db_list (Hint_db.add_list hintl local_db)
 	     argl g))
      ::
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 6333e088b8..ee638499f1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -35,7 +35,6 @@ type auto_tactic =
 open Rawterm
 
 type pri_auto_tactic = { 
-  hname : identifier;     (* name of the hint *)
   pri   : int;            (* A number between 0 and 4, 4 = lower priority *)
   pat   : constr_pattern option; (* A pattern for the concl of the Goal *)
   code  : auto_tactic;    (* the tactic to apply when the concl matches pat *)
@@ -74,21 +73,18 @@ val print_hint_ref : global_reference -> unit
 val print_hint_db_by_name : hint_db_name -> unit
 
 (* [make_exact_entry hint_name (c, ctyp)]. 
-   [hint_name] is the name of then hint;
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [hc]. *)
 
-val make_exact_entry :
-  identifier -> constr * constr -> global_reference * pri_auto_tactic
+val make_exact_entry : constr * constr -> global_reference * pri_auto_tactic
 
-(* [make_apply_entry (eapply,verbose) name (c,cty)].
+(* [make_apply_entry (eapply,verbose) (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
-   [name] is the name of then hint;
    [c] is the term given as an exact proof to solve the goal;
    [cty] is the type of [hc]. *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool -> identifier -> constr * constr
+  env -> evar_map -> bool * bool -> constr * constr
       -> global_reference * pri_auto_tactic
 
 (* A constr which is Hint'ed will be:
@@ -99,8 +95,8 @@ val make_apply_entry :
        has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> identifier -> bool * bool -> constr * constr -> 
-    (global_reference * pri_auto_tactic) list
+  env -> evar_map -> bool -> constr -> 
+      (global_reference * pri_auto_tactic) list
 
 (* [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
@@ -111,10 +107,10 @@ val make_resolve_hyp :
   env -> evar_map -> named_declaration ->
       (global_reference * pri_auto_tactic) list
 
-(* [make_extern name pri pattern tactic_expr] *)
+(* [make_extern pri pattern tactic_expr] *)
 
 val make_extern :
-  identifier -> int -> constr_pattern -> Tacexpr.glob_tactic_expr
+  int -> constr_pattern -> Tacexpr.glob_tactic_expr
       -> global_reference * pri_auto_tactic
 
 val set_extern_interp :
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 36a0d237d2..0ba2610c4b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -108,11 +108,11 @@ type comment =
   | CommentInt of int
 
 type hints =
-  | HintsResolve of (identifier option * constr_expr) list
-  | HintsImmediate of (identifier option * constr_expr) list
-  | HintsUnfold of (identifier option * reference) list
-  | HintsConstructors of identifier option * reference list
-  | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr
+  | HintsResolve of constr_expr list
+  | HintsImmediate of constr_expr list
+  | HintsUnfold of reference list
+  | HintsConstructors of reference list
+  | HintsExtern of int * constr_expr * raw_tactic_expr
   | HintsDestruct of identifier *
       int * (bool,unit) location * constr_expr * raw_tactic_expr