Code simplification in CC

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

5 files changed, 251 insertions, 241 deletions

diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index 93b60531b..2dc2216a5 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -16,104 +16,158 @@ open Term
 
 let init_size=251
   
-type term=Symb of constr|Appli of term*term
+type term=
+    Symb of constr
+  | Appli of term*term
 
+type rule=
+    Congruence
+  | Axiom of identifier
+
+type valid={lhs:int;rhs:int;rule:rule}
+
+let congr_valid i j= {lhs=i;rhs=j;rule=Congruence}
+
+let ax_valid i j id= {lhs=i;rhs=j;rule=Axiom id}
 
 (* Basic Union-Find algo w/o path compression *)
     
 module UF = struct
-  type tag=Congr|Ax of identifier
-      
-  type cl=Rep of int*(int list)|Eqto of int*(int*int*tag)
+
+  type cl=Rep of int*(int list)|Eqto of int*valid
 
   type vertex=Leaf|Node of (int*int) 
 
-  type t=(int ref)*((int,(cl*vertex*term)) Hashtbl.t)
+  type node={clas:cl;vertex:vertex;term:term}    
+
+  type t={mutable size:int;
+	  map:(int,node) Hashtbl.t;
+	  syms:(term,int) Hashtbl.t}
 	
-  let empty ()=(((ref 0),(Hashtbl.create init_size)):t)
-   	   
-  let add_lst i t ((a,m):t)=
-    match Hashtbl.find m i with
-      ((Rep(l,lst)),v,trm)->Hashtbl.replace m i ((Rep((l+1),(t::lst))),v,trm)
-    | _ ->failwith "add_lst: not a representative"
-	  
-  let rec find ((a,m):t) i=
-    let (cl,_,_)=Hashtbl.find m i in
-    match cl with
-      Rep(_,_) -> i
-    | Eqto(j,_) ->find (a,m) j
-	  
-  let list ((a,m):t) i=
-    match Hashtbl.find m i with
-      ((Rep(_,lst)),_,_)-> lst
-    | _ ->failwith "list: not a class"
+  let empty ():t={size=0;
+		  map=Hashtbl.create init_size;
+		  syms=Hashtbl.create init_size}
+
+  let add_lst i t uf=
+    let node=Hashtbl.find uf.map i in
+      match node.clas with
+	  Rep(l,lst)->Hashtbl.replace uf.map i 
+	    {node with clas=Rep(l+1,t::lst)}
+	| _ ->failwith "add_lst: not a representative"
+	    
+  let rec find uf i=
+    match (Hashtbl.find uf.map i).clas with
+	Rep(_,_) -> i
+      | Eqto(j,_) ->find uf j
 	  
-  let size ((a,m):t) i=
-    match Hashtbl.find m i with
-      ((Rep (l,_)),_,_) -> l
-    | _ ->failwith "size: not a class"
+  let list uf i=
+    match (Hashtbl.find uf.map i).clas with
+	Rep(_,lst)-> lst
+      | _ ->failwith "list: not a class"
 	  
-  let signature ((a,m):t) i=
-    let (_,v,_)=Hashtbl.find m i in
-    match v with
-      Node(j,k)->(find (a,m) j,find (a,m) k)
-    | _ ->failwith "signature: not a node"
-
-  let nodes ((a,m):t)=  (* cherche les noeuds binaires *)
-    Hashtbl.fold (fun i (_,v,_) l->match v with Node (_,_)->i::l|_->l) m [] 
-
-  let rec add t (a,m) syms = 
-    try Hashtbl.find syms t with Not_found ->
-	match t with
-	  Symb s -> 
-	    let b= !a in incr a;
-	    Hashtbl.add m b ((Rep (0,[])),Leaf,t);
-	    Hashtbl.add syms t b;
-	    b
-	| Appli (t1,t2) -> 
-	    let i1=add t1 (a,m) syms and i2=add t2 (a,m) syms in
-	    let b= !a in incr a;
-	    add_lst (find (a,m) i1) b (a,m);
-            add_lst (find (a,m) i2) b (a,m);
-	    Hashtbl.add m b ((Rep (0,[])),(Node(i1,i2)),t);
-	    Hashtbl.add syms t b;
+  let size uf i=
+    match (Hashtbl.find uf.map i).clas with
+	Rep (l,_) -> l
+      | _ ->failwith "size: not a class"
+
+  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)
+      | _ -> failwith "subterms: not a node"
+
+  let signature uf i=
+    match (Hashtbl.find uf.map i).vertex with
+	Node(j,k)->(find uf j,find uf k)
+      | _ ->failwith "signature: not a node"
+
+  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 rec add t uf= 
+    try Hashtbl.find uf.syms t with 
+	Not_found ->
+	  let b=next uf in
+	  let new_node=
+	    match t with
+		Symb s -> 
+		  {clas=Rep (0,[]);
+		   vertex=Leaf;
+		   term=t}
+	      | Appli (t1,t2) -> 
+		  let i1=add t1 uf 
+		  and i2=add t2 uf in
+		    add_lst (find uf i1) b uf;
+		    add_lst (find uf i2) b uf;
+		    {clas=Rep (0,[]);
+		     vertex=Node(i1,i2);
+		     term=t}
+      in
+	    Hashtbl.add uf.map b new_node;
+	    Hashtbl.add uf.syms t b;
 	    b
 	      
-  let union ((a,m):t) i1 i2 t=
-    let (cl1,v1,t1)=(Hashtbl.find m i1) and 
-	(cl2,v2,t2)=(Hashtbl.find m i2) in
-    match cl1,cl1 with
-      ((Rep (l1,lst1)),(Rep (l2,lst2))) -> 
-	Hashtbl.replace m i2 ((Eqto (i1,t)),v2,t2);
-	Hashtbl.replace m i1 ((Rep((l2+l1),(lst2@lst1))),v1,t1)
-    | _ ->failwith "union: not classes"
-	  
-	  
+  let union uf i1 i2 t=
+    let node1=(Hashtbl.find uf.map i1) 
+    and node2=(Hashtbl.find uf.map i2) in
+      match node1.clas,node2.clas with
+	  Rep (l1,lst1),Rep (l2,lst2) -> 
+	    Hashtbl.replace uf.map i2 {node2 with clas=Eqto (i1,t)};
+	    Hashtbl.replace uf.map i1 
+	      {node1 with clas=Rep(l2+l1,lst2@lst1)}
+	| _ ->failwith "union: not classes"	  	  
+	    
+  let rec up_path uf i l=
+    match (Hashtbl.find uf.map i).clas with
+	Eqto(j,t)->up_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 join_path uf i j=
+    assert (find uf i=find uf j);
+    min_path (up_path uf i [],up_path uf j [])
+      
 end    
     
 (* Signature table *)
 
 module ST=struct
   
-(* l: sign -> term r: term -> sign *)
+  (* l: sign -> term r: term -> sign *)
 	
-  type t = ((int*int,int) Hashtbl.t) * ((int,int*int) Hashtbl.t)
+  type t = {toterm:(int*int,int) Hashtbl.t;
+	    tosign:(int,int*int) Hashtbl.t}
 	
-  let empty ()=((Hashtbl.create init_size),(Hashtbl.create init_size))
+  let empty ()=
+    {toterm=Hashtbl.create init_size;
+     tosign=Hashtbl.create init_size}
       
-  let enter t sign ((l,r) as st:t)=
-    if Hashtbl.mem l sign then 
+  let enter t sign st=
+    if Hashtbl.mem st.toterm sign then 
 	failwith "enter: signature already entered"
     else 
-	Hashtbl.replace l sign t;
-	Hashtbl.replace r t sign
+	Hashtbl.replace st.toterm sign t;
+	Hashtbl.replace st.tosign t sign
 	  
-  let query sign ((l,r):t)=Hashtbl.find l sign
+  let query sign st=Hashtbl.find st.toterm sign
 	  
-  let delete t ((l,r) as st:t)=
-    try let sign=Hashtbl.find r t in
-	Hashtbl.remove l sign;
-	Hashtbl.remove r t
+  let delete t st=
+    try let sign=Hashtbl.find st.tosign t in
+	Hashtbl.remove st.toterm sign;
+	Hashtbl.remove st.tosign t
     with
 	Not_found -> ()
 
@@ -139,17 +193,17 @@ let rec process_rec uf st=function
       let pending=process_rec uf st combine in
       let i=UF.find uf v 
       and j=UF.find uf w in
-      if (i==j)|| ((Hashtbl.hash i)=(Hashtbl.hash j) && (i=j)) then 
+      if i=j then 
 	pending 
       else
 	if (UF.size uf i)<(UF.size uf j) then
 	  let l=UF.list uf i in
-	  UF.union uf j i (v,w,UF.Congr);
+	  UF.union uf j i (congr_valid v w);
 	  ST.delete_list l st;
 	  l@pending
 	else
 	  let l=UF.list uf j in
-	  UF.union uf i j (w,v,UF.Congr);
+	  UF.union uf i j (congr_valid w v);
 	  ST.delete_list l st;
 	  l@pending
 	  
@@ -162,22 +216,15 @@ let rec cc_rec uf st=function
 	
 let cc uf=(cc_rec uf (ST.empty ()) (UF.nodes uf))
 
-let rec make_uf syms=function
+let rec make_uf=function
     []->(UF.empty ())
   | (ax,(v,w))::q->
-      let uf=make_uf syms q in
-      let i1=UF.add v uf syms in
-      let i2=UF.add w uf syms in
-      UF.union uf (UF.find uf i2) (UF.find uf i1) (i1,i2,(UF.Ax ax));
+      let uf=make_uf q in
+      let i1=UF.add v uf in
+      let i2=UF.add w uf in
+      UF.union uf (UF.find uf i2) (UF.find uf i1) (ax_valid i1 i2 ax);
       uf
 	
-let decide_prb (axioms,(v,w))=
-  let syms=Hashtbl.create init_size in
-  let uf=make_uf syms axioms in
-  let i1=UF.add v uf syms in
-  let i2=UF.add w uf syms in
-  cc uf;
-  (UF.find uf i1)=(UF.find uf i2)
 
 
 
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 6f55d8541..582df715f 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -10,58 +10,52 @@
 
 val init_size : int
 
-type term = Symb of Term.constr | Appli of term * term
+type term = 
+    Symb of Term.constr 
+  | Appli of term * term 
 
-module UF :
-  sig
-    type tag = Congr | Ax of Names.identifier
-    and cl =
-        Rep of int * int list
-      | Eqto of int * (int * int * tag)
-    and vertex = Leaf | Node of (int * int)
-    and t = int ref * (int, cl * vertex * term) Hashtbl.t
-    val empty : unit -> t
-    val add_lst : int -> int -> t -> unit
-    val find : t -> int -> int
-    val list : t -> int -> int list
-    val size : t -> int -> int
-    val signature : t -> int -> int * int
-    val nodes : t -> int list
-    val add :
-      term ->
-      int ref * (int, cl * vertex * term) Hashtbl.t ->
-      (term, int) Hashtbl.t -> int
-    val union :
-      t -> int -> int -> int * int * tag -> unit
-  end
-
-module ST :
-  sig
-    type t =
-      (int * int, int) Hashtbl.t *
-      (int, int * int) Hashtbl.t
-    val empty :
-      unit -> ('a, 'b) Hashtbl.t * ('c, 'd) Hashtbl.t
-    val enter : int -> int * int -> t -> unit
-    val query : int * int -> t -> int
-    val delete : int -> t -> unit
-    val delete_list : int list -> t -> unit
-  end
+type rule = 
+    Congruence 
+  | Axiom of Names.identifier      
 
-val combine_rec :
-  UF.t -> ST.t -> int list -> (int * int) list
+type valid =
+    {lhs : int; 
+     rhs : int; 
+     rule : rule}
 
-val process_rec :
-  UF.t -> ST.t -> (int * int) list -> int list
+module UF :
+sig
+  type t 
+  val empty : unit -> t
+  val add_lst : int -> int -> t -> unit
+  val find : t -> int -> int
+  val list : t -> int -> int list
+  val size : t -> int -> int
+  val term : t -> int -> term    
+  val subterms : t -> int -> int * int
+  val signature : t -> int -> int * int
+  val nodes : t -> int list
+  val add : term -> t -> int
+  val union : t -> int -> int -> valid -> unit
+  val join_path : t -> int -> int -> 
+    ((int*int)*valid) list*
+    ((int*int)*valid) list
+end
+
+  
+module ST :
+sig
+  type t
+  val empty : unit -> t
+  val enter : int -> int * int -> t -> unit
+  val query : int * int -> t -> int
+  val delete : int -> t -> unit
+  val delete_list : int list -> t -> unit
+end
 
-val cc_rec : UF.t -> ST.t -> int list -> unit
 
 val cc : UF.t -> unit
 
 val make_uf :
-  (term, int) Hashtbl.t ->
   (Names.identifier * (term * term)) list -> UF.t
 
-val decide_prb :
-  (Names.identifier * (term * term)) list * (term * term) ->
-  bool
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 26e229917..f3c86d9c5 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -20,95 +20,81 @@ type proof=
   | Trans of proof*proof
   | Sym of proof
   | Congr of proof*proof
-	
-let rec up_path uf i l=
-  let (cl,_,_)=(Hashtbl.find uf i) in
-  match cl with 
-    UF.Eqto(j,t)->up_path uf j (((i,j),t)::l)
-  | UF.Rep(_,_)->l
-	
-let rec min_path=function 
-    ([],l2)->([],l2)
-  | (l1,[])->(l1,[])
-  | (((c1,t1)::q1),((c2,t2)::q2)) as cpl->
-      if c1=c2 then 
-	min_path (q1,q2) 
-      else 
-	cpl
-	  
+		  
 let pcongr=function
-    ((Refl t1),(Refl t2))->Refl (Appli (t1,t2))
-  | (p1,p2) -> Congr (p1,p2)
+    Refl t1, Refl t2 ->Refl (Appli (t1,t2))
+  | p1, p2 -> Congr (p1,p2)
 
 let rec ptrans=function
-    ((Refl _),p)->p
-  | (p,(Refl _))->p
-  | (Trans(p1,p2),p3)->ptrans(p1,ptrans (p2,p3))
-  | (Congr(p1,p2),Congr(p3,p4))->pcongr(ptrans(p1,p3),ptrans(p2,p4))
-  | (Congr(p1,p2),Trans(Congr(p3,p4),p5))->
-	ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5)
-  | (p1,p2)->Trans (p1,p2)
+    Refl _, p ->p
+  | p, Refl _ ->p
+  | Trans(p1,p2), p3 ->ptrans(p1,ptrans (p2,p3))
+  | Congr(p1,p2), Congr(p3,p4) ->pcongr(ptrans(p1,p3),ptrans(p2,p4))
+  | Congr(p1,p2), Trans(Congr(p3,p4),p5) ->
+      ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5)
+  | p1, p2 ->Trans (p1,p2)
 	
 let rec psym=function
     Refl p->Refl p
   | Sym p->p
   | Ax s-> Sym(Ax s)
-  | Trans (p1,p2)-> ptrans ((psym p2),(psym p1))
-  | Congr (p1,p2)-> pcongr ((psym p1),(psym p2))
+  | Trans (p1,p2)-> ptrans (psym p2,psym p1)
+  | Congr (p1,p2)-> pcongr (psym p1,psym p2)
 	
 let pcongr=function
-    ((Refl t1),(Refl t2))->Refl (Appli (t1,t2))
-  | (p1,p2) -> Congr (p1,p2)
+    Refl t1, Refl t2 ->Refl (Appli (t1,t2))
+  | p1, p2 -> Congr (p1,p2)
 	
-let build_proof ((a,m):UF.t) i j=
+let build_proof uf i j=
+  
   let rec equal_proof i j=
-    let (li,lj)=min_path ((up_path m i []),(up_path m j [])) in
-    ptrans ((path_proof i li),(psym (path_proof j lj)))
-  and arrow_proof ((i,j),t)=
-    let (i0,j0,t0)=t in
-    let pi=(equal_proof i i0) in
-    let pj=psym (equal_proof j j0) in
+    let (li,lj)=UF.join_path uf i j in
+      ptrans (path_proof i li,psym (path_proof j lj))
+  
+  and edge_proof ((i,j),t)=
+    let pi=equal_proof i t.lhs in
+    let pj=psym (equal_proof j t.rhs) in
     let pij=
-      match t0 with 
-	UF.Ax s->Ax s
-      | UF.Congr->(congr_proof i0 j0)	
+      match t.rule with 
+	  Axiom s->Ax s
+	| Congruence->congr_proof t.lhs t.rhs
     in  ptrans(ptrans (pi,pij),pj)
+  
   and path_proof i=function
-      []->let (_,_,t)=Hashtbl.find m i in Refl t
-    | (((_,j),_) as x)::q->ptrans ((path_proof j q),(arrow_proof x))
+      [] -> let t=UF.term uf i in Refl t
+    | x::q->ptrans (path_proof j q,edge_proof x)
+  
   and congr_proof i j=
-    let (_,vi,_)=(Hashtbl.find m i) and (_,vj,_)=(Hashtbl.find m j) in   
-    match (vi,vj) with
-      ((UF.Node(i1,i2)),(UF.Node(j1,j2)))->
-	pcongr ((equal_proof i1 j1),(equal_proof i2 j2))
-    | _ -> failwith "congr_proof: couldn't find subterms"
+    let (i1,i2) = UF.subterms uf i
+    and (j1,j2) = UF.subterms uf j in   
+      pcongr (equal_proof i1 j1, equal_proof i2 j2)
+  
   in
-  (equal_proof i j)
-    
-let rec type_proof uf axioms p=
+    equal_proof i j
+
+let rec type_proof axioms p=
   match p with
     Ax s->List.assoc s axioms
-  | Refl t->(t,t)
+  | Refl t-> t,t
   | Trans (p1,p2)->
-      let (s1,t1)=type_proof uf axioms p1 
-      and (t2,s2)=type_proof uf axioms p2 in
+      let (s1,t1)=type_proof axioms p1 
+      and (t2,s2)=type_proof axioms p2 in
       if t1=t2 then (s1,s2) else failwith "invalid transitivity"
-  | Sym p->let (t1,t2)=type_proof uf axioms p in (t2,t1)
+  | Sym p->let (t1,t2)=type_proof axioms p in (t2,t1)
   | Congr (p1,p2)->
-      let (i1,j1)=(type_proof uf axioms p1)
-      and (i2,j2)=(type_proof uf axioms p2) in
-      ((Appli (i1,i2)),(Appli (j1,j2)))
+      let (i1,j1)=type_proof axioms p1
+      and (i2,j2)=type_proof axioms p2 in
+      Appli (i1,i2),Appli (j1,j2)
 	
 let cc_proof (axioms,(v,w))=
-  let syms=Hashtbl.create init_size in
-  let uf=make_uf syms axioms in
-  let i1=(UF.add v uf syms) in
-  let i2=(UF.add w uf syms) in
+  let uf=make_uf axioms in
+  let i1=UF.add v uf in
+  let i2=UF.add w uf in
   cc uf;
-  if (UF.find uf i1)=(UF.find uf i2) then 
-    let p=(build_proof uf i1 i2) in
-    (if (v,w)=(type_proof uf axioms p) then Some (p,uf,axioms) 
-    else failwith "Proof check failed !!")
+  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 failwith "Proof check failed !!"
   else
     None;;
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index a699af694..2dcb01e14 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -17,16 +17,6 @@ type proof =
   | Sym of proof
   | Congr of proof * proof
 
-val up_path :
-  (int, UF.cl * 'a * 'b) Hashtbl.t ->
-  int ->
-  ((int * int) * (int * int * UF.tag)) list ->
-  ((int * int) * (int * int * UF.tag)) list
-
-val min_path :
-  ('a * 'b) list * ('a * 'c) list ->
-  ('a * 'b) list * ('a * 'c) list
-
 val pcongr : proof * proof -> proof
 val ptrans : proof * proof -> proof
 val psym : proof -> proof
@@ -35,14 +25,9 @@ val pcongr : proof * proof -> proof
 val build_proof : UF.t -> int -> int -> proof
 
 val type_proof :
-  'a ->
-  (Names.identifier * (term * term)) list ->
-  proof -> term * term
+  (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) ->
+  (proof * UF.t * (Names.identifier * (term * term)) list) option
 
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 420d0e4db..247bac99a 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -32,7 +32,6 @@ exception Not_an_eq
 
 let fail()=raise Not_an_eq
     
-
 let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
 let eq2eqT_theo = constant ["Logic";"Eqdep_dec"] "eq2eqT"
@@ -48,9 +47,10 @@ let t_make_app=(Array.fold_left (fun s t->Appli (s,t)))
 
 let rec decompose_term t=
   match kind_of_term t with
-    App (f,args)->let targs=Array.map decompose_term args in
-    (t_make_app (Symb f) targs)
-  | _->(Symb t)
+    App (f,args)->
+      let targs=Array.map decompose_term args in
+	(t_make_app (Symb f) targs)
+  | _ ->(Symb t)
 
 (* decompose equality in members and type *)
 	
@@ -59,8 +59,7 @@ let eq_type_of_term term=
       App (f,args)->
 	(try 
 	   let ref = reference_of_constr f in
-	     if (ref=Coqlib.glob_eq || ref=Coqlib.glob_eqT) && 
-	       (Array.length args)=3 
+	     if ref=Coqlib.glob_eq && (Array.length args)=3 
 	     then (args.(0),args.(1),args.(2)) 
 	     else fail()
 	 with
@@ -79,7 +78,7 @@ let rec make_term=function
     Symb s->s
   | Appli (s1,s2)->make_app [(make_term s2)] s1
 and make_app l=function
-    Symb s->mkApp (s,(Array.of_list l))
+    Symb s->applistc s l
   | Appli (s1,s2)->make_app ((make_term s2)::l) s1
 
 (* store all equalities from the context *)
@@ -96,24 +95,19 @@ let make_prb gl=
   let hyps=gl.evar_hyps in
   (read_hyps hyps),(read_eq concl)
 
-(* apply tac, followed (or not) by aplication of theorem theo *)
-
-let st_wrap theo tac= 
-  tclORELSE tac (tclTHEN (apply theo) tac)
-
 (* generate an adhoc tactic following the proof tree  *)
 
 let rec proof_tac uf axioms=function
-    Ax id->(fun gl->(st_wrap (Lazy.force eq2eqT_theo) (exact_check (mkVar id)) gl))
+    Ax id->exact_check (mkVar id)
   | Refl t->reflexivity
-  | Trans (p1,p2)->let t=(make_term (snd (type_proof uf axioms p1))) in
+  | 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)])
   | Sym p->tclTHEN symmetry (proof_tac uf axioms p)
   | Congr (p1,p2)->
       (fun gl->
-	 let (s1,t1)=(type_proof uf axioms p1) and
-	   (s2,t2)=(type_proof uf axioms p2) in
+	 let (s1,t1)=(type_proof axioms p1) and
+	   (s2,t2)=(type_proof axioms p2) in
          let ts1=(make_term s1) and tt1=(make_term t1) 
 	and ts2=(make_term s2) and tt2=(make_term t2) in
       let typ1=pf_type_of gl ts1 and typ2=pf_type_of gl ts2 in
@@ -125,23 +119,27 @@ let rec proof_tac uf axioms=function
 	   [(proof_tac uf axioms p1);(proof_tac uf axioms p2)])		
 	   (tclTHEN
 	      (let p=mkLambda(destProd typ1) in
-	      let acdt=mkApp((Lazy.force congr_dep_theo),[|typ2;p;ts1;tt1;ts2|]) in 
+	      let acdt=mkApp((Lazy.force congr_dep_theo),
+			     [|typ2;p;ts1;tt1;ts2|]) in 
 	      apply acdt) (proof_tac uf axioms p1))
 	gl)
 
 (* wrap everything *)
 	
-let cc_tactic gl_sg=
+let cc_tactic gls=
   Library.check_required_library ["Coq";"cc";"CC"];
-  let gl=gl_sg.it in
-  let prb=try make_prb gl with Not_an_eq ->
-    errorlabstrm  "CC" [< str "Couldn't match goal with an equality" >] in
-  match (cc_proof prb) with
-    None->errorlabstrm  "CC" [< str "CC couldn't solve goal" >] 
-  | Some (p,uf,axioms)->let tac=proof_tac uf axioms p in
-    (tclORELSE (st_wrap (Lazy.force eqT2eq_theo) tac)
-       (fun _->errorlabstrm  "CC" 
-	  [< str "CC doesn't know how to handle dependent equality." >]) gl_sg)
+  let prb=
+    try make_prb gls.it with 
+	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)->
+	  tclORELSE (proof_tac uf axioms p)
+	  (fun _->errorlabstrm  "CC" 
+	     [< str "CC doesn't know how to handle dependent equality." >]) 
+	  gls
 
 (* Tactic registration *)