Ground major update ... mmm, sounds exciting !

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

13 files changed, 223 insertions, 226 deletions

diff --git a/.depend b/.depend
index ecae0d18f7..9fa3b063d5 100644
--- a/.depend
+++ b/.depend
@@ -242,7 +242,7 @@ tactics/btermdn.cmi: pretyping/pattern.cmi kernel/term.cmi
 tactics/contradiction.cmi: kernel/names.cmi proofs/proof_type.cmi \
     kernel/term.cmi 
 tactics/dhyp.cmi: kernel/names.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
-    interp/topconstr.cmi 
+    interp/topconstr.cmi toplevel/vernacexpr.cmo 
 tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi \
     pretyping/rawterm.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
     kernel/term.cmi 
@@ -406,10 +406,11 @@ contrib/extraction/table.cmi: kernel/environ.cmi library/libnames.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi 
 contrib/first-order/formula.cmi: library/libnames.cmi kernel/names.cmi \
     proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
+contrib/first-order/ground.cmi: proofs/proof_type.cmi \
+    contrib/first-order/sequent.cmi proofs/tacmach.cmi 
 contrib/first-order/instances.cmi: contrib/first-order/formula.cmi \
     library/libnames.cmi kernel/names.cmi contrib/first-order/rules.cmi \
-    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi \
-    contrib/first-order/unify.cmi 
+    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi 
 contrib/first-order/rules.cmi: library/libnames.cmi kernel/names.cmi \
     contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi 
 contrib/first-order/sequent.cmi: contrib/first-order/formula.cmi lib/heap.cmi \
@@ -2777,43 +2778,51 @@ contrib/field/field.cmx: toplevel/cerrors.cmx interp/constrintern.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx kernel/term.cmx \
     interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx 
-contrib/first-order/formula.cmo: interp/coqlib.cmi kernel/declarations.cmi \
+contrib/first-order/formula.cmo: kernel/declarations.cmi kernel/environ.cmi \
     library/global.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
     library/libnames.cmi kernel/names.cmi pretyping/reductionops.cmi \
     proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi \
     pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
     contrib/first-order/formula.cmi 
-contrib/first-order/formula.cmx: interp/coqlib.cmx kernel/declarations.cmx \
+contrib/first-order/formula.cmx: kernel/declarations.cmx kernel/environ.cmx \
     library/global.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \
     library/libnames.cmx kernel/names.cmx pretyping/reductionops.cmx \
     proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx \
     pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
     contrib/first-order/formula.cmi 
-contrib/first-order/ground.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
-    contrib/first-order/formula.cmi interp/genarg.cmi library/goptions.cmi \
-    contrib/first-order/instances.cmi library/libnames.cmi parsing/pcoq.cmi \
-    lib/pp.cmi parsing/pptactic.cmi proofs/proof_trees.cmi proofs/refiner.cmi \
+contrib/first-order/g_ground.cmo: toplevel/cerrors.cmi interp/coqlib.cmi \
+    parsing/egrammar.cmi contrib/first-order/formula.cmi interp/genarg.cmi \
+    library/goptions.cmi contrib/first-order/ground.cmi kernel/names.cmi \
+    parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/refiner.cmi \
+    contrib/first-order/sequent.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi 
+contrib/first-order/g_ground.cmx: toplevel/cerrors.cmx interp/coqlib.cmx \
+    parsing/egrammar.cmx contrib/first-order/formula.cmx interp/genarg.cmx \
+    library/goptions.cmx contrib/first-order/ground.cmx kernel/names.cmx \
+    parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/refiner.cmx \
+    contrib/first-order/sequent.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx 
+contrib/first-order/ground.cmo: contrib/first-order/formula.cmi lib/heap.cmi \
+    contrib/first-order/instances.cmi lib/pp.cmi proofs/proof_trees.cmi \
     contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \
-    proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \
-    proofs/tactic_debug.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi 
-contrib/first-order/ground.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
-    contrib/first-order/formula.cmx interp/genarg.cmx library/goptions.cmx \
-    contrib/first-order/instances.cmx library/libnames.cmx parsing/pcoq.cmx \
-    lib/pp.cmx parsing/pptactic.cmx proofs/proof_trees.cmx proofs/refiner.cmx \
+    tactics/tacinterp.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    contrib/first-order/ground.cmi 
+contrib/first-order/ground.cmx: contrib/first-order/formula.cmx lib/heap.cmx \
+    contrib/first-order/instances.cmx lib/pp.cmx proofs/proof_trees.cmx \
     contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \
-    proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
-    proofs/tactic_debug.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx 
+    tactics/tacinterp.cmx proofs/tacmach.cmx proofs/tactic_debug.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    contrib/first-order/ground.cmi 
 contrib/first-order/instances.cmo: kernel/declarations.cmi \
-    contrib/first-order/formula.cmi library/libnames.cmi \
+    contrib/first-order/formula.cmi lib/heap.cmi library/libnames.cmi \
     pretyping/rawterm.cmi pretyping/reductionops.cmi \
     contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \
     proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
     kernel/term.cmi pretyping/termops.cmi contrib/first-order/unify.cmi \
     lib/util.cmi contrib/first-order/instances.cmi 
 contrib/first-order/instances.cmx: kernel/declarations.cmx \
-    contrib/first-order/formula.cmx library/libnames.cmx \
+    contrib/first-order/formula.cmx lib/heap.cmx library/libnames.cmx \
     pretyping/rawterm.cmx pretyping/reductionops.cmx \
     contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
@@ -2821,16 +2830,16 @@ contrib/first-order/instances.cmx: kernel/declarations.cmx \
     lib/util.cmx contrib/first-order/instances.cmi 
 contrib/first-order/rules.cmo: interp/coqlib.cmi kernel/declarations.cmi \
     contrib/first-order/formula.cmi library/libnames.cmi kernel/names.cmi \
-    pretyping/reductionops.cmi contrib/first-order/sequent.cmi \
-    kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi contrib/first-order/rules.cmi 
+    contrib/first-order/sequent.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    contrib/first-order/rules.cmi 
 contrib/first-order/rules.cmx: interp/coqlib.cmx kernel/declarations.cmx \
     contrib/first-order/formula.cmx library/libnames.cmx kernel/names.cmx \
-    pretyping/reductionops.cmx contrib/first-order/sequent.cmx \
-    kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx contrib/first-order/rules.cmi 
+    contrib/first-order/sequent.cmx kernel/sign.cmx proofs/tacexpr.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    contrib/first-order/rules.cmi 
 contrib/first-order/sequent.cmo: tactics/auto.cmi interp/constrextern.cmi \
     contrib/first-order/formula.cmi library/global.cmi lib/heap.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi parsing/ppconstr.cmi \
@@ -3483,8 +3492,8 @@ contrib/linear/dpc.cmo: parsing/grammar.cma
 contrib/linear/dpc.cmx: parsing/grammar.cma
 contrib/funind/tacinv.cmo: parsing/grammar.cma
 contrib/funind/tacinv.cmx: parsing/grammar.cma
-contrib/first-order/ground.cmo: parsing/grammar.cma
-contrib/first-order/ground.cmx: parsing/grammar.cma
+contrib/first-order/g_ground.cmo: parsing/grammar.cma
+contrib/first-order/g_ground.cmx: parsing/grammar.cma
 parsing/lexer.cmo: 
 parsing/lexer.cmx: 
 parsing/q_util.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index b2e8d8b668..77b3b80925 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -20,7 +20,7 @@ contrib/cc/cctac.ml: parsing/grammar.cma
 contrib/linear/ccidpc.ml: parsing/grammar.cma
 contrib/linear/dpc.ml: parsing/grammar.cma
 contrib/funind/tacinv.ml: parsing/grammar.cma
-contrib/first-order/ground.ml: parsing/grammar.cma
+contrib/first-order/g_ground.ml: parsing/grammar.cma
 parsing/lexer.ml: 
 parsing/q_util.ml: 
 parsing/q_coqast.ml: 
diff --git a/.depend.newcoq b/.depend.newcoq
index 9cdc3b1da4..8e5bf3ee55 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -1,3 +1,9 @@
+newtheories/FSets/FSet.vo: newtheories/FSets/FSet.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetBridge.vo newtheories/FSets/FSetProperties.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetRBT.vo
+newtheories/FSets/FSetList.vo: newtheories/FSets/FSetList.v newtheories/FSets/FSetInterface.vo
+newtheories/FSets/FSetBridge.vo: newtheories/FSets/FSetBridge.v newtheories/FSets/FSetInterface.vo
+newtheories/FSets/FSetProperties.vo: newtheories/FSets/FSetProperties.v newcontrib/omega/Omega.vo newtheories/FSets/FSetInterface.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Bool/Zerob.vo
+newtheories/FSets/FSetInterface.vo: newtheories/FSets/FSetInterface.v newtheories/Bool/Bool.vo newtheories/Lists/PolyList.vo newtheories/Sorting/Sorting.vo newtheories/Setoids/Setoid.vo
+newtheories/FSets/FSetRBT.vo: newtheories/FSets/FSetRBT.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetBridge.vo newcontrib/omega/Omega.vo newtheories/ZArith/ZArith.vo
 newtheories/Reals/TypeSyntax.vo: newtheories/Reals/TypeSyntax.v
 newtheories/Reals/Rdefinitions.vo: newtheories/Reals/Rdefinitions.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/TypeSyntax.vo
 newtheories/Reals/Rsyntax.vo: newtheories/Reals/Rsyntax.v newtheories/Reals/Rdefinitions.vo
diff --git a/Makefile b/Makefile
index a5ecb3a88c..504a8c28a2 100644
--- a/Makefile
+++ b/Makefile
@@ -279,7 +279,8 @@ FUNINDCMO=\
 FOCMO=\
   contrib/first-order/formula.cmo contrib/first-order/unify.cmo \
   contrib/first-order/sequent.cmo contrib/first-order/rules.cmo \
-  contrib/first-order/instances.cmo contrib/first-order/ground.cmo
+  contrib/first-order/instances.cmo contrib/first-order/ground.cmo \
+  contrib/first-order/g_ground.cmo
 
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
 
@@ -297,7 +298,7 @@ LINEARCMO=\
 
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
   contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4 contrib/funind/tacinv.ml4 \
-  contrib/first-order/ground.ml4
+  contrib/first-order/g_ground.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 3cf0997733..bce1ef24ed 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -63,25 +63,19 @@ let ind_hyps nevar ind largs=
       fst (Sign.decompose_prod_assum t2) in
     Array.init lp myhyps
 
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
-
-let id_not=lazy (destConst (constant "not"))
-let id_iff=lazy (destConst (constant "iff"))
-
 let match_with_evaluable gl t=
   let env=pf_env gl in
+  let hd=       
     match kind_of_term t with
-	App (hd,b)-> 
-	  (match kind_of_term hd with
-	       Const cst->
-		 if (*Environ.evaluable_constant cst env*) 
-		   cst=(Lazy.force id_not) || 
-		   cst=(Lazy.force id_iff) then 
-		   Some(EvalConstRef cst,t)
-		 else None
-	     | _-> None)
+	App (head,_) -> head
+      | _ -> t in
+    match kind_of_term hd with
+	Const cst->
+	  if Environ.evaluable_constant cst env 
+	  then Some (EvalConstRef cst,t)
+	  else None
       | _-> None
-	
+
 type kind_of_formula=
     Arrow of constr*constr
   | False of inductive*constr list
@@ -90,7 +84,6 @@ type kind_of_formula=
   | Exists of inductive*constr list
   | Forall of constr*constr
   | Atom of constr
-  | Evaluable of evaluable_global_reference*constr 
       
 let rec kind_of_formula gl term =
   let cciterm=whd_betaiotazeta term in
@@ -116,8 +109,14 @@ let rec kind_of_formula gl term =
 			Some (i,l)-> Exists((destInd i),l)
 		      |_-> 
 			 match match_with_evaluable gl cciterm with 
-			     Some (ec,t)->Evaluable (ec,t)
-			   | None ->Atom cciterm
+			     Some (ec,t)->	  
+			       let nt=Tacred.unfoldn [[1],ec] 
+					(pf_env gl)
+					(Refiner.sig_sig gl) t in
+				 kind_of_formula gl nt
+			   | None ->Atom (nf_betadeltaiota 
+					    (pf_env gl) 
+					    (Refiner.sig_sig gl) cciterm)
   
 type atoms = {positive:constr list;negative:constr list}
 
@@ -161,10 +160,6 @@ let build_atoms gl metagen polarity cciterm =
 	      positive:= unsigned :: !positive 
 	    else 
 	      negative:= unsigned :: !negative
-      | Evaluable(ec,t)->
-	  let nt=Tacred.unfoldn [[1],ec] (Lazy.force pfenv) 
-		   (Refiner.sig_sig gl) t in
-	    build_rec env polarity nt
   in 
     build_rec [] polarity cciterm;
     (!trivial,
@@ -179,7 +174,6 @@ type right_pattern =
   | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-  | Revaluable of evaluable_global_reference
    
 type left_arrow_pattern=
     LLatom
@@ -189,7 +183,6 @@ type left_arrow_pattern=
   | LLforall of constr
   | LLexists of inductive*constr list
   | LLarrow of constr*constr*constr
-  | LLevaluable of evaluable_global_reference
 
 type left_pattern=
     Lfalse    
@@ -197,7 +190,6 @@ type left_pattern=
   | Lor of inductive 
   | Lforall of metavariable*constr*bool
   | Lexists of inductive
-  | Levaluable of evaluable_global_reference
   | LA of constr*left_arrow_pattern
 
 type t={id:global_reference;
@@ -224,8 +216,7 @@ let build_formula side nam typ gl metagen=
 		let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
 		  Rexists(m,d,trivial)
 	    | Forall (_,a) -> Rforall 
-	    | Arrow (a,b) -> Rarrow 
-	    | Evaluable (egc,_)->Revaluable egc in
+	    | Arrow (a,b) -> Rarrow in
 	  Right pat
       else
 	let pat=
@@ -237,44 +228,22 @@ let build_formula side nam typ gl metagen=
 	    | Exists (ind,_) ->  Lexists ind 
 	    | Forall (d,_) -> 
 		Lforall(m,d,trivial)
-	    | Evaluable (egc,_) ->Levaluable egc 
-	    | Arrow (a,b) ->LA (a, 
-				match kind_of_formula gl a with
-				    False(i,l)-> LLfalse(i,l)
-				  | Atom t->     LLatom
-				  | And(i,l)->      LLand(i,l)
-				  | Or(i,l)->       LLor(i,l)
-				  | Arrow(a,c)-> LLarrow(a,c,b)
-				  | Exists(i,l)->LLexists(i,l)
-				  | Forall(_,_)->LLforall a
-				  | Evaluable (egc,_)-> LLevaluable egc) in
+	    | Arrow (a,b) ->
+		let nfa=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) a in
+		  LA (nfa, 
+		      match kind_of_formula gl a with
+			  False(i,l)-> LLfalse(i,l)
+			| Atom t->     LLatom
+			| And(i,l)->      LLand(i,l)
+			| Or(i,l)->       LLor(i,l)
+			| Arrow(a,c)-> LLarrow(a,c,b)
+			| Exists(i,l)->LLexists(i,l)
+			| Forall(_,_)->LLforall a) in
 	  Left pat
     in
       Left {id=nam;
-	    constr=typ;
+	    constr=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) typ;
 	    pat=pattern;
 	    atoms=atoms}
-  with Is_atom a-> Right a
-(*    
-let build_right_entry typ gl metagen=
-  try
-    let m=meta_succ(metagen false) in 
-    let trivial,atoms=
-      if !qflag then 
-	build_atoms gl metagen true typ
-      else no_atoms in
-    let pattern=
-      match kind_of_formula gl typ with
-	  False(_,_)        -> raise (Is_atom typ)
-	| Atom a       -> raise (Is_atom a)
-	| And(_,_)        -> Rand
-	| Or(_,_)         -> Ror
-	| Exists (i,l) -> 
-	    let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
-	      Rexists(m,d,trivial)
-	| Forall (_,a) -> Rforall 
-	| Arrow (a,b) -> Rarrow 
-	| Evaluable (egc,_)->Revaluable egc in
-      Complex(pattern,typ,atoms)
-  with Is_atom a-> Atomic a
-*)
+  with Is_atom a-> Right a (* already in nf *)
+    
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 815657f543..cbf3dc1522 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -39,7 +39,6 @@ type kind_of_formula =
   | Exists of inductive*constr list
   | Forall of constr*constr
   | Atom of constr
-  | Evaluable of Names.evaluable_global_reference * Term.constr
 
 val kind_of_formula : Proof_type.goal Tacmach.sigma -> 
   constr -> kind_of_formula
@@ -58,7 +57,6 @@ type right_pattern =
   | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-  | Revaluable of Names.evaluable_global_reference
     
 type left_arrow_pattern=
     LLatom
@@ -68,7 +66,6 @@ type left_arrow_pattern=
   | LLforall of constr
   | LLexists of inductive*constr list
   | LLarrow of constr*constr*constr
-  | LLevaluable of Names.evaluable_global_reference
 
 type left_pattern=
     Lfalse    
@@ -76,7 +73,6 @@ type left_pattern=
   | Lor of inductive 
   | Lforall of metavariable*constr*bool
   | Lexists of inductive
-  | Levaluable of Names.evaluable_global_reference
   | LA of constr*left_arrow_pattern
       
 type t={id: global_reference;
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
new file mode 100644
index 0000000000..059ca69a6a
--- /dev/null
+++ b/contrib/first-order/g_ground.ml4
@@ -0,0 +1,96 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma"  i*)
+
+(* $Id$ *)
+
+open Formula
+open Sequent
+open Ground
+open Goptions
+open Tactics
+open Tacticals
+open Term
+open Names
+
+(* declaring search depth as a global option *)
+
+let ground_depth=ref 5
+
+let _=
+  let gdopt=
+    { optsync=false;
+      optname="ground_depth";
+      optkey=SecondaryTable("Ground","Depth"); 
+      optread=(fun ()->Some !ground_depth); 
+      optwrite=
+   (function 
+	None->ground_depth:=5
+      |	Some i->ground_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+      
+let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
+    
+let fail_solver=tclFAIL 0 "GTauto failed"
+		      
+let gen_ground_tac flag taco l gl=
+  let backup= !qflag in
+    try
+      qflag:=flag;
+      let solver= 
+	match taco with 
+	    Some tac->tac
+	  | None-> default_solver in
+      let startseq=create_with_ref_list l !ground_depth in
+      let result=ground_tac solver startseq gl in 
+	qflag:=backup;result
+    with e ->qflag:=backup;raise e
+
+(* special for compatibility with old Intuition *)
+
+let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+
+let defined_connectives=lazy
+  [[],EvalConstRef (destConst (constant "not"));
+   [],EvalConstRef (destConst (constant "iff"))]
+
+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))
+
+TACTIC EXTEND Ground
+      |   [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> 
+	    [ gen_ground_tac true (Some (snd t)) l ]
+      |   [ "Ground" tactic(t) ] -> 
+	    [ gen_ground_tac true (Some (snd t)) [] ]
+      |   [ "Ground" "with" ne_reference_list(l) ] -> 
+	    [ gen_ground_tac true None l ]
+      |   [ "Ground" ] ->
+	    [ gen_ground_tac true None [] ]
+END
+
+TACTIC EXTEND GTauto   
+  [ "GTauto" ] ->
+     [ gen_ground_tac false (Some fail_solver) [] ]   
+END
+
+TACTIC EXTEND GIntuition
+   ["GIntuition" tactic(t)] ->
+     [ gen_ground_tac false 
+	 (Some(tclTHEN normalize_evaluables (snd t))) [] ]
+|  [ "GIntuition" ] ->
+     [ gen_ground_tac false 
+	 (Some (tclTHEN normalize_evaluables default_solver)) [] ] 
+END
+
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml
index 69f70d590f..cc63b4afca 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma"  i*)
-
 (* $Id$ *)
 
 open Formula
@@ -18,40 +16,18 @@ open Term
 open Tacmach
 open Tactics
 open Tacticals
-open Libnames
-open Util
-open Goptions
-
-(* declaring search depth as a global option *)
-
-let ground_depth=ref 5
-
-let set_qflag b= qflag:=b
-		   
-let _=
-  let gdopt=
-    { optsync=false;
-      optname="ground_depth";
-      optkey=SecondaryTable("Ground","Depth"); 
-      optread=(fun ()->Some !ground_depth); 
-      optwrite=
-   (function 
-	None->ground_depth:=5
-      |	Some i->ground_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
       
 let ground_tac solver startseq gl=
-  let rec toptac ctx seq gl=
+  let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
     then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try      
 	  let (hd,seq1)=take_formula seq  
-	  and re_add s=re_add_formula_list ctx s in
+	  and re_add s=re_add_formula_list skipped s in
 	  let continue=toptac [] 
-	  and backtrack=toptac (hd::ctx) seq1  in
+	  and backtrack=toptac (hd::skipped) seq1  in
 	    match hd.pat with
 		Right rpat->
 		  begin
@@ -62,8 +38,6 @@ let ground_tac solver startseq gl=
 			  forall_tac continue (re_add seq1)
 		      | Rarrow->
 			  arrow_tac continue (re_add seq1)
-		      | Revaluable egr->
-			  evaluable_tac egr continue (re_add seq1)
 		      | Ror->
 			  tclORELSE
 			  (or_tac continue (re_add seq1))
@@ -71,7 +45,7 @@ let ground_tac solver startseq gl=
 		      | Rfalse->backtrack 
 		      | Rexists(i,dom,triv)->
 			  let (lfp,seq2)=collect_quantified seq in
-			  let backtrack2=toptac (lfp@ctx) seq2 in
+			  let backtrack2=toptac (lfp@skipped) seq2 in
 			    tclORELSE
 			      (if seq.depth<=0 || not !qflag then 
 				 tclFAIL 0 "max depth" 
@@ -90,7 +64,7 @@ let ground_tac solver startseq gl=
 			  left_or_tac ind hd.id continue (re_add seq1)
 		      | Lforall (_,_,_)->
 			  let (lfp,seq2)=collect_quantified seq in
-			  let backtrack2=toptac (lfp@ctx) seq2 in
+			  let backtrack2=toptac (lfp@skipped) seq2 in
 			    tclORELSE
 			      (if seq.depth<=0 || not !qflag then 
 				 tclFAIL 0 "max depth" 
@@ -101,8 +75,6 @@ let ground_tac solver startseq gl=
 			  if !qflag then
 			    left_exists_tac ind hd.id continue (re_add seq1)
 			  else backtrack
-		      | Levaluable egr->
-			  left_evaluable_tac egr hd.id continue (re_add seq1)
 		      | LA (typ,lap)->
 			  tclORELSE
 			  (ll_atom_tac typ hd.id continue (re_add seq1))
@@ -132,54 +104,8 @@ let ground_tac solver startseq gl=
 				  (ll_arrow_tac a b c hd.id continue 
 				     (re_add seq1))
 				  backtrack
-			      | LLevaluable egr->
-				  left_evaluable_tac egr hd.id continue 
-				  (re_add seq1)
 			  end
 		  end
 	    with Heap.EmptyHeap->solver
       end gl in
     wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
-      
-let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
-    
-let fail_solver=tclFAIL 0 "GroundTauto failed"
-		      
-let gen_ground_tac flag taco l gl=
-  let backup= !qflag in
-    try
-      set_qflag flag;
-      let solver= 
-	match taco with 
-	    Some tac->tac
-	  | None-> default_solver in
-      let startseq=create_with_ref_list l !ground_depth in
-      let result=ground_tac solver startseq gl in 
-	set_qflag backup;result
-    with e -> set_qflag backup;raise e
-	   
-TACTIC EXTEND Ground
-      |   [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> 
-	    [ gen_ground_tac true (Some (snd t)) l ]
-      |   [ "Ground" tactic(t) ] -> 
-	    [ gen_ground_tac true (Some (snd t)) [] ]
-      |   [ "Ground" "with" ne_reference_list(l) ] -> 
-	    [ gen_ground_tac true None l ]
-      |   [ "Ground" ] ->
-	    [ gen_ground_tac true None [] ]
-END
-
-TACTIC EXTEND GTauto   
-  [ "GTauto" ] ->
-     [ gen_ground_tac false (Some fail_solver) [] ]   
-END
-
-TACTIC EXTEND GIntuition
-   ["GIntuition" tactic(t)] ->
-     [ gen_ground_tac false 
-	 (Some(tclTHEN normalize_evaluables (snd t))) [] ]
-|  [ "GIntuition" ] ->
-     [ gen_ground_tac false 
-	 (Some (tclTHEN normalize_evaluables default_solver)) [] ] 
-END
-
diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli
new file mode 100644
index 0000000000..fff45816a8
--- /dev/null
+++ b/contrib/first-order/ground.mli
@@ -0,0 +1,13 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+val ground_tac:     Tacmach.tactic ->
+  (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 41a4078cc3..e75ee8fb8b 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -115,41 +115,47 @@ let left_instance_tac (inst,id) tacrec seq=
 	else
 	  tclTHENS (cut dom) 
 	    [tclTHENLIST
-	       [intro;
+	       [introf;
 		(fun gls->generalize 
 		   [mkApp(constr_of_reference id,
 			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		intro;
+		introf;
 		tclSOLVE [wrap 1 false tacrec 
 			    (deepen (record (id,None) seq))]];
 	    tclTRY assumption]
-    | Real((m,t) as c,_)->
-	if lookup (id,Some c) seq || m>0 then 
+    | Real((0,t) as c,_)->
+	if lookup (id,Some c) seq then 
 	  tclFAIL 0 "already done" 
 	else
 	  tclTHENLIST 
 	    [generalize [mkApp(constr_of_reference id,[|t|])];
-	     intro; 
+	     introf; 
 	     tclSOLVE 
 	       [wrap 1 false tacrec 
 		  (deepen (record (id,Some c) seq))]]
+    | Real((m,t) as c,_)->
+	if lookup (id,Some c) seq then 
+	  tclFAIL 0 "already done" 
+	else 
+	  tclFAIL 0 "not implemented ... yet"
+
 
 let right_instance_tac inst tacrec seq=
   match inst with
       Phantom dom ->
 	tclTHENS (cut dom) 
 	[tclTHENLIST
-	   [intro;
+	   [introf;
 	    (fun gls->
 	       split (Rawterm.ImplicitBindings 
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
 	 tclTRY assumption] 
+    | Real ((0,t),_) ->
+	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	   (tclSOLVE [wrap 0 true tacrec (deepen seq)]))
     | Real ((m,t),_) ->
-	if m>0 then tclFAIL 0 "not implemented ... yes"
-	else
-	  tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	    (tclSOLVE [wrap 0 true tacrec (deepen seq)])
+	tclFAIL 0 "not implemented ... yet"
 
 let instance_tac inst=
   if (snd inst)==dummy_id then 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index e7b71f54fd..3ee0871dea 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -15,7 +15,6 @@ open Tacmach
 open Tactics
 open Tacticals
 open Termops
-open Reductionops
 open Declarations
 open Formula
 open Sequent
@@ -65,27 +64,10 @@ let ll_atom_tac a id tacrec seq=
       [generalize [mkApp(constr_of_reference id,
 			 [|constr_of_reference (find_left a seq)|])];
        clear_global id;
-       intro;
+       introf;
        wrap 1 false tacrec seq] 
   with Not_found->tclFAIL 0 "No link" 
 
-(* evaluation rules *)
-
-let evaluable_tac ec tacrec seq gl=
-  tclTHEN
-    (unfold_in_concl [[1],ec]) 
-    (wrap 0 true tacrec seq) gl
-
-let left_evaluable_tac ec id tacrec seq gl=
-  tclTHENLIST
-    [generalize [constr_of_reference id];
-     clear_global id;
-     intro;
-     (fun gls->
-	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
-
 (* right connectives rules *)
 
 let and_tac tacrec seq=
@@ -95,7 +77,7 @@ let or_tac tacrec seq=
   any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq]))
 
 let arrow_tac tacrec seq=
-  tclTHEN intro (wrap 1 true tacrec seq)
+  tclTHEN introf (wrap 1 true tacrec seq)
    
 (* left connectives rules *)
 
@@ -104,7 +86,7 @@ let left_and_tac ind id tacrec seq=
     tclTHENLIST 
       [simplest_elim (constr_of_reference id);
        clear_global id; 
-       tclDO n intro;
+       tclDO n introf;
        wrap n false tacrec seq]
 
 let left_or_tac ind id tacrec seq=
@@ -112,7 +94,7 @@ let left_or_tac ind id tacrec seq=
   let f n=
     tclTHENLIST
       [clear_global id;
-       tclDO n intro;
+       tclDO n introf;
        wrap n false tacrec seq] in
     tclTHENSV
       (simplest_elim (constr_of_reference id))
@@ -143,7 +125,7 @@ let ll_ind_tac ind largs id tacrec seq gl=
 	 tclTHENLIST 
 	   [generalize newhyps;
 	    clear_global id;
-	    tclDO lp intro;
+	    tclDO lp introf;
 	    wrap lp false tacrec seq]
    with Invalid_argument _ ->tclFAIL 0 "") gl
 
@@ -154,40 +136,40 @@ let ll_arrow_tac a b c id tacrec seq=
 			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclTHENS (cut c)
       [tclTHENLIST
-	 [intro;
+	 [introf;
 	  clear_global id;
 	  wrap 1 false tacrec seq];
        tclTHENS (cut cc) 
          [exact_no_check (constr_of_reference id); 
 	  tclTHENLIST 
 	    [generalize [d];
-	     intro;
+	     introf;
 	     clear_global id;
 	     tclSOLVE [wrap 1 true tacrec seq]]]]
 
 (* quantifier rules (easy side) *)
 
 let forall_tac tacrec seq=
-  tclTHEN intro (wrap 0 true tacrec seq)
+  tclTHEN introf (wrap 0 true tacrec seq)
 
 let left_exists_tac ind id tacrec seq=
   let n=(construct_nhyps ind).(0) in  
     tclTHENLIST
       [simplest_elim (constr_of_reference id);
        clear_global id;
-       tclDO n intro;
+       tclDO n introf;
        (wrap (n-1) false tacrec seq)]
 
 let ll_forall_tac prod id tacrec seq=
   tclTHENS (cut prod)
     [tclTHENLIST
-       [intro;
+       [introf;
 	(fun gls->
 	   let id0=pf_nth_hyp_id gls 1 in
 	   let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
 	     tclTHEN (generalize [term]) (clear [id0]) gls);  
 	clear_global id;
-	intro;
+	introf;
 	tclSOLVE [wrap 1 false tacrec (deepen seq)]];
      tclSOLVE [wrap 0 true tacrec (deepen seq)]]
 
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 10ffe863d2..afccfcd1bb 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -27,10 +27,6 @@ val axiom_tac : constr -> Sequent.t -> tactic
 
 val ll_atom_tac : constr -> lseqtac
 
-val evaluable_tac : evaluable_global_reference -> seqtac
-
-val left_evaluable_tac : evaluable_global_reference -> lseqtac
-
 val and_tac : seqtac
 
 val or_tac : seqtac
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4942503c6a..4c18090b93 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -31,7 +31,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 	    | Ror ->             -15
 	    | Rfalse ->          -50 (* dead end for sure *)
 	    | Rforall ->         100
-	    | Revaluable _ ->    100 
 	    | Rexists (_,_,_) -> -30
 	end
     | Left lf ->
@@ -41,7 +40,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 	  | Lor _              ->    40
 	  | Lforall (_,_,_)      -> -30 (* must stay at lowest priority *)
 	  | Lexists _           ->   60
-	  | Levaluable _       ->   100
 	  | LA(_,lap) ->
 	      match lap with
 		  LLatom             ->   0
@@ -51,7 +49,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 		| LLforall _         -> -20
 		| LLexists (_,_)     ->  50
 		| LLarrow  (_,_,_)   -> -10 
-		| LLevaluable _      -> 100
 
 let left_reversible lpat=(priority lpat)>0