Ground bugfix

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

2 files changed, 26 insertions, 17 deletions

diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index ebfb0e0181..95b162d288 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -16,8 +16,10 @@ open Ground
 open Goptions
 open Tactics
 open Tacticals
+open Tacinterp
 open Term
 open Names
+open Util
 open Libnames
 
 (* declaring search depth as a global option *)
@@ -52,7 +54,7 @@ let gen_ground_tac flag taco ext gl=
       qflag:=flag;
       let solver= 
 	match taco with 
-	    Some tac->tac
+	    Some tac-> tac
 	  | None-> default_solver in
       let startseq=
 	match ext with
@@ -80,18 +82,12 @@ let normalize_evaluables=
 	   (Tacexpr.InHypType id)) *)
 
 TACTIC EXTEND Ground
-    [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> 
-      [ gen_ground_tac true (Some (snd t)) (Ids l) ]
-|   [ "Ground" "with" ne_reference_list(l) ] -> 
-      [ gen_ground_tac true None (Ids l) ]
-|   [ "Ground" tactic(t) "using" ne_preident_list(l) ] -> 
-      [ gen_ground_tac true (Some (snd t)) (Bases l) ]
-|   [ "Ground" "using" ne_preident_list(l) ] -> 
-      [ gen_ground_tac true None (Bases l) ]
-|   [ "Ground" tactic(t) ] -> 
-      [ gen_ground_tac true (Some (snd t)) Void ]
-|   [ "Ground" ] ->
-      [ gen_ground_tac true None Void ]
+    [ "Ground" tactic_opt(t) "with" ne_reference_list(l) ] -> 
+      [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
+|   [ "Ground" tactic_opt(t) "using" ne_preident_list(l) ] -> 
+      [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
+|   [ "Ground" tactic_opt(t) ] -> 
+      [ gen_ground_tac true (option_app eval_tactic t) Void ]
 END
 
 TACTIC EXTEND GTauto   
@@ -100,9 +96,7 @@ TACTIC EXTEND GTauto
 END
 
 TACTIC EXTEND GIntuition
-   [ "GIntuition" tactic(t) ] ->
-     [ gen_ground_tac false (Some (snd t)) Void ]
-|  [ "GIntuition" ] ->
-     [ gen_ground_tac false (Some default_solver) Void ] 
+  [ "GIntuition" tactic_opt(t) ] ->
+     [ gen_ground_tac false (option_app eval_tactic t) Void ]
 END
 
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 06d3872251..65cb4d4be8 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -18,6 +18,7 @@ open Tactics
 open Tacticals
 open Libnames
 
+(*
 let old_search=ref !Auto.searchtable 
 
 (* I use this solution as a means to know whether hints have changed, 
@@ -41,6 +42,20 @@ let update_flags ()=
 	Closure.RedFlags.red_add_transparent 
 	  Closure.betaiotazeta (Names.Idpred.full,!predref)
     end
+*)
+
+let update_flags ()=
+  let predref=ref Names.KNpred.empty in
+  let f coe=
+    try
+      let kn=destConst (Classops.get_coercion_value coe) in
+	predref:=Names.KNpred.add kn !predref
+    with Invalid_argument "destConst"-> () in
+    List.iter f (Classops.coercions ());
+    red_flags:=
+    Closure.RedFlags.red_add_transparent 
+      Closure.betaiotazeta 
+      (Names.Idpred.full,Names.KNpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();