new congruence

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

8 files changed, 924 insertions, 614 deletions

diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index b2eb2ab22..d6cc79657 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -12,39 +12,27 @@
 (* Downey,Sethi and Tarjan. *)
 
 open Util
+open Pp
+open Goptions
 open Names
 open Term
 
-let init_size=251
+let init_size=5
 
-type pa_constructor=
-    {head_constr: int;
-     arity:int;
-     nhyps:int;
-     args:int list;
-     term_head:int}
-
-
-module PacMap=Map.Make(struct type t=int*int let compare=compare end) 
-
-type term=
-    Symb of constr
-  | Appli of term*term
-  | Constructor of constructor*int*int (* constructor arity+ nhyps *)
+let cc_verbose=ref false 
 
-type rule=
-    Congruence
-  | Axiom of identifier
-  | Injection of int*int*int*int (* terms+head+arg position *)
+let debug msg (stdpp:std_ppcmds) = 
+  if !cc_verbose then msg stdpp
 
-type equality = {lhs:int;rhs:int;rule:rule}
-
-let swap eq=
-  let swap_rule=match eq.rule with
-      Congruence -> Congruence
-    | Injection (i,j,c,a) -> Injection (j,i,c,a)
-    | Axiom id -> anomaly "no symmetry for axioms"    
-  in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule}
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Congruence Verbose";
+      optkey=SecondaryTable("Congruence","Verbose"); 
+      optread=(fun ()-> !cc_verbose); 
+      optwrite=(fun b -> cc_verbose := b)}  
+  in
+    declare_bool_option gdopt
 
 (* Signature table *)
 
@@ -68,290 +56,452 @@ module ST=struct
 	  
   let query sign st=Hashtbl.find st.toterm sign
 	  
-  let delete t st=
+  let delete st t=
     try let sign=Hashtbl.find st.tosign t in
 	Hashtbl.remove st.toterm sign;
 	Hashtbl.remove st.tosign t
     with
 	Not_found -> ()
 
-  let rec delete_list l st=
-    match l with
-      []->()
-    | t::q -> delete t st;delete_list q st
+  let rec delete_set st s = Intset.iter (delete st) s
 	  
 end
-    
-(* Basic Union-Find algo w/o path compression *)
-    
-module UF = struct
 
-module IndMap=Map.Make(struct type t=inductive let compare=compare end) 
+type pa_constructor=
+    { cnode : int;
+      arity : int;
+      args  : int list}
 
-  type representative=
-      {mutable nfathers:int;
-       mutable fathers:int list;
-       mutable constructors:pa_constructor PacMap.t;
-       mutable inductives:(int * int) IndMap.t}
+module PacMap=Map.Make(struct 
+			 type t=pa_constructor 
+			 let compare=Pervasives.compare end) 
 
-  type cl = Rep of representative| Eqto of int*equality
+type cinfo=
+    {ci_constr: constructor; (* inductive type *)
+     ci_arity: int;     (* # args *)
+     ci_nhyps: int}     (* # projectable args *)
 
-  type vertex = Leaf| Node of (int*int) 
+type term=
+    Symb of constr
+  | Eps
+  | Appli of term*term
+  | Constructor of cinfo (* constructor arity + nhyps *)
 
-  type node = 
-      {clas:cl;
-       vertex:vertex;
-       term:term;
-       mutable node_constr: int PacMap.t}    
+type rule=
+    Congruence
+  | Axiom of identifier * bool 
+  | Injection of int * pa_constructor * int * pa_constructor * int
 
-  type t={mutable size:int;
-          map:(int,node) Hashtbl.t;
-          syms:(term,int) Hashtbl.t;
-	  sigtable:ST.t}
+type from=
+    Goal
+  | Hyp of identifier
+  | HeqG of identifier
+  | HeqnH of identifier * identifier
 
-  let empty ():t={size=0;
-		  map=Hashtbl.create init_size;
-		  syms=Hashtbl.create init_size;
-		  sigtable=ST.empty ()}
+type 'a eq = {lhs:int;rhs:int;rule:'a}
 
-  let rec find uf i=
-    match (Hashtbl.find uf.map i).clas with
-	Rep _ -> i
-      | Eqto (j,_) ->find uf j
-	  
-  let get_representative uf i=
-    let node=Hashtbl.find uf.map i in
-      match node.clas with
-	  Rep r ->r
-	| _ -> anomaly "get_representative: not a representative"
+type equality = rule eq
+
+type disequality = from eq
 
-  let get_constructor uf i=
-    match (Hashtbl.find uf.map i).term with
-	Constructor (cstr,_,_)->cstr
-      | _ -> anomaly "get_constructor: not a constructor"
+let swap eq : equality =
+  let swap_rule=match eq.rule with
+      Congruence -> Congruence
+    | Injection (i,pi,j,pj,k) -> Injection (j,pj,i,pi,k)
+    | Axiom (id,reversed) -> Axiom (id,not reversed)
+  in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule}
+    
+type inductive_status =
+    Unknown
+  | Partial of pa_constructor
+  | Partial_applied
+  | Total of (int * pa_constructor)
+
+type representative=
+    {mutable nfathers:int;
+     mutable lfathers:Intset.t;
+     mutable fathers:Intset.t;
+     mutable inductive_status: inductive_status;
+     mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
+
+type cl = Rep of representative| Eqto of int*equality
+  
+type vertex = Leaf| Node of (int*int) 
+
+type node = 
+    {mutable clas:cl;
+     mutable cpath: int; 
+     vertex:vertex;
+     term:term}
+    
+type forest=
+    {mutable max_size:int;
+     mutable size:int;
+     mutable map: node array;
+     axioms: (identifier,term*term) Hashtbl.t;
+     mutable epsilons: pa_constructor list;
+     syms:(term,int) Hashtbl.t}
+
+type state = 
+    {uf: forest;
+     sigtable:ST.t;
+     mutable terms: Intset.t; 
+     combine: equality Queue.t; 
+     marks: (int * pa_constructor) Queue.t;
+     mutable diseq: disequality list;
+     mutable pa_classes: Intset.t}
+
+let dummy_node =
+  {clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
+   cpath=min_int;
+   vertex=Leaf;
+   term=Symb (mkRel min_int)}
+
+let empty ():state =
+  {uf=
+     {max_size=init_size;
+      size=0;
+      map=Array.create init_size dummy_node;
+      epsilons=[];
+      axioms=Hashtbl.create init_size;
+      syms=Hashtbl.create init_size};
+  terms=Intset.empty;
+  combine=Queue.create ();
+  marks=Queue.create ();
+  sigtable=ST.empty ();
+  diseq=[];
+  pa_classes=Intset.empty}
+
+let forest state = state.uf 
+       
+let compress_path uf i j = uf.map.(j).cpath<-i
+			     
+let rec find_aux uf visited i=  
+  let j = uf.map.(i).cpath in 
+    if j<0 then let _ = List.iter (compress_path uf i) visited in i else
+      find_aux uf (i::visited) j
+	
+let find uf i= find_aux uf [] i
+		 
+let get_representative uf i=
+  match uf.map.(i).clas with
+      Rep r -> r
+    | _ -> anomaly "get_representative: not a representative"
+
+let find_pac uf i pac =
+  PacMap.find pac (get_representative uf i).constructors
+
+let get_constructor_info uf i=
+  match uf.map.(i).term with
+      Constructor cinfo->cinfo
+    | _ -> anomaly "get_constructor: not a constructor"
+	
+let size uf i=
+  (get_representative uf i).nfathers
 
+let axioms uf = uf.axioms
 
-  let fathers uf i=
-    (get_representative uf i).fathers
-	  
-  let size uf i=
-    (get_representative uf i).nfathers
+let epsilons uf = uf.epsilons
 
-  let add_father uf i t=
-    let r=get_representative uf i in
-      r.nfathers<-r.nfathers+1;
-      r.fathers<-t::r.fathers 
+let add_lfather uf i t=
+  let r=get_representative uf i in
+    r.nfathers<-r.nfathers+1;
+    r.lfathers<-Intset.add t r.lfathers;
+    r.fathers <-Intset.add t r.fathers
 
-  let pac_map uf i=
-    (get_representative uf i).constructors  
+let add_rfather uf i t=
+  let r=get_representative uf i in
+    r.nfathers<-r.nfathers+1;
+    r.fathers <-Intset.add t r.fathers
 
-  let pac_arity uf i sg=
-    (PacMap.find sg (get_representative uf i).constructors).arity
+exception Discriminable of int * pa_constructor * int * pa_constructor 
 
-  let add_node_pac uf i sg j=
-    let node=Hashtbl.find uf.map i in
-      if not (PacMap.mem sg node.node_constr) then
-	node.node_constr<-PacMap.add sg j node.node_constr 
-  
-  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 
-    let add_pac sg pac=
-      try  
-	let opac=PacMap.find sg rep.constructors in
-	  if (snd sg)>0 then () else
-	    let tk=pac.term_head 
-	    and tl=opac.term_head in
-	    let rec f n lk ll q=
-	      if n > 0 then match (lk,ll) with
-		  k::qk,l::ql->
-		    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 -> (* Still Unknown Constructor *)
-	rep.constructors <- PacMap.add sg pac rep.constructors;
-	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
+let append_pac t p =
+  {p with arity=pred p.arity;args=t::p.args} 
+
+let tail_pac p=
+  {p with arity=succ p.arity;args=List.tl p.args}
+    
+let add_pac rep pac t =
+  if not (PacMap.mem pac rep.constructors) then
+    rep.constructors<-PacMap.add pac t rep.constructors
+
+let term uf i=uf.map.(i).term
+		
+let subterms uf i=
+  match uf.map.(i).vertex with
+      Node(j,k) -> (j,k)
+    | _ -> anomaly "subterms: not a node"
 	
-  let term uf i=(Hashtbl.find uf.map i).term
-		  
-  let subterms uf i=
-    match (Hashtbl.find uf.map i).vertex with
-	Node(j,k) -> (j,k)
-      | _ -> anomaly "subterms: not a node"
-
-  let signature uf i=
-    let j,k=subterms uf i in (find uf j,find uf k)
-
-  let nodes uf=  (* cherche les noeuds binaires *)
-    Hashtbl.fold 
-      (fun i node l->
-	 match node.vertex with 
-	     Node (_,_)->i::l
-	   | _ ->l) uf.map [] 
-
-  let next uf=
-    let n=uf.size in uf.size<-n+1; n
+let signature uf i=
+  let j,k=subterms uf i in (find uf j,find uf k)
+			     
+let next uf=
+  let size=uf.size in
+  let nsize= succ size in
+    if nsize=uf.max_size then
+      let newmax=uf.max_size * 3 / 2 + 1 in
+      let newmap=Array.create newmax dummy_node in
+	begin
+	  uf.max_size<-newmax;
+	  Array.blit uf.map 0 newmap 0 size;
+	  uf.map<-newmap
+	end 
+    else ();
+    uf.size<-nsize; 
+    size
 	
-  let new_representative pm im=
-    {nfathers=0;
-     fathers=[];
-     constructors=pm;
-     inductives=im}
-
-  let rec add uf t= 
+let new_representative ()=
+  {nfathers=0;
+   lfathers=Intset.empty;
+   fathers=Intset.empty;
+   inductive_status=Unknown;
+   constructors=PacMap.empty}
+    
+let rec add_term state t= 
+  let uf=state.uf in
     try Hashtbl.find uf.syms t with 
 	Not_found ->
 	  let b=next uf in
 	  let new_node=
 	    match t with
-		Symb s -> 
-		  {clas=Rep (new_representative PacMap.empty IndMap.empty);
-		   vertex=Leaf;term=t;node_constr=PacMap.empty}
+		Symb _ | Eps -> 
+		  {clas= Rep (new_representative ());
+		   cpath= -1;
+		   vertex= Leaf;
+		   term= t}
 	      | 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 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
-		  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}
+		  let i1=add_term state t1 and i2=add_term state t2 in
+		    add_lfather uf (find uf i1) b;
+		    add_rfather uf (find uf i2) b;
+		    state.terms<-Intset.add b state.terms;
+		    {clas= Rep (new_representative ());
+		     cpath= -1;
+		     vertex= Node(i1,i2);
+		     term= t}
+	      | Constructor cinfo ->
+		  let pac =
+		    {cnode= b;
+		     arity= cinfo.ci_arity;
+		     args=[]} in
+		    Queue.add (b,pac) state.marks;
+		    {clas=Rep (new_representative ());
+		     cpath= -1;
+		     vertex=Leaf;
+		     term=t}
 	  in
-	    Hashtbl.add uf.map b new_node;
+	    uf.map.(b)<-new_node;
 	    Hashtbl.add uf.syms t b;
 	    b
 
-  let link uf i j eq= (* links i -> j *)
-    let node=Hashtbl.find uf.map i in 
-      Hashtbl.replace uf.map i {node with clas=Eqto (j,eq)}
-	      
-  let union uf i1 i2 eq=
-    let r1= get_representative uf i1 
-    and r2= get_representative uf i2 in
-      link uf i1 i2 eq;
-      r2.nfathers<-r1.nfathers+r2.nfathers;
-      r2.fathers<-r1.fathers@r2.fathers;
-      add_pacs uf i2 r1.constructors 
+let add_equality state id s t=
+  let i = add_term state s in
+  let j = add_term state t in
+    Queue.add {lhs=i;rhs=j;rule=Axiom(id,false)} state.combine;
+    Hashtbl.add state.uf.axioms id (s,t)
+
+let add_disequality state from s t =
+  let i = add_term state s in
+  let j = add_term state t in
+    state.diseq<-{lhs=i;rhs=j;rule=from}::state.diseq
+
+let link uf i j eq = (* links i -> j *)
+  let node=uf.map.(i) in 
+    node.clas<-Eqto (j,eq);
+    node.cpath<-j
 	
-  let rec down_path uf i l=
-    match (Hashtbl.find uf.map i).clas with
-	Eqto(j,t)->down_path uf j (((i,j),t)::l)
-      | Rep _ ->l
-
-  let rec min_path=function
-      ([],l2)->([],l2)
-    | (l1,[])->(l1,[])
-    | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) 
-    | cpl -> cpl
+let rec down_path uf i l=
+  match uf.map.(i).clas with
+      Eqto(j,t)->down_path uf j (((i,j),t)::l)
+    | Rep _ ->l
 	
-  let join_path uf i j=
-    assert (find uf i=find uf j);
-    min_path (down_path uf i [],down_path uf j [])
+let rec min_path=function
+    ([],l2)->([],l2)
+  | (l1,[])->(l1,[])
+  | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) 
+  | cpl -> cpl
       
-end    
-    
-let rec combine_rec uf=function 
-    []->[]
-  | t::pending->
-      let combine=combine_rec uf pending in
-      let s=UF.signature uf t in
-      let u=snd (UF.subterms uf t) in
-      let f (c,a) pac pacs=
-	if a=0 then pacs else 
-	  let sg=(c,a-1) in
-	    UF.add_node_pac uf t sg pac.term_head;
-	    PacMap.add sg {pac with args=u::pac.args;term_head=t} pacs
-      in
-      let pacs=PacMap.fold f (UF.pac_map uf (fst s)) PacMap.empty in
-      let i=UF.find uf t in
-      let (p,c)=UF.add_pacs uf i pacs in
-      let combine2=(combine_rec uf p)@c@combine in
-      try {lhs=t;rhs=ST.query s uf.UF.sigtable;rule=Congruence}::combine2 with
-	Not_found->
-	  ST.enter t s uf.UF.sigtable;combine2
-	    
-let rec process_rec uf=function
-    []->[] 
-  | eq::combine->
-      let pending=process_rec uf combine in
-      let i=UF.find uf eq.lhs 
-      and j=UF.find uf eq.rhs in
-      if i=j then
-	pending
+let join_path uf i j=
+  assert (find uf i=find uf j);
+  min_path (down_path uf i [],down_path uf j [])
+
+let union state i1 i2 eq=
+  debug msgnl (str "Linking " ++ int i1 ++ str " and " ++ int i2 ++ str ".");
+  let r1= get_representative state.uf i1 
+  and r2= get_representative state.uf i2 in
+    link state.uf i1 i2 eq;
+    let f= Intset.union r1.fathers r2.fathers in
+      r2.nfathers<-Intset.cardinal f;
+      r2.fathers<-f;
+      r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
+      ST.delete_set state.sigtable r1.fathers;
+      state.terms<-Intset.union state.terms r1.fathers;       
+      PacMap.iter (fun pac b -> Queue.add (b,pac) state.marks) r1.constructors;
+      match r1.inductive_status,r2.inductive_status with 
+	  Unknown,_ -> ()
+	| Partial pac,Unknown -> 
+	    r2.inductive_status<-Partial pac;
+	    state.pa_classes<-Intset.remove i1 state.pa_classes;
+	    state.pa_classes<-Intset.add i2 state.pa_classes
+	| Partial _ ,(Partial _ |Partial_applied) -> 
+	    state.pa_classes<-Intset.remove i1 state.pa_classes
+	| Partial_applied,Unknown -> 
+	    r2.inductive_status<-Partial_applied	      
+	| Partial_applied,Partial _ -> 
+	    state.pa_classes<-Intset.remove i2 state.pa_classes;
+	    r2.inductive_status<-Partial_applied
+	| Total cpl,Unknown -> r2.inductive_status<-Total cpl;
+	| Total cpl,Total _ -> Queue.add cpl state.marks    
+	| _,_ -> () 
+            
+let merge eq state = (* merge and no-merge *)
+  debug msgnl 
+    (str "Merging " ++ int eq.lhs ++ str " and " ++ int eq.rhs ++ str ".");
+  let uf=state.uf in
+  let i=find uf eq.lhs 
+  and j=find uf eq.rhs in
+    if i<>j then 
+      if (size uf i)<(size uf j) then
+	union state i j eq
       else
-	if (UF.size uf i)<(UF.size uf j) then
-	  let l=UF.fathers uf i in
-	  let (p,c)=UF.union uf i j eq in
-	  let _ =ST.delete_list l uf.UF.sigtable in
-	  let inj_pending=process_rec uf c in
-	    inj_pending@p@l@pending
+	union state j i (swap eq)
+
+let update t state = (* update 1 and 2 *)
+  debug msgnl 
+    (str "Updating term " ++ int t ++ str ".");
+  let (i,j) as sign = signature state.uf t in
+  let (u,v) = subterms state.uf t in
+  let rep = get_representative state.uf i in
+    begin
+      match rep.inductive_status with 
+	  Partial _ ->
+	    rep.inductive_status <- Partial_applied;
+	    state.pa_classes <- Intset.remove i state.pa_classes
+	| _ -> ()
+    end;
+    PacMap.iter 
+      (fun pac _ -> Queue.add (t,append_pac v pac) state.marks) 
+      rep.constructors; 
+    try 
+      let s = ST.query sign state.sigtable in 
+	Queue.add {lhs=t;rhs=s;rule=Congruence} state.combine
+    with 
+	Not_found -> ST.enter t sign state.sigtable
+
+let process_mark t pac state =
+  debug msgnl 
+    (str "Processing mark for term " ++ int t ++ str ".");
+  let i=find state.uf t in
+  let rep=get_representative state.uf i in
+    match rep.inductive_status with
+	Total (s,opac) ->
+	  if pac.cnode <> opac.cnode then (* Conflict *) 
+	    raise (Discriminable (s,opac,t,pac)) 
+	  else (* Match *)
+	    let cinfo = get_constructor_info state.uf pac.cnode in
+	    let rec f n oargs args=
+	      if n > 0 then 
+		match (oargs,args) with
+		    s1::q1,s2::q2->
+		      Queue.add 
+			{lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
+			state.combine;
+		      f (n-1) q1 q2 
+		  | _-> anomaly 
+		      "add_pacs : weird error in injection subterms merge" 
+	    in f cinfo.ci_nhyps opac.args pac.args
+      | Partial_applied | Partial _ ->
+	  add_pac rep pac t;
+	  state.terms<-Intset.union rep.lfathers state.terms
+      | Unknown ->
+	  if pac.arity = 0 then
+	    rep.inductive_status <- Total (t,pac)
+	  else
+	    begin
+	      add_pac rep pac t;
+	      state.terms<-Intset.union rep.lfathers state.terms;
+	      rep.inductive_status <- Partial pac;
+	      state.pa_classes<- Intset.add i state.pa_classes
+	    end
+
+type explanation =
+    Discrimination of (int*pa_constructor*int*pa_constructor)
+  | Contradiction of disequality
+  | Incomplete
+
+let check_disequalities state =
+  let uf=state.uf in
+  let rec check_aux = function
+      dis::q -> 
+	debug msg 
+	(str "Checking if " ++ int dis.lhs ++ str " = " ++ 
+	 int dis.rhs ++ str " ... ");  
+	if find uf dis.lhs=find uf dis.rhs then 
+	  begin debug msgnl (str "Yes");Some dis end 
 	else
-	  let l=UF.fathers uf j in
-	  let (p,c)=UF.union uf j i (swap eq) in
-	  let _ =ST.delete_list l uf.UF.sigtable in
-	  let inj_pending=process_rec uf c in
-	    inj_pending@p@l@pending
-	  
-let rec cc_rec uf=function
-    []->()
-  | pending->
-      let combine=combine_rec uf pending in
-      let pending0=process_rec uf combine in
-	cc_rec uf pending0
-	
-let cc uf=cc_rec uf (UF.nodes uf)
-
-let rec make_uf=function
-    []->UF.empty ()
-  | (ax,(t1,t2))::q->
-      let uf=make_uf q in
-      let i1=UF.add uf t1 in
-      let i2=UF.add uf t2 in
-      let j1=UF.find uf i1 and j2=UF.find uf i2 in
-	if j1=j2 then uf else  
-	    let (_,inj_combine)=
-		UF.union uf j1 j2 {lhs=i1;rhs=i2;rule=Axiom ax} in
-	    let _ = process_rec uf inj_combine in uf
-      
-let add_one_diseq uf (t1,t2)=(UF.add uf t1,UF.add uf t2)
-
-let add_disaxioms uf disaxioms=
-  let f (id,cpl)=(id,add_one_diseq uf cpl) in
-    List.map f disaxioms
-
-let check_equal uf (i1,i2) = UF.find uf i1 = UF.find uf i2
-
-let find_contradiction uf diseq =
-  List.find (fun (id,cpl) -> check_equal uf cpl) diseq
- 
+	  begin debug msgnl (str "No");check_aux q end
+    | [] -> None 
+  in
+    check_aux state.diseq
+
+let one_step state =
+    try
+      let eq = Queue.take state.combine in
+	merge eq state
+    with Queue.Empty -> 
+      try 
+	let (t,m) = Queue.take state.marks in
+	  process_mark t m state
+      with Queue.Empty ->
+	  let t = Intset.choose state.terms in
+	    state.terms<-Intset.remove t state.terms;
+	    update t state
+
+let complete_one_class state i=
+  match (get_representative state.uf i).inductive_status with
+      Partial pac ->
+	let rec app t n = 
+	  if n<=0 then t else
+	    app (Appli(t,Eps)) (n-1) in
+	  state.uf.epsilons <- pac :: state.uf.epsilons; 
+	  ignore (add_term state (app (term state.uf i) pac.arity))
+    | _ -> anomaly "wrong incomplete class" 
+
+let complete state =
+  Intset.iter (complete_one_class state) state.pa_classes
+
+let rec execute first_run state =
+  debug msgnl (str "Executing ... ");
+  try
+    while true do 
+      one_step state
+    done;
+    anomaly "keep out of here" 
+  with 
+      Discriminable(s,spac,t,tpac) -> 
+	Some
+	begin
+	  if first_run then 
+	    Discrimination (s,spac,t,tpac)
+	  else
+	    Incomplete
+	end
+    | Not_found ->
+	match check_disequalities state with
+	    None -> 
+	      if not(Intset.is_empty state.pa_classes) then
+		begin 
+		  debug msgnl 
+		    (str "First run was incomplete, completing ... ");
+		  complete state;
+		  execute false state
+		end
+	      else None
+	  | Some dis -> Some
+	      begin
+		if first_run then 
+		  Contradiction dis
+		else
+		  Incomplete
+	      end
 
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 71a0227a3..3390769be 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -8,13 +8,107 @@
 
 (* $Id$ *)
 
-type pa_constructor
-    (*{head: int; arity: int; args: (int * int) list}*)
+open Util
+open Term
+open Names
 
-module PacMap:Map.S with type key=int * int 
+type cinfo =
+    {ci_constr: constructor; (* inductive type *)
+     ci_arity: int;     (* # args *)
+     ci_nhyps: int}     (* # projectable args *)
+
+type term =
+    Symb of constr
+  | Eps
+  | Appli of term*term
+  | Constructor of cinfo (* constructor arity + nhyps *)
+
+type pa_constructor =
+    { cnode : int;
+      arity : int;
+      args  : int list}
+
+module PacMap : Map.S with type key = pa_constructor  
+
+type forest
+
+type state 
+
+type rule=
+    Congruence
+  | Axiom of identifier * bool 
+  | Injection of int * pa_constructor * int * pa_constructor * int
+
+type from=
+    Goal
+  | Hyp of identifier
+  | HeqG of identifier
+  | HeqnH of identifier * identifier
+
+type 'a eq = {lhs:int;rhs:int;rule:'a}
+
+type equality = rule eq
+
+type disequality = from eq
+
+type explanation =
+    Discrimination of (int*pa_constructor*int*pa_constructor)
+  | Contradiction of disequality
+  | Incomplete
+
+val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
+
+val forest : state -> forest
+
+val axioms : forest -> (identifier, term * term) Hashtbl.t
+
+val epsilons : forest -> pa_constructor list
+
+val empty : unit -> state
+
+val add_term : state -> term -> int
+
+val add_equality : state -> identifier -> term -> term -> unit
+
+val add_disequality : state -> from -> term -> term -> unit
+
+val tail_pac : pa_constructor -> pa_constructor
+
+val find : forest -> int -> int
+
+val find_pac : forest -> int -> pa_constructor -> int
+
+val term : forest -> int -> term
+
+val get_constructor_info : forest -> int -> cinfo
+
+val subterms : forest -> int -> int * int
+
+val join_path : forest -> int -> int -> 
+  ((int * int) * equality) list * ((int * int) * equality) list
+
+val execute : bool -> state -> explanation option
+
+
+
+
+
+
+
+
+
+
+
+
+
+(*type pa_constructor
+
+
+module PacMap:Map.S with type key=pa_constructor
 
 type term = 
     Symb of Term.constr 
+  | Eps
   | Appli of term * term 
   | Constructor of Names.constructor*int*int
 
@@ -79,6 +173,6 @@ val check_equal : UF.t -> int * int -> bool
 val find_contradiction : UF.t -> 
   (Names.identifier * (int * int)) list -> 
   (Names.identifier * (int * int))
-
+*)
 
 
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 60b5e7469..cf7c7d30e 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -51,8 +51,8 @@ let pcongr=function
 let build_proof uf=
   
   let rec equal_proof i j=
-    if i=j then Refl (UF.term uf i) else 
-      let (li,lj)=UF.join_path uf i j in
+    if i=j then Refl (term uf i) else 
+      let (li,lj)=join_path uf i j in
 	ptrans (path_proof i li,psym (path_proof j lj))
   
   and edge_proof ((i,j),eq)=
@@ -60,45 +60,44 @@ let build_proof uf=
     let pj=psym (equal_proof j eq.rhs) in
     let pij=
       match eq.rule with 
-	  Axiom s->Ax s
+	  Axiom (s,reversed)->if reversed then SymAx s else Ax s
 	| Congruence ->congr_proof eq.lhs eq.rhs
-	| Injection (ti,tj,c,a) ->
-	    let p=equal_proof ti tj 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" 
+	| Injection (ti,ipac,tj,jpac,k) ->
+	    let p=ind_proof ti ipac tj jpac in
+	    let cinfo= get_constructor_info uf ipac.cnode in
+	      Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k)	
     in  ptrans(ptrans (pi,pij),pj)
 
-  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 constr_proof i t ipac=
+    if ipac.args=[] then
+      equal_proof i t
+    else
+      let npac=tail_pac ipac in
+      let (j,arg)=subterms uf t in
+      let targ=term uf arg in
+      let rj=find uf j in
+      let u=find_pac uf rj npac in
+      let p=constr_proof j u npac in
+	ptrans (equal_proof i t, pcongr (p,Refl targ))
 
   and path_proof i=function
-      [] -> Refl (UF.term uf i)
+      [] -> Refl (term uf i)
     | 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   
+    let (i1,i2) = subterms uf i
+    and (j1,j2) = subterms uf j in   
       pcongr (equal_proof i1 j1, equal_proof i2 j2)
 	
-  and discr_proof i ci j cj=
+  and ind_proof i ipac j jpac=
     let p=equal_proof i j 
-    and p1=constr_proof i i ci 0 
-    and p2=constr_proof j j cj 0 in
+    and p1=constr_proof i i ipac 
+    and p2=constr_proof j j jpac in
       ptrans(psym p1,ptrans(p,p2))
   in
     function
-	`Prove_goal (i,j) | `Refute_hyp (i,j) -> equal_proof i j
-      | `Discriminate (i,ci,j,cj)-> discr_proof i ci j cj
+	`Prove (i,j) -> equal_proof i j
+      | `Discr (i,ci,j,cj)-> ind_proof i ci j cj
 
 let rec nth_arg t n=
   match t with 
@@ -110,8 +109,8 @@ let rec nth_arg t n=
 
 let rec type_proof axioms p=
   match p with
-      Ax s->List.assoc s axioms
-    | SymAx s-> let (t1,t2)=List.assoc s axioms in (t2,t1)
+      Ax s->Hashtbl.find axioms s
+    | SymAx s-> let (t1,t2)=Hashtbl.find axioms s in (t2,t1)
     | Refl t-> t,t
     | Trans (p1,p2)->
 	let (s1,t1)=type_proof axioms p1 
@@ -125,33 +124,3 @@ let rec type_proof axioms p=
 	let (ti,tj)=type_proof axioms p in
 	  nth_arg ti (n-a),nth_arg tj (n-a)
 
-let by_contradiction uf diseq axioms disaxioms= 
-  try 
-    let id,cpl=find_contradiction uf diseq in
-    let prf=build_proof uf (`Refute_hyp cpl) in
-      if List.assoc id disaxioms=type_proof axioms prf then
-	`Refute_hyp (id,prf)
-      else 
-	anomaly "wrong proof generated"
-  with Not_found ->
-    errorlabstrm  "Congruence" (Pp.str "I couldn't solve goal")  
-
-let cc_proof axioms disaxioms glo=
-  try
-    let uf=make_uf axioms in
-    let diseq=add_disaxioms uf disaxioms in
-      match glo with 
-	  Some cpl ->
-	    let goal=add_one_diseq uf cpl in cc uf;
-	      if check_equal uf goal then 
-		let prf=build_proof uf (`Prove_goal goal) in
-		  if cpl=type_proof axioms prf then
-		    `Prove_goal prf
-		  else anomaly "wrong proof generated"
-	      else by_contradiction uf diseq axioms disaxioms  
-	| None -> cc uf; by_contradiction uf diseq axioms disaxioms
-    with UF.Discriminable (i,ci,j,cj,uf) ->
-      let prf=build_proof uf (`Discriminate (i,ci,j,cj)) in 
-	`Discriminate (UF.get_constructor uf ci,prf) 
-
-
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index 363a1c402..456d13e4b 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -19,27 +19,12 @@ type proof =
   | Congr of proof * proof
   | Inject of proof * constructor * int * int
 
-val pcongr : proof * proof -> proof
-val ptrans : proof * proof -> proof
-val psym : proof -> proof
-val pcongr : proof * proof -> proof
-
 val build_proof : 
-  UF.t -> 
-  [ `Discriminate of int * int * int * int
-  | `Prove_goal of int * int
-  | `Refute_hyp of int * int ]
-  -> proof
+  forest -> 
+  [ `Discr of int * pa_constructor * int * pa_constructor
+  | `Prove of int * int ] -> proof
 
 val type_proof :
-  (identifier * (term * term)) list -> proof -> term * term
-
-val cc_proof :
-  (identifier * (term * term)) list ->
-  (identifier * (term * term)) list ->
-  (term * term) option ->
-  [ `Discriminate of constructor * proof
-  | `Prove_goal of proof
-  | `Refute_hyp of identifier * proof ]
+  (identifier, (term * term)) Hashtbl.t -> proof -> term * term
 
 
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
new file mode 100644
index 000000000..d685051e9
--- /dev/null
+++ b/contrib/cc/cctac.ml
@@ -0,0 +1,336 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \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$ *)
+
+(* This file is the interface between the c-c algorithm and Coq *)
+
+open Evd
+open Proof_type
+open Names
+open Libnames
+open Nameops
+open Inductiveops
+open Declarations
+open Term
+open Termops
+open Tacmach
+open Tactics
+open Tacticals
+open Ccalgo
+open Tacinterp
+open Ccproof
+open Pp
+open Util
+open Format
+
+let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
+
+let _f_equal = constant ["Init";"Logic"] "f_equal"
+
+let _eq_rect = constant ["Init";"Logic"] "eq_rect"
+
+let _eq = constant ["Init";"Logic"] "eq"
+
+let _False = constant ["Init";"Logic"] "False"
+
+(* decompose member of equality in an applicative format *)
+
+let whd env=
+  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let whd_delta env=
+   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let rec decompose_term env t=
+    match kind_of_term (whd env t) with
+      App (f,args)->
+	let tf=decompose_term env f in
+	let targs=Array.map (decompose_term env) args in
+	  Array.fold_left (fun s t->Appli (s,t)) tf targs
+    | Construct c->
+	let (_,oib)=Global.lookup_inductive (fst c) in
+	let nargs=mis_constructor_nargs_env env c in
+	  Constructor {ci_constr=c;
+		       ci_arity=nargs;
+		       ci_nhyps=nargs-oib.mind_nparams}
+    | _ ->(Symb t)
+	
+(* decompose equality in members and type *)
+	
+let atom_of_constr env term =
+  let wh =  (whd_delta env term) in
+  let kot = kind_of_term wh in 
+    match kot with
+      App (f,args)->
+	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3 
+	  then `Eq (args.(0),
+		   decompose_term env args.(1), 
+		   decompose_term env args.(2)) 
+	  else `Other (decompose_term env term)
+    | _ -> `Other (decompose_term env term)
+
+let rec litteral_of_constr env term=
+  match kind_of_term (whd_delta env term) with
+      Prod (_,atom,ff) -> 
+	if eq_constr ff (Lazy.force _False) then
+	  match (atom_of_constr env atom) with
+	      `Eq(t,a,b) -> `Neq(t,a,b)
+	    | `Other(p) -> `Nother(p)
+	else 
+	  `Other (decompose_term env term)
+    | _ -> atom_of_constr env term
+	
+(* rebuild a term from applicative format *)
+    
+let rec make_term = function
+    Symb s->s
+  | Eps -> anomaly "epsilon constant has no value" 
+  | Constructor cinfo -> mkConstruct cinfo.ci_constr 
+  | Appli (s1,s2)->
+      make_app [(make_term s2)] s1
+and make_app l=function
+    Appli (s1,s2)->make_app ((make_term s2)::l) s1    
+  | other -> applistc (make_term other) l 
+
+(* store all equalities from the context *)
+	
+let rec make_prb gls additionnal_terms =
+  let env=pf_env gls in
+  let state = empty () in
+  let pos_hyps = ref [] in
+  let neg_hyps =ref [] in
+    List.iter
+      (fun c ->
+	 let t = decompose_term env c in
+	   ignore (add_term state t)) additionnal_terms; 
+    List.iter 
+      (fun (id,_,e) ->
+	 begin
+	   match litteral_of_constr env e with
+	       `Eq (t,a,b) -> add_equality state id a b
+	     | `Neq (t,a,b) -> add_disequality state (Hyp id) a b
+	     | `Other ph ->
+		 List.iter 
+		   (fun (idn,nh) -> 
+		      add_disequality state (HeqnH (id,idn)) ph nh) 
+		   !neg_hyps;
+		 pos_hyps:=(id,ph):: !pos_hyps
+	     | `Nother nh ->
+		 List.iter 
+		   (fun (idp,ph) -> 
+		      add_disequality state (HeqnH (idp,id)) ph nh) 
+		   !pos_hyps;
+		 neg_hyps:=(id,nh):: !neg_hyps
+	 end) gls.it.evar_hyps;
+    begin
+      match atom_of_constr env gls.it.evar_concl with
+	  `Eq (t,a,b) -> add_disequality state Goal a b
+	|	`Other g ->  
+		  List.iter 
+	      (fun (idp,ph) -> 
+		 add_disequality state (HeqG idp) ph g) !pos_hyps
+    end;
+    state
+
+(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
+
+let build_projection intype outtype (cstr:constructor) special default gls=
+  let env=pf_env gls in 
+  let (h,argv) = 
+    try destApp intype with 
+	Invalid_argument _ -> (intype,[||])  in
+  let ind=destInd h in 
+  let types=Inductiveops.arities_of_constructors env ind in
+  let lp=Array.length types in
+  let ci=(snd cstr)-1 in
+  let branch i=
+    let ti=Term.prod_appvect types.(i) argv in
+    let rc=fst (Sign.decompose_prod_assum ti) in
+    let head=
+      if i=ci then special else default in  
+      Sign.it_mkLambda_or_LetIn head rc in
+  let branches=Array.init lp branch in
+  let casee=mkRel 1 in
+  let pred=mkLambda(Anonymous,intype,outtype) in
+  let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
+  let body= mkCase(case_info, pred, casee, branches) in
+  let id=pf_get_new_id (id_of_string "t") gls in     
+    mkLambda(Name id,intype,body)
+  
+(* generate an adhoc tactic following the proof tree  *)
+
+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 axioms p1);(proof_tac axioms p2)])
+  | Congr (p1,p2)->
+      fun gls->
+	let (f1,f2)=(type_proof axioms p1) 
+	and (x1,x2)=(type_proof axioms p2) in
+        let tf1=make_term f1 and tx1=make_term x1 
+	and tf2=make_term f2 and tx2=make_term x2 in
+	let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1
+	and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in
+	let id=pf_get_new_id (id_of_string "f") gls in
+	let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
+	let lemma1=
+	  mkApp(Lazy.force _f_equal,[|typf;typfx;appx1;tf1;tf2|])
+	and lemma2=
+	  mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in
+	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
+	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
+  	      tclFIRST
+		[tclTHEN (apply lemma2) (proof_tac axioms p2);
+		 reflexivity;
+		 fun gls ->
+		   errorlabstrm  "Congruence" 
+		   (Pp.str 
+		      "I don't know how to handle dependent equality")]]
+	     gls)
+  | Inject (prf,cstr,nargs,argind)  as gprf->
+      (fun gls ->
+	 let ti,tj=type_proof axioms prf in
+	 let ai,aj=type_proof axioms gprf in
+	 let cti=make_term ti in
+	 let ctj=make_term tj in
+	 let cai=make_term ai in
+	 let intype=pf_type_of gls cti in
+	 let outtype=pf_type_of gls cai in
+	 let special=mkRel (1+nargs-argind) in
+	 let default=make_term ai in
+	 let proj=build_projection intype outtype cstr special default gls in
+	 let injt=
+	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in 
+	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
+
+let refute_tac axioms id t1 t2 p gls =      
+  let tt1=make_term t1 and tt2=make_term t2 in
+  let intype=pf_type_of gls tt1 in
+  let neweq=
+    mkApp(Lazy.force _eq,
+	  [|intype;tt1;tt2|]) in
+  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let false_t=mkApp (mkVar id,[|mkVar hid|]) in
+    tclTHENS (true_cut (Name hid) neweq)
+      [proof_tac axioms p; simplest_elim false_t] gls
+
+let convert_to_goal_tac axioms id t1 t2 p gls =
+  let tt1=make_term t1 and tt2=make_term t2 in
+  let sort=pf_type_of gls tt2 in
+  let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in 
+  let e=pf_get_new_id (id_of_string "e") gls in
+  let x=pf_get_new_id (id_of_string "X") gls in
+  let identity=mkLambda (Name x,sort,mkRel 1) in 
+  let endt=mkApp (Lazy.force _eq_rect,
+		  [|sort;tt1;identity;mkVar id;tt2;mkVar e|]) in
+    tclTHENS (true_cut (Name e) neweq) 
+      [proof_tac axioms p;exact_check endt] gls
+
+let convert_to_hyp_tac axioms id1 t1 id2 t2 p gls =
+  let tt2=make_term t2 in
+  let h=pf_get_new_id (id_of_string "H") gls in
+  let false_t=mkApp (mkVar id2,[|mkVar h|]) in
+    tclTHENS (true_cut (Name h) tt2)
+      [convert_to_goal_tac axioms id1 t1 t2 p;
+       simplest_elim false_t] gls
+  
+let discriminate_tac axioms cstr p gls =
+  let t1,t2=type_proof axioms p in 
+  let tt1=make_term t1 and tt2=make_term t2 in
+  let intype=pf_type_of gls tt1 in
+  let concl=pf_concl gls in
+  let outsort=mkType (new_univ ()) in
+  let xid=pf_get_new_id (id_of_string "X") gls in
+  let tid=pf_get_new_id (id_of_string "t") gls in
+  let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
+  let trivial=pf_type_of gls identity in
+  let outtype=mkType (new_univ ()) in
+  let pred=mkLambda(Name xid,outtype,mkRel 1) in
+  let hid=pf_get_new_id (id_of_string "Heq") gls in     
+  let proj=build_projection intype outtype cstr trivial concl gls in
+  let injt=mkApp (Lazy.force _f_equal,
+		  [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
+  let endt=mkApp (Lazy.force _eq_rect,
+		  [|outtype;trivial;pred;identity;concl;injt|]) in
+  let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in
+    tclTHENS (true_cut (Name hid) neweq) 
+      [proof_tac axioms p;exact_check endt] gls
+      
+(* wrap everything *)
+	
+let build_term_to_complete uf meta pac =
+  let cinfo = get_constructor_info uf pac.cnode in
+  let real_args = List.map (fun i -> make_term (term uf i)) pac.args in
+  let dummy_args = List.rev (list_tabulate meta pac.arity) in
+  let all_args = List.rev_append real_args dummy_args in
+    applistc (mkConstruct cinfo.ci_constr) all_args
+      
+let cc_tactic additionnal_terms gls=
+  Coqlib.check_required_library ["Coq";"Init";"Logic"];
+  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
+  let state = make_prb gls additionnal_terms in
+  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
+  let sol = execute true state in
+  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
+  let uf=forest state in
+    match sol with
+	None -> tclFAIL 0 "congruence failed" gls  
+      | Some reason ->
+	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
+	  match reason with
+	      Discrimination (i,ipac,j,jpac) ->
+		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in	  
+		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+		  discriminate_tac (axioms uf) cstr p gls
+	    | Incomplete ->
+		let metacnt = ref 0 in
+		let newmeta _ = incr metacnt; mkMeta !metacnt in
+		let terms_to_complete = 
+		  List.map 
+		    (build_term_to_complete uf newmeta) 
+		    (epsilons uf) in 
+		  Pp.msgnl
+		    (Pp.str "Goal is solvable by congruence but \
+ some arguments are missing.");
+		  Pp.msgnl
+		    (Pp.str "  Try " ++
+		     hov 8
+		       begin 
+			 str "\"congruence with (" ++  
+			 prlist_with_sep 
+			   (fun () -> str ")" ++ pr_spc () ++ str "(")
+			   (print_constr_env (pf_env gls))
+			   terms_to_complete ++ 
+			 str ")\","
+		       end);
+		  Pp.msgnl
+		    (Pp.str "  replacing metavariables by arbitrary terms.");
+		  tclFAIL 0 "Incomplete" gls
+	    | Contradiction dis ->
+		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+		let ta=term uf dis.lhs and tb=term uf dis.rhs in
+		let axioms = axioms uf in 
+		  match dis.rule with
+		      Goal -> proof_tac axioms p gls
+		    | Hyp id -> refute_tac axioms id ta tb p gls
+		    | HeqG id -> 
+			convert_to_goal_tac axioms id ta tb p gls
+		    | HeqnH (ida,idb) -> 
+			convert_to_hyp_tac axioms ida ta idb tb p gls
+		    
+
+let cc_fail gls =
+  errorlabstrm  "Congruence" (Pp.str "congruence failed.")     
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
deleted file mode 100644
index 3ac3b42f4..000000000
--- a/contrib/cc/cctac.ml4
+++ /dev/null
@@ -1,247 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-(* This file is the interface between the c-c algorithm and Coq *)
-
-open Evd
-open Proof_type
-open Names
-open Libnames
-open Nameops
-open Inductiveops
-open Declarations
-open Term
-open Termops
-open Tacmach
-open Tactics
-open Tacticals
-open Ccalgo
-open Tacinterp
-open Ccproof
-open Pp
-open Util
-open Format
-
-exception Not_an_eq
-
-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 eq_rect_theo = constant ["Init";"Logic"] "eq_rect"
-
-(* decompose member of equality in an applicative format *)
-
-let rec decompose_term env t=
-  match kind_of_term t with
-      App (f,args)->
-	let tf=decompose_term env f in
-	let targs=Array.map (decompose_term env) args in
-	  Array.fold_left (fun s t->Appli (s,t)) tf targs
-    | Construct c->
-	let (_,oib)=Global.lookup_inductive (fst c) in
-	let nargs=mis_constructor_nargs_env env c in
-	  Constructor (c,nargs,nargs-oib.mind_nparams)
-    | _ ->(Symb t)
-	
-(* decompose equality in members and type *)
-	
-let rec eq_type_of_term term=
-  match kind_of_term term with
-      App (f,args)->
-	(try 
-	   let ref = reference_of_constr f in
-	     if ref=Coqlib.glob_eq && (Array.length args)=3 
-	     then (true,args.(0),args.(1),args.(2)) 
-	     else 
-	       if ref=(Lazy.force Coqlib.coq_not_ref) && 
-		 (Array.length args)=1 then
-		   let (pol,t,a,b)=eq_type_of_term args.(0) in
-		     if pol then (false,t,a,b) else fail ()
-	       else fail ()
-	 with Not_found -> fail ())
-    | Prod (_,eq,ff) ->
-	(try 
-	   let ref = reference_of_constr ff in
-	     if ref=(Lazy.force Coqlib.coq_False_ref) then
-	       let (pol,t,a,b)=eq_type_of_term eq in
-		 if pol then (false,t,a,b) else fail ()
-	     else fail ()
-	 with Not_found -> fail ())
-    | _ -> fail ()
-	
-(* read an equality *)
-	  
-let read_eq env term=
-  let (pol,_,t1,t2)=eq_type_of_term term in 
-    (pol,(decompose_term env t1,decompose_term env t2))
-
-(* rebuild a term from applicative format *)
-    
-let rec make_term=function
-    Symb s->s
-  | Constructor(c,_,_)->mkConstruct c 
-  | Appli (s1,s2)->
-      make_app [(make_term s2)] s1
-and make_app l=function
-    Symb s->applistc s l
-  | Constructor(c,_,_)->applistc (mkConstruct c) l
-  | Appli (s1,s2)->make_app ((make_term s2)::l) s1
-
-(* store all equalities from the context *)
-	
-let rec read_hyps env=function
-    []->[],[]
-  | (id,_,e)::hyps->let eq,diseq=read_hyps env hyps in
-      try let pol,cpl=read_eq env e in
-	if pol then 
-	  ((id,cpl)::eq),diseq 
-	else 
-	  eq,((id,cpl)::diseq)
-      with Not_an_eq -> eq,diseq
-
-(* build a problem ( i.e. read the goal as an equality ) *)
-	
-let make_prb gl=
-  let env=pf_env gl in
-  let eq,diseq=read_hyps env gl.it.evar_hyps in
-    try
-      let pol,cpl=read_eq env gl.it.evar_concl in
-	if pol then (eq,diseq,Some cpl) else assert false with 
-	    Not_an_eq -> (eq,diseq,None)
-
-(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
-
-let build_projection intype outtype (cstr:constructor) special default gls=
-  let env=pf_env gls in 
-  let (h,argv) = 
-    try destApp intype with 
-	Invalid_argument _ -> (intype,[||])  in
-  let ind=destInd h in 
-  let types=Inductiveops.arities_of_constructors env ind in
-  let lp=Array.length types in
-  let ci=(snd cstr)-1 in
-  let branch i=
-    let ti=Term.prod_appvect types.(i) argv in
-    let rc=fst (Sign.decompose_prod_assum ti) in
-    let head=
-      if i=ci then special else default in  
-      Sign.it_mkLambda_or_LetIn head rc in
-  let branches=Array.init lp branch in
-  let casee=mkRel 1 in
-  let pred=mkLambda(Anonymous,intype,outtype) in
-  let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
-  let body= mkCase(case_info, pred, casee, branches) in
-  let id=pf_get_new_id (id_of_string "t") gls in     
-    mkLambda(Name id,intype,body)
-  
-(* generate an adhoc tactic following the proof tree  *)
-
-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 axioms p1);(proof_tac axioms p2)])
-  | Congr (p1,p2)->
-      fun gls->
-	let (f1,f2)=(type_proof axioms p1) 
-	and (x1,x2)=(type_proof axioms p2) in
-        let tf1=make_term f1 and tx1=make_term x1 
-	and tf2=make_term f2 and tx2=make_term x2 in
-	let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1
-	and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in
-	let id=pf_get_new_id (id_of_string "f") gls in
-	let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1=
-	  mkApp(Lazy.force f_equal_theo,[|typf;typfx;appx1;tf1;tf2|])
-	and lemma2=
-	  mkApp(Lazy.force f_equal_theo,[|typx;typfx;tf2;tx1;tx2|]) in
-	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
-	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
-  	      tclFIRST
-		[tclTHEN (apply lemma2) (proof_tac axioms p2);
-		 reflexivity;
-		 fun gls ->
-		   errorlabstrm  "Congruence" 
-		   (Pp.str 
-		      "I don't know how to handle dependent equality")]]
-	     gls)
-  | Inject (prf,cstr,nargs,argind)  as gprf->
-      (fun gls ->
-	 let ti,tj=type_proof axioms prf in
-	 let ai,aj=type_proof axioms gprf in
-	 let cti=make_term ti in
-	 let ctj=make_term tj in
-	 let cai=make_term ai in
-	 let intype=pf_type_of gls cti in
-	 let outtype=pf_type_of gls cai in
-	 let special=mkRel (1+nargs-argind) in
-	 let default=make_term ai in
-	 let proj=build_projection intype outtype cstr special default gls in
-	 let injt=
-	   mkApp (Lazy.force f_equal_theo,[|intype;outtype;proj;cti;ctj|]) in 
-	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
-
-let refute_tac axioms disaxioms id p gls =      
-  let t1,t2=List.assoc id disaxioms in
-  let tt1=make_term t1 and tt2=make_term t2 in
-  let intype=pf_type_of gls tt1 in
-  let neweq=
-    mkApp(constr_of_global Coqlib.glob_eq,
-	  [|intype;tt1;tt2|]) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in
-  let false_t=mkApp (mkVar id,[|mkVar hid|]) in
-    tclTHENS (true_cut (Name hid) neweq)
-      [proof_tac axioms p; simplest_elim false_t] gls
-
-let discriminate_tac axioms cstr p gls =
-  let t1,t2=type_proof axioms p in 
-  let tt1=make_term t1 and tt2=make_term t2 in
-  let intype=pf_type_of gls tt1 in
-  let concl=pf_concl gls in
-  let outsort=mkType (new_univ ()) in
-  let xid=pf_get_new_id (id_of_string "X") gls in
-  let tid=pf_get_new_id (id_of_string "t") gls in
-  let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
-  let trivial=pf_type_of gls identity in
-  let outtype=mkType (new_univ ()) in
-  let pred=mkLambda(Name xid,outtype,mkRel 1) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in     
-  let proj=build_projection intype outtype cstr trivial concl gls in
-  let injt=mkApp (Lazy.force f_equal_theo,
-		  [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
-  let endt=mkApp (Lazy.force eq_rect_theo,
-		  [|outtype;trivial;pred;identity;concl;injt|]) in
-  let neweq=mkApp(constr_of_global Coqlib.glob_eq,[|intype;tt1;tt2|]) in
-    tclTHENS (true_cut (Name hid) neweq) 
-      [proof_tac axioms p;exact_check endt] gls
-      
-(* wrap everything *)
-	
-let cc_tactic gls=
-  Coqlib.check_required_library ["Coq";"Init";"Logic"];
-  let (axioms,disaxioms,glo)=make_prb gls in
-    match (cc_proof axioms disaxioms glo) with
-        `Prove_goal p -> proof_tac axioms p gls
-      | `Refute_hyp (id,p) -> refute_tac axioms disaxioms id p gls
-      | `Discriminate (cstr,p) -> discriminate_tac axioms cstr p gls
-
-(* Tactic registration *)
-      
-TACTIC EXTEND CC
- [ "Congruence" ] -> [ tclSOLVE [tclTHEN (tclREPEAT introf) cc_tactic] ]
-END
-   
diff --git a/contrib/cc/CCSolve.v b/contrib/cc/cctac.mli
index 93770c992..0622ca37a 100644
--- a/contrib/cc/CCSolve.v
+++ b/contrib/cc/cctac.mli
@@ -8,15 +8,9 @@
 
 (* $Id$ *)
 
-Ltac CCsolve :=
-  repeat
-   match goal with
-   | H:?X1 |- ?X2 =>
-       let Heq := fresh "Heq" in
-       (assert (Heq : X2 = X1); [ congruence | rewrite Heq; exact H ])
-   | H:?X1,G:(?X2 -> ?X3) |- _ =>
-       let Heq := fresh "Heq" in
-       (assert (Heq : X2 = X1);
-         [ congruence
-         | rewrite Heq in G; generalize (G H); clear G; intro G ])
-   end.  
+open Term 
+open Proof_type
+
+val cc_tactic : constr list -> tactic
+
+val cc_fail : tactic
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4
new file mode 100644
index 000000000..33811b3d9
--- /dev/null
+++ b/contrib/cc/g_congruence.ml4
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \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 Cctac
+open Tactics
+open Tacticals
+
+(* Tactic registration *)
+      
+TACTIC EXTEND CC
+ [ "Congruence" ] -> [ tclORELSE 
+			 (tclTHEN (tclREPEAT introf) (cc_tactic [])) 
+			 cc_fail ]
+END
+      
+TACTIC EXTEND CCwith
+ [ "Congruence" "with" ne_constr_list(l) ] -> [ tclORELSE 
+			 (tclTHEN (tclREPEAT introf) (cc_tactic l)) 
+			 cc_fail]
+END