ground->firstorder, cc-> congruence, CC final commit

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

13 files changed, 174 insertions, 108 deletions

diff --git a/.depend b/.depend
index f03b912e44..aa810984c2 100644
--- a/.depend
+++ b/.depend
@@ -2316,26 +2316,28 @@ contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi lib/util.cmi \
     contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx lib/util.cmx \
     contrib/cc/ccalgo.cmi 
-contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi lib/util.cmi \
-    contrib/cc/ccproof.cmi 
-contrib/cc/ccproof.cmx: contrib/cc/ccalgo.cmx kernel/names.cmx lib/util.cmx \
-    contrib/cc/ccproof.cmi 
+contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi lib/pp.cmi \
+    lib/util.cmi contrib/cc/ccproof.cmi 
+contrib/cc/ccproof.cmx: contrib/cc/ccalgo.cmx kernel/names.cmx lib/pp.cmx \
+    lib/util.cmx contrib/cc/ccproof.cmi 
 contrib/cc/cctac.cmo: contrib/cc/ccalgo.cmi contrib/cc/ccproof.cmi \
     toplevel/cerrors.cmi interp/coqlib.cmi kernel/declarations.cmi \
-    parsing/egrammar.cmi pretyping/evd.cmi library/global.cmi \
-    pretyping/inductiveops.cmi library/libnames.cmi library/library.cmi \
-    library/nameops.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
-    lib/pp.cmi parsing/pptactic.cmi proofs/proof_type.cmi proofs/refiner.cmi \
-    kernel/sign.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+    parsing/egrammar.cmi tactics/equality.cmi pretyping/evd.cmi \
+    library/global.cmi pretyping/inductiveops.cmi library/libnames.cmi \
+    library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/proof_type.cmi \
+    proofs/refiner.cmi kernel/sign.cmi tactics/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi 
 contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     toplevel/cerrors.cmx interp/coqlib.cmx kernel/declarations.cmx \
-    parsing/egrammar.cmx pretyping/evd.cmx library/global.cmx \
-    pretyping/inductiveops.cmx library/libnames.cmx library/library.cmx \
-    library/nameops.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
-    lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
-    kernel/sign.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+    parsing/egrammar.cmx tactics/equality.cmx pretyping/evd.cmx \
+    library/global.cmx pretyping/inductiveops.cmx library/libnames.cmx \
+    library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx \
+    proofs/refiner.cmx kernel/sign.cmx tactics/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx 
 contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
diff --git a/.depend.newcoq b/.depend.newcoq
index eec84030f6..edb72a828d 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -290,4 +290,4 @@ newcontrib/correctness/Sorted.vo: newcontrib/correctness/Sorted.v newcontrib/cor
 newcontrib/correctness/Tuples.vo: newcontrib/correctness/Tuples.v
 newcontrib/fourier/Fourier_util.vo: newcontrib/fourier/Fourier_util.v newtheories/Reals/Rbase.vo
 newcontrib/fourier/Fourier.vo: newcontrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo newcontrib/fourier/Fourier_util.vo newcontrib/field/Field.vo newtheories/Reals/DiscrR.vo
-newcontrib/cc/CC.vo: newcontrib/cc/CC.v newtheories/Logic/Eqdep_dec.vo
+newcontrib/cc/CC.vo: newcontrib/cc/CC.v
diff --git a/Makefile b/Makefile
index 9e0cc51fd7..8eb8a56533 100644
--- a/Makefile
+++ b/Makefile
@@ -762,7 +762,7 @@ FUNINDVO=
 JPROVERVO= 
 
 CCVO=\
- contrib/cc/CC.vo
+ contrib/cc/CCSolve.vo
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(CORRECTNESSVO) $(FOURIERVO) \
diff --git a/contrib/cc/CC.v b/contrib/cc/CCSolve.v
index ff850ea574..30622aeaa8 100644
--- a/contrib/cc/CC.v
+++ b/contrib/cc/CCSolve.v
@@ -8,15 +8,13 @@
 
 (* $Id$ *)
 
-(* Here were some deprecated lemmata *)
-
 Tactic Definition CCsolve :=
  Repeat (Match Context With
  [ H: ?1 |- ?2] -> 
   Let Heq = FreshId "Heq" In
- (Assert Heq:(?2==?1);[CC|(Rewrite Heq;Exact H)])
+ (Assert Heq:(?2==?1);[Congruence|(Rewrite Heq;Exact H)])
  |[ H: ?1; G: ?2 -> ?3 |- ?] ->                        
   Let Heq = FreshId "Heq" In
- (Assert Heq:(?2==?1) ;[CC|                              
+ (Assert Heq:(?2==?1) ;[Congruence|                              
      (Rewrite Heq in G;Generalize (G H);Clear G;Intro G)])).  
 
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index d7f056dcc5..5f83e3f790 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -86,12 +86,13 @@ end
     
 module UF = struct
 
-module PacSet=Set.Make(struct type t=int*int let compare=compare end) 
+module IndMap=Map.Make(struct type t=inductive let compare=compare end) 
 
   type representative=
       {mutable nfathers:int;
        mutable fathers:int list;
-       mutable constructors:pa_constructor PacMap.t}
+       mutable constructors:pa_constructor PacMap.t;
+       mutable inductives:(int * int) IndMap.t}
 
   type cl = Rep of representative| Eqto of int*equality
 
@@ -124,6 +125,12 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
 	  Rep r ->r
 	| _ -> anomaly "get_representative: not a representative"
 
+  let get_constructor uf i=
+    match (Hashtbl.find uf.map i).term with
+	Constructor (cstr,_,_)->cstr
+      | _ -> anomaly "get_constructor: not a constructor"
+
+
   let fathers uf i=
     (get_representative uf i).fathers
 	  
@@ -149,6 +156,8 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
   let mem_node_pac uf i sg= 
     PacMap.find sg (Hashtbl.find uf.map i).node_constr
   
+  exception Discriminable of int * int * int * int * t 
+
   let add_pacs uf i pacs =
     let rep=get_representative uf i in
     let pending=ref [] and combine=ref [] in 
@@ -161,17 +170,26 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
 	    let rec f n lk ll q=
 	      if n > 0 then match (lk,ll) with
 		  k::qk,l::ql->
-		    let qq=
-		      {lhs=k;rhs=l;rule=Injection(tk,tl,pac.head_constr,n)}::q 
-		    in
-		      f (n-1) qk ql qq 
-		| _->anomaly 
+		    let eq=
+		      {lhs=k;rhs=l;rule=Injection(tk,tl,pac.head_constr,n)} 
+		    in f (n-1) qk ql (eq::q) 
+		| _-> anomaly 
 		    "add_pacs : weird error in injection subterms merge"
 	      else q in
  	      combine:=f pac.nhyps pac.args opac.args !combine
-      with Not_found ->
+      with Not_found -> (* Still Unknown Constructor *)
 	rep.constructors <- PacMap.add sg pac rep.constructors;
-	pending:=(fathers uf (find uf pac.term_head))@rep.fathers@ !pending in
+	pending:=
+	    (fathers uf (find uf pac.term_head)) @rep.fathers@ !pending;
+	let (c,a)=sg in
+	  if a=0 then
+	    let (ind,_)=get_constructor uf c in  
+	      try
+		let th2,hc2=IndMap.find ind rep.inductives in
+		  raise (Discriminable (pac.term_head,c,th2,hc2,uf)) 
+	      with Not_found ->
+		rep.inductives<-
+		IndMap.add ind (pac.term_head,c) rep.inductives in
       PacMap.iter add_pac pacs;
       !pending,!combine
 	
@@ -195,7 +213,11 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
   let next uf=
     let n=uf.size in uf.size<-n+1; n
 	
-  let new_representative l={nfathers=0;fathers=[];constructors=l}
+  let new_representative pm im=
+    {nfathers=0;
+     fathers=[];
+     constructors=pm;
+     inductives=im}
 
   let rec add uf t= 
     try Hashtbl.find uf.syms t with 
@@ -204,20 +226,25 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
 	  let new_node=
 	    match t with
 		Symb s -> 
-		  {clas=Rep (new_representative PacMap.empty);
+		  {clas=Rep (new_representative PacMap.empty IndMap.empty);
 		   vertex=Leaf;term=t;node_constr=PacMap.empty}
 	      | Appli (t1,t2) -> 
 		  let i1=add uf t1 and i2=add uf t2 in
 		    add_father uf (find uf i1) b;
 		    add_father uf (find uf i2) b;
-		    {clas=Rep (new_representative PacMap.empty);
+		    {clas=Rep (new_representative PacMap.empty IndMap.empty);
 		     vertex=Node(i1,i2);term=t;node_constr=PacMap.empty}
 	      | Constructor (c,a,n) ->
 		  let pacs=
 		    PacMap.add (b,a) 
 		      {head_constr=b;arity=a;nhyps=n;args=[];term_head=b} 
 		      PacMap.empty in
-		    {clas=Rep (new_representative pacs);
+		  let inds=
+		    if a=0 then
+		      let (ind,_)=c in
+			IndMap.add ind (b,b) IndMap.empty 
+		    else IndMap.empty in
+		    {clas=Rep (new_representative pacs inds);
 		     vertex=Leaf;term=t;node_constr=PacMap.empty}
 	  in
 	    Hashtbl.add uf.map b new_node;
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 941adab17b..0343c96211 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -41,11 +41,14 @@ end
 module UF :
 sig
   type t 
+  exception Discriminable of int * int * int * int * t 
   val empty : unit -> t
   val find : t -> int -> int
   val size : t -> int -> int
   val pac_arity : t -> int -> int * int -> int
   val mem_node_pac : t -> int -> int * int -> int 
+  val add_pacs : t -> int -> pa_constructor PacMap.t -> 
+    int list * equality list
   val term : t -> int -> term    
   val subterms : t -> int -> int * int
   val add : t -> term -> int
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 95752c122c..9bcdf56f21 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -48,9 +48,11 @@ let pcongr=function
     Refl t1, Refl t2 ->Refl (Appli (t1,t2))
   | p1, p2 -> Congr (p1,p2)
 
-let pid (s:string) (p:proof)=p
-	
-let build_proof uf i j=
+type ('a,'b) mission=
+    Prove of 'a
+  | Refute of 'b
+
+let build_proof uf=
   
   let rec equal_proof i j=
     if i=j then Refl (UF.term uf i) else 
@@ -66,35 +68,41 @@ let build_proof uf i j=
 	| Congruence ->congr_proof eq.lhs eq.rhs
 	| Injection (ti,tj,c,a) ->
 	    let p=equal_proof ti tj in
-	    let arity=UF.pac_arity uf (UF.find uf ti) (c,0) in
-	    let p1=constr_proof ti ti c 0 arity
-	    and p2=constr_proof tj tj c 0 arity  in
+	    let p1=constr_proof ti ti c 0
+	    and p2=constr_proof tj tj c 0 in
 	      match UF.term uf c with
 		  Constructor (cstr,nargs,nhyps) -> 
 		    Inject(ptrans(psym p1,ptrans(p,p2)),cstr,nhyps,a)
 		| _ -> anomaly "injection on non-constructor terms" 
     in  ptrans(ptrans (pi,pij),pj)
 
-  and constr_proof i j c n a=
-       if n<a then 
-	 let nj=UF.mem_node_pac uf j (c,n) in
-	 let (ni,arg)=UF.subterms uf j in 
-	 let p=constr_proof ni nj c (n+1) a in
-	 let targ=UF.term uf arg in 
-	   ptrans (equal_proof i j, pcongr (p,Refl targ))
-       else equal_proof i j
+  and constr_proof i j c n=
+    try
+      let nj=UF.mem_node_pac uf j (c,n) in
+      let (ni,arg)=UF.subterms uf j in 
+      let p=constr_proof ni nj c (n+1) in
+      let targ=UF.term uf arg in 
+	ptrans (equal_proof i j, pcongr (p,Refl targ))
+    with Not_found->equal_proof i j
 
   and path_proof i=function
       [] -> Refl (UF.term uf i)
-    | x::q->ptrans (path_proof j q,edge_proof x)
+    | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x)
   
   and congr_proof i j=
     let (i1,i2) = UF.subterms uf i
     and (j1,j2) = UF.subterms uf j in   
       pcongr (equal_proof i1 j1, equal_proof i2 j2)
-  
+	
+  and discr_proof i ci j cj=
+    let p=equal_proof i j 
+    and p1=constr_proof i i ci 0 
+    and p2=constr_proof j j cj 0 in
+      ptrans(psym p1,ptrans(p,p2))
   in
-    equal_proof i j
+    function
+	Prove(i,j)-> equal_proof i j
+      | Refute(i,ci,j,cj)-> discr_proof i ci j cj
 
 let rec nth_arg t n=
   match t with 
@@ -121,21 +129,27 @@ let rec type_proof axioms p=
 	let (ti,tj)=type_proof axioms p in
 	  nth_arg ti (n-a),nth_arg tj (n-a)
 
-exception Wrong_proof of proof
-
-let cc_proof (axioms,(v,w))=
-  let uf=make_uf axioms in
-  let i1=UF.add uf v in
-  let i2=UF.add uf w in
-  cc uf;
-  if UF.find uf i1=UF.find uf i2 then 
-    let prf=build_proof uf i1 i2 in
-      if (v,w)=type_proof axioms prf then Some (prf,uf,axioms) 
-      else anomaly "Oops !! Wrong equality proof generated"
-  else
-    None
-
-    
-
+let cc_proof (axioms,m)=
+  try
+    let uf=make_uf axioms in
+      match m with 
+	  Some (v,w) ->
+	    let i1=UF.add uf v in
+	    let i2=UF.add uf w in
+	      cc uf;
+	      if UF.find uf i1=UF.find uf i2 then 
+		let prf=build_proof uf (Prove(i1,i2)) in
+		  if (v,w)=type_proof axioms prf then
+		    Prove (prf,axioms)
+		  else anomaly "wrong proof generated"
+	      else
+		errorlabstrm  "CC" (Pp.str "CC couldn't solve goal")
+	| None ->
+	    cc uf;
+	    errorlabstrm  "CC" (Pp.str "CC couldn't solve goal")
+    with UF.Discriminable (i,ci,j,cj,uf) ->
+      let prf=build_proof uf (Refute(i,ci,j,cj)) in 
+      let (t1,t2)=type_proof axioms prf in 
+	Refute (t1,t2,prf,axioms) 
 
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index 99ed30d991..664ac31f81 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -23,16 +23,17 @@ val ptrans : proof * proof -> proof
 val psym : proof -> proof
 val pcongr : proof * proof -> proof
 
-val pid : string -> proof -> proof
+type ('a,'b) mission=
+    Prove of 'a
+  | Refute of 'b
 
-val build_proof : UF.t -> int -> int -> proof
-
-exception Wrong_proof of proof
+val build_proof : UF.t -> (int * int, int * int * int * int) mission -> proof
 
 val type_proof :
   (Names.identifier * (term * term)) list -> proof -> term * term
 
 val cc_proof :
-  (Names.identifier * (term * term)) list * (term * term) ->
-  (proof * UF.t * (Names.identifier * (term * term)) list) option
+  (Names.identifier * (term * term)) list * (term * term) option ->
+  (proof * (Names.identifier * (term * term)) list, 
+   term * term * proof * (Names.identifier * (term * term)) list ) mission
 
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 2bc225b662..2089d59974 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -37,8 +37,6 @@ let fail()=raise Not_an_eq
 let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
 let f_equal_theo = constant ["Init";"Logic"] "f_equal"
-let congr_theo = constant ["cc";"CC"] "Congr_nodep"
-let congr_dep_theo = constant ["cc";"CC"] "Congr_dep"
 
 (* decompose member of equality in an applicative format *)
 
@@ -96,7 +94,10 @@ let rec read_hyps env=function
 	
 let make_prb gl=
   let env=pf_env gl in
-  (read_hyps env gl.it.evar_hyps,read_eq env gl.it.evar_concl)
+  let hyps=read_hyps env gl.it.evar_hyps in
+    try (hyps,Some (read_eq env gl.it.evar_concl)) with 
+	Not_an_eq -> (hyps,None)
+
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
@@ -126,13 +127,13 @@ let build_projection (cstr:constructor) nargs argind ttype default atype gls=
 
 (* generate an adhoc tactic following the proof tree  *)
 
-let rec proof_tac uf axioms=function
+let rec proof_tac axioms=function
     Ax id->exact_check (mkVar id)
   | SymAx id->tclTHEN symmetry (exact_check (mkVar id))
   | Refl t->reflexivity
   | Trans (p1,p2)->let t=(make_term (snd (type_proof axioms p1))) in
       (tclTHENS (transitivity t) 
-	 [(proof_tac uf axioms p1);(proof_tac uf axioms p2)])
+	 [(proof_tac axioms p1);(proof_tac axioms p2)])
   | Congr (p1,p2)->
       fun gls->
 	let (f1,f2)=(type_proof axioms p1) 
@@ -148,9 +149,9 @@ let rec proof_tac uf axioms=function
 	and lemma2=
 	  mkApp(Lazy.force f_equal_theo,[|typx;typfx;tf2;tx1;tx2|]) in
 	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
-	     [tclTHEN (apply lemma1) (proof_tac uf axioms p1);
+	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
   	      tclFIRST
-		[tclTHEN (apply lemma2) (proof_tac uf axioms p2);
+		[tclTHEN (apply lemma2) (proof_tac axioms p2);
 		 reflexivity;
 		 fun gls ->
 		   errorlabstrm  "CC" 
@@ -169,7 +170,7 @@ let rec proof_tac uf axioms=function
 	 let proj=build_projection cstr nargs argind ttype cai atype gls in
 	 let injt=
 	   mkApp (Lazy.force f_equal_theo,[|ttype;atype;proj;cti;ctj|]) in   
-	   tclTHEN (apply injt) (proof_tac uf axioms prf) gls)
+	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
 
 (* wrap everything *)
 	
@@ -180,13 +181,20 @@ let cc_tactic gls=
 	Not_an_eq ->
 	  errorlabstrm  "CC" (str "Goal is not an equality") in
     match (cc_proof prb) with
-	None->errorlabstrm  "CC" (str "CC couldn't solve goal") 
-      | Some (p,uf,axioms)->proof_tac uf axioms p gls
-	
+        Prove (p,axioms)-> proof_tac axioms p gls
+      | Refute (t1,t2,p,axioms) ->
+	  let tt1=make_term t1 and tt2=make_term t2 in
+	  let typ=pf_type_of gls tt1 in
+	  let id=pf_get_new_id (id_of_string "Heq") gls in     
+	  let neweq=
+	    mkApp(constr_of_reference Coqlib.glob_eq,[|typ;tt1;tt2|]) in
+	    tclTHENS (true_cut (Some id) neweq)
+	      [proof_tac axioms p;Equality.discr id] gls
+
 (* Tactic registration *)
       
 TACTIC EXTEND CC
- [ "CC" ] -> [ cc_tactic ]
+ [ "Congruence" ] -> [ cc_tactic ]
 END
 
 
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 33e4107f65..d6f76a0a94 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -29,8 +29,8 @@ let ground_depth=ref 5
 let _=
   let gdopt=
     { optsync=true;
-      optname="Ground Depth";
-      optkey=SecondaryTable("Ground","Depth"); 
+      optname="Firstorder Depth";
+      optkey=SecondaryTable("Firstorder","Depth"); 
       optread=(fun ()->Some !ground_depth); 
       optwrite=
    (function 
@@ -65,7 +65,7 @@ let gen_ground_tac flag taco ext gl=
 	qflag:=backup;result
     with e ->qflag:=backup;raise e
       
-(* special for compatibility with old Intuition 
+(* special for compatibility with Intuition 
 
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
@@ -81,12 +81,12 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives) 
 	   (Tacexpr.InHypType id)) *)
 
-TACTIC EXTEND Ground
-    [ "Ground" tactic_opt(t) "with" ne_reference_list(l) ] -> 
+TACTIC EXTEND Firstorder
+    [ "Firstorder" 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) ] -> 
+|   [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> 
       [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
-|   [ "Ground" tactic_opt(t) ] -> 
+|   [ "Firstorder" tactic_opt(t) ] -> 
       [ gen_ground_tac true (option_app eval_tactic t) Void ]
 END
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index c30c109c27..8f11089bf5 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -279,7 +279,8 @@ let create_with_auto_hints l depth gl=
     let hdb=
       try
 	Util.Stringmap.find dbname !searchtable 
-      with Not_found-> error ("Ground: "^dbname^" : No such Hint database") in
+      with Not_found-> 
+	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
     List.iter h l;
     !seqref
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index 4c0287dc36..4d898da97d 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -2,14 +2,14 @@
 Theorem t1: (A:Set)(a:A)(f:A->A)
 	(f a)=a->(f (f a))=a.
 Intros.
-CC.
+Congruence.
 Save.
 
 Theorem t2: (A:Set)(a,b:A)(f:A->A)(g:A->A->A)
 	a=(f a)->(g b (f a))=(f (f a))->(g a b)=(f (g b a))->
 	(g a b)=a.
 Intros.
-CC.
+Congruence.
 Save.
 
 (* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)
@@ -20,7 +20,7 @@ Theorem t3: (N:Set)(o:N)(s:N->N)(d:N->N)
 	(s (s (s (s (s (s o))))))=o->
 	o=(s o).
 Intros.
-CC.
+Congruence.
 Save.
 
 (* Examples that fail due to dependencies *) 
@@ -40,29 +40,41 @@ Intros;Rewrite e;Reflexivity.
 Save.
 
 
-(* example that CC can solve 	
+(* example that Congruence. can solve 	
 	(dependent function applied to the same argument)*) 
 
-Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x).		
-Intros.	
-CC.
+Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x).		Intros.	
+Congruence.
 Save.
 
 (* Examples with injection rule *)
 
-Theorem t5 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d.
+Theorem inj1 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d.
 Intros.
-Split;CC.
+Split;Congruence.
 Save.
 
-Theorem t6 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))->(f c)=(f d)->c=d.
+Theorem inj2 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))->
+  (Some ? (f c))=(Some ? (f d))->c=d.                             
 Intros.
-CC.
+Congruence.
 Save.
 
-(* example with CCSolve (requires CC)*)
+(* Examples with discrimination rule *)
 
-Require CC.
+Theorem discr1 : true=false->False.
+Intros.
+Congruence.
+Save.
+
+Theorem discr2 : (Some ? true)=(Some ? false)->False.
+Intros.
+Congruence.
+Save.
+
+(* example with Congruence.Solve (requires CCSolve.v)*)
+
+Require CCSolve.
 
 Theorem t4 :  (A:Set; P:(A->Prop); a,b,c,d:A)a=b->c=d->
                  (P a)->((P b)->(P c))->(P d).
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index f26caca8e8..eecfc42b2d 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -179,7 +179,7 @@ Apply Hrec; Intros.
 Assert H2: `0<0`.
   Apply Zle_lt_trans with y; Intuition.
 Inversion H2.
-Ground.
+Firstorder.
 Unfold Zle Zcompare in H; Elim H; Auto.
 Defined.