GIntuition now matches Intuition up to hyps renaming.

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

5 files changed, 20 insertions, 2 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index e00f26f3d4..42611884ef 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -49,6 +49,10 @@ let op2bool = function Some _->true | None->false
 let id_not=constant "Logic" "not"
 let id_iff=constant "Logic" "iff"
 
+let defined_connectives=lazy
+  [[],EvalConstRef (destConst (id_not ()));
+   [],EvalConstRef (destConst (id_iff ()))]
+
 let match_with_evaluable t=
   match kind_of_term t with
       App (hd,b)-> 
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index d40764e74e..c31eec2b28 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -22,6 +22,8 @@ val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) ->
 
 type ('a,'b) sum = Left of 'a | Right of 'b
 
+val defined_connectives: (int list * evaluable_global_reference) list lazy_t
+
 type kind_of_formula=
    Arrow of constr*constr
   |And of inductive*constr list
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index 914b209f12..054b28a070 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -185,8 +185,10 @@ END
 
 TACTIC EXTEND GIntuition
    ["GIntuition" tactic(t)] ->
-     [ gen_ground_tac false (Some(snd t)) [] ]
+     [ gen_ground_tac false 
+	 (Some(tclTHEN normalize_evaluables (snd t))) [] ]
 |  [ "GIntuition" ] ->
-     [ gen_ground_tac false None [] ] 
+     [ gen_ground_tac false 
+	 (Some (tclTHEN normalize_evaluables default_solver)) [] ] 
 END
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 85abca7218..73b280d0ab 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -69,6 +69,14 @@ let left_evaluable_tac ec id tacrec seq gl=
 	let nid=(Tacmach.pf_nth_hyp_id gls 1) in
 	  unfold_in_hyp [[1],ec] (Tacexpr.InHypType nid) gls);
      wrap 1 false tacrec seq] gl
+
+let normalize_evaluables=
+  onAllClauses
+    (function 
+	 None->unfold_in_concl (Lazy.force defined_connectives)
+       | Some id-> 
+	   unfold_in_hyp (Lazy.force defined_connectives) 
+	   (Tacexpr.InHypType id))
     
 let and_tac tacrec seq=
   tclTHEN simplest_split (wrap 0 true tacrec seq)
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 692443baed..91fdc8cf37 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -27,6 +27,8 @@ val evaluable_tac : evaluable_global_reference -> seqtac
 
 val left_evaluable_tac : evaluable_global_reference -> lseqtac
 
+val normalize_evaluables : tactic
+
 val and_tac : seqtac
 
 val left_and_tac : inductive -> lseqtac