reorganisation des niveaux (ex: = est a 70)

Hint Destruct: syntaxe similaire aux autres hints...


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

2 files changed, 37 insertions, 12 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4683ce144..de23d854b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -434,14 +434,16 @@ let forward_intern_tac =
 
 let set_extern_intern_tac f = forward_intern_tac := f
 
-let add_hints local dbnames h =
-  let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
+let add_hints local dbnames0 h =
+  let dbnames = if dbnames0 = [] then ["core"] else dbnames0 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 (reference_of_constr c)
+	  | None -> (*id_of_global (reference_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
@@ -450,7 +452,8 @@ let add_hints local dbnames h =
       let f (n,c) = 
 	let c = Constrintern.interp_constr sigma env c in
 	let n = match n with
-	  | None -> id_of_global (reference_of_constr c)
+	  | None -> (*id_of_global (reference_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
@@ -462,17 +465,28 @@ let add_hints local dbnames h =
 	  | Some n -> n in
 	(n,r) in
       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 local dbnames
+  | HintsConstructors (hintname, 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
       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
+  | HintsDestruct(na,pri,loc,pat,code) ->
+      if dbnames0<>[] then
+        warn (str"Database selection not implemented for destruct hints");
+      Dhyp.add_destructor_hint local na loc pat pri code
 
 (**************************************************************************)
 (*                    Functions for printing the hints                    *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6f87f1016..276e033ac 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -125,7 +125,8 @@ let add_rewrite_hint name ort t lcsr =
   let f c = Constrintern.interp_constr sigma env c, ort, t in
   add_rew_rules name (List.map f lcsr)
 
-VERNAC COMMAND EXTEND HintRewrite
+(* V7 *)
+VERNAC COMMAND EXTEND HintRewrite_v7
   [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] ->
   [ add_rewrite_hint b o Tacexpr.TacId l ]
 | [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b)
@@ -133,6 +134,16 @@ VERNAC COMMAND EXTEND HintRewrite
   [ add_rewrite_hint b o t l ]
 END
 
+(* V8 *)
+VERNAC COMMAND EXTEND HintRewrite
+  [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
+  [ add_rewrite_hint b o Tacexpr.TacId l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
+    ":" preident(b) ] ->
+  [ add_rewrite_hint b o t l ]
+END
+
+
 (* Refine *)
 
 open Refine