Imported Upstream snapshot 8.3~beta0+13298

8 files changed, 0 insertions, 1826 deletions

diff --git a/contrib/cc/README b/contrib/cc/README
deleted file mode 100644
index 073b140e..00000000
--- a/contrib/cc/README
+++ /dev/null
@@ -1,20 +0,0 @@
-
-cctac: congruence-closure for coq
-
-author: Pierre Corbineau, 
-	Stage de DEA au LSV, ENS Cachan
-	Thèse au LRI, Université Paris Sud XI 
-
-Files :
-
-- ccalgo.ml : congruence closure algorithm
-- ccproof.ml : proof generation code
-- cctac.ml4 : the tactic itself
-- CCSolve.v : a small Ltac tactic based on congruence 
-
-Known Bugs : the congruence tactic can fail due to type dependencies.
-
-Related documents:
-	Peter J. Downey, Ravi Sethi, and Robert E. Tarjan.
-	Variations on the common subexpression problem.
-	JACM, 27(4):758-771, October 1980.	
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
deleted file mode 100644
index e67797e4..00000000
--- a/contrib/cc/ccalgo.ml
+++ /dev/null
@@ -1,884 +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        *)
-(************************************************************************)
-
-(* $Id: ccalgo.ml 10579 2008-02-21 13:54:00Z corbinea $ *)
-
-(* This file implements the basic congruence-closure algorithm by *)
-(* Downey,Sethi and Tarjan. *)
-
-open Util
-open Pp
-open Goptions
-open Names
-open Term
-open Tacmach
-open Evd
-open Proof_type
-
-let init_size=5
-
-let cc_verbose=ref false 
-
-let debug f x = 
-  if !cc_verbose then f x
-
-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 *)
-
-module ST=struct
-  
-  (* l: sign -> term r: term -> sign *)
-	
-  type t = {toterm:(int*int,int) Hashtbl.t;
-	    tosign:(int,int*int) Hashtbl.t}
-	
-  let empty ()=
-    {toterm=Hashtbl.create init_size;
-     tosign=Hashtbl.create init_size}
-      
-  let enter t sign st=
-    if Hashtbl.mem st.toterm sign then 
-	anomaly "enter: signature already entered"
-    else 
-	Hashtbl.replace st.toterm sign t;
-	Hashtbl.replace st.tosign t sign
-	  
-  let query sign st=Hashtbl.find st.toterm sign
-
-  let rev_query term st=Hashtbl.find st.tosign term
-	  
-  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_set st s = Intset.iter (delete st) s
-	  
-end
-
-type pa_constructor=
-    { cnode : int;
-      arity : int;
-      args  : int list}
-
-type pa_fun=
-    {fsym:int;
-     fnargs:int}
-
-type pa_mark=
-    Fmark of pa_fun
-  | Cmark of pa_constructor
-
-module PacMap=Map.Make(struct 
-			 type t=pa_constructor 
-			 let compare=Pervasives.compare end) 
-
-module PafMap=Map.Make(struct 
-			 type t=pa_fun
-			 let compare=Pervasives.compare end)
-
-type cinfo=
-    {ci_constr: constructor; (* inductive type *)
-     ci_arity: int;     (* # args *)
-     ci_nhyps: int}     (* # projectable args *)
-
-type term=
-    Symb of constr
-  | Product of sorts_family * sorts_family
-  | Eps of identifier
-  | Appli of term*term
-  | Constructor of cinfo (* constructor arity + nhyps *)
-
-type ccpattern =
-    PApp of term * ccpattern list (* arguments are reversed *)
-  | PVar of int 
-
-type rule=
-    Congruence
-  | Axiom of constr * bool 
-  | Injection of int * pa_constructor * int * pa_constructor * int
-
-type from=
-    Goal
-  | Hyp of constr
-  | HeqG of constr
-  | HeqnH of constr * constr
-
-type 'a eq = {lhs:int;rhs:int;rule:'a}
-
-type equality = rule eq
-
-type disequality = from eq
-
-type patt_kind =
-    Normal 
-  | Trivial of types
-  | Creates_variables
-
-type quant_eq =
-    {qe_hyp_id: identifier;
-     qe_pol: bool;
-     qe_nvars:int;
-     qe_lhs: ccpattern;
-     qe_lhs_valid:patt_kind;
-     qe_rhs: ccpattern;
-     qe_rhs_valid:patt_kind}
-
-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 weight:int;
-     mutable lfathers:Intset.t;
-     mutable fathers:Intset.t;
-     mutable inductive_status: inductive_status;
-     class_type : Term.types;
-     mutable functions: Intset.t PafMap.t;
-     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: (constr,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_mark) Queue.t;
-     mutable diseq: disequality list;
-     mutable quant: quant_eq list;
-     mutable pa_classes: Intset.t;
-     q_history: (identifier,int array) Hashtbl.t;
-     mutable rew_depth:int;
-     mutable changed:bool;
-     by_type: (types,Intset.t) Hashtbl.t;
-     mutable gls:Proof_type.goal Tacmach.sigma}
-
-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 depth gls: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=[];
-  quant=[];
-  pa_classes=Intset.empty;
-  q_history=Hashtbl.create init_size;
-  rew_depth=depth;
-  by_type=Hashtbl.create init_size;
-  changed=false;
-  gls=gls}
-
-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).weight
-
-let axioms uf = uf.axioms
-
-let epsilons uf = uf.epsilons
-
-let add_lfather uf i t=
-  let r=get_representative uf i in
-    r.weight<-r.weight+1;
-    r.lfathers<-Intset.add t r.lfathers;
-    r.fathers <-Intset.add t r.fathers
-
-let add_rfather uf i t=
-  let r=get_representative uf i in
-    r.weight<-r.weight+1;
-    r.fathers <-Intset.add t r.fathers
-
-exception Discriminable of int * pa_constructor * int * pa_constructor 
-
-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 fsucc paf =
-  {paf with fnargs=succ paf.fnargs}
-    
-let add_pac rep pac t =
-  if not (PacMap.mem pac rep.constructors) then
-    rep.constructors<-PacMap.add pac t rep.constructors
-
-let add_paf rep paf t =
-  let already = 
-    try PafMap.find paf rep.functions with Not_found -> Intset.empty in
-    rep.functions<- PafMap.add paf (Intset.add t already) rep.functions
-
-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 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 typ =
-  {weight=0;
-   lfathers=Intset.empty;
-   fathers=Intset.empty;
-   inductive_status=Unknown;
-   class_type=typ;
-   functions=PafMap.empty;
-   constructors=PacMap.empty}
-    
-(* rebuild a constr from an applicative term *)
-    
-let _A_ = Name (id_of_string "A")
-let _B_ = Name (id_of_string "A")
-let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
-
-let cc_product s1 s2 = 
-  mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
-	   mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
-
-let rec constr_of_term = function
-    Symb s->s
-  | Product(s1,s2) -> cc_product s1 s2
-  | Eps id -> mkVar id
-  | Constructor cinfo -> mkConstruct cinfo.ci_constr 
-  | Appli (s1,s2)->
-      make_app [(constr_of_term s2)] s1
-and make_app l=function
-    Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1    
-  | other -> applistc (constr_of_term other) l 
-
-(* rebuild a term from a pattern and a substitution *)
-
-let build_subst uf subst =
-  Array.map (fun i -> 
-	       try term uf i 
-	       with _ -> anomaly "incomplete matching") subst
-
-let rec inst_pattern subst = function
-    PVar i -> 
-      subst.(pred i) 
-  | PApp (t, args) -> 
-      List.fold_right
-	(fun spat f -> Appli (f,inst_pattern subst spat))
-	   args t  
-
-let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
-
-let pr_term t = str "[" ++
-  Termops.print_constr (constr_of_term t) ++ str "]"
-
-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 typ = pf_type_of state.gls (constr_of_term t) in
-	  let new_node=
-	    match t with
-		Symb _ | Product (_,_) ->
-		  let paf =
-		    {fsym=b;
-		     fnargs=0} in
-		    Queue.add (b,Fmark paf) state.marks;
-		    {clas= Rep (new_representative typ);
-		     cpath= -1;
-		     vertex= Leaf;
-		     term= t}
-	      | Eps id -> 
-		  {clas= Rep (new_representative typ);
-		   cpath= -1;
-		   vertex= Leaf;
-		   term= t}
-	      | Appli (t1,t2) -> 
-		  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 typ);
-		     cpath= -1;
-		     vertex= Node(i1,i2);
-		     term= t}
-	      | Constructor cinfo ->
-		  let paf =
-		    {fsym=b;
-		     fnargs=0} in
-		    Queue.add (b,Fmark paf) state.marks;
-		  let pac =
-		    {cnode= b;
-		     arity= cinfo.ci_arity;
-		     args=[]} in
-		    Queue.add (b,Cmark pac) state.marks;
-		    {clas=Rep (new_representative typ);
-		     cpath= -1;
-		     vertex=Leaf;
-		     term=t}
-	  in
-	    uf.map.(b)<-new_node;
-	    Hashtbl.add uf.syms t b;
-	    Hashtbl.replace state.by_type typ 
-	      (Intset.add b 
-		 (try Hashtbl.find state.by_type typ with 
-		      Not_found -> Intset.empty));
-	    b
-
-let add_equality state c s t=
-  let i = add_term state s in
-  let j = add_term state t in
-    Queue.add {lhs=i;rhs=j;rule=Axiom(c,false)} state.combine;
-    Hashtbl.add state.uf.axioms c (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 add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
-  state.quant<-
-    {qe_hyp_id= id;
-     qe_pol= pol;
-     qe_nvars=nvars;
-     qe_lhs= patt1;
-     qe_lhs_valid=valid1;
-     qe_rhs= patt2;
-     qe_rhs_valid=valid2}::state.quant
-
-let is_redundant state id args =
-  try  
-    let norm_args = Array.map (find state.uf) args in
-    let prev_args = Hashtbl.find_all state.q_history id in
-    List.exists 
-      (fun old_args -> 
-	 Util.array_for_all2 (fun i j -> i = find state.uf j) 
-         norm_args old_args) 
-      prev_args
-    with Not_found -> false
-
-let add_inst state (inst,int_subst) = 
-  check_for_interrupt ();
-  if state.rew_depth > 0 then
-  if is_redundant state inst.qe_hyp_id int_subst then
-    debug msgnl (str "discarding redundant (dis)equality")
-  else   
-    begin
-      Hashtbl.add state.q_history inst.qe_hyp_id int_subst;
-      let subst = build_subst (forest state) int_subst in
-      let prfhead= mkVar inst.qe_hyp_id in
-      let args = Array.map constr_of_term subst in
-      let _ = array_rev args in (* highest deBruijn index first *)
-      let prf= mkApp(prfhead,args) in
-	  let s = inst_pattern subst inst.qe_lhs 
-	  and t = inst_pattern subst inst.qe_rhs in
-	    state.changed<-true;
-	    state.rew_depth<-pred state.rew_depth;
-	    if inst.qe_pol then
-	      begin
-		debug (fun () -> 
-		  msgnl 
-		   (str "Adding new equality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++ 
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
-		add_equality state prf s t
-	      end
-	    else
-	      begin
-		debug (fun () -> 
-		  msgnl 
-		   (str "Adding new disequality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++ 
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
-		add_disequality state (Hyp prf) s t 
-	      end
-  end
-
-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 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 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 (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++ 
-		 str " and " ++ pr_idx_term state i2 ++ str ".")) ();
-  let r1= get_representative state.uf i1 
-  and r2= get_representative state.uf i2 in
-    link state.uf i1 i2 eq;
-    Hashtbl.replace state.by_type r1.class_type 
-      (Intset.remove i1 
-	 (try Hashtbl.find state.by_type r1.class_type with 
-	      Not_found -> Intset.empty));
-    let f= Intset.union r1.fathers r2.fathers in
-      r2.weight<-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,Cmark pac) state.marks) 
-	r1.constructors;
-      PafMap.iter 
-	(fun paf -> Intset.iter 
-	   (fun b -> Queue.add (b,Fmark paf) state.marks)) 
-	r1.functions;
-      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 (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks    
-	| _,_ -> () 
-            
-let merge eq state = (* merge and no-merge *)
-  debug (fun () -> msgnl 
-    (str "Merging " ++ pr_idx_term state eq.lhs ++ 
-       str " and " ++ pr_idx_term state 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
-	union state j i (swap eq)
-
-let update t state = (* update 1 and 2 *)
-  debug (fun () -> msgnl 
-    (str "Updating term " ++ pr_idx_term state 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,Cmark (append_pac v pac)) state.marks) 
-      rep.constructors; 
-    PafMap.iter 
-      (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks) 
-      rep.functions; 
-    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_function_mark t rep paf state  =
-  add_paf rep paf t;
-  state.terms<-Intset.union rep.lfathers state.terms
-    
-let process_constructor_mark t i rep pac state =
-    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
-
-let process_mark t m state = 
-  debug (fun () -> msgnl 
-    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
-  let i=find state.uf t in
-  let rep=get_representative state.uf i in
-    match m with
-	Fmark paf -> process_function_mark t rep paf state
-      | Cmark pac -> process_constructor_mark t i rep pac state
-
-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 (fun () -> msg   
-	(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++ 
-	 pr_idx_term state dis.rhs ++ str " ... ")) ();  
-	if find uf dis.lhs=find uf dis.rhs then 
-	  begin debug msgnl (str "Yes");Some dis end 
-	else
-	  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;
-	true
-    with Queue.Empty -> 
-      try 
-	let (t,m) = Queue.take state.marks in
-	  process_mark t m state;
-	  true
-      with Queue.Empty ->
-	try
-	  let t = Intset.choose state.terms in
-	    state.terms<-Intset.remove t state.terms;
-	    update t state;
-	    true
-	with Not_found -> false
-
-let __eps__ = id_of_string "_eps_"  
-
-let new_state_var typ state =
-  let id = pf_get_new_id __eps__ state.gls in
-    state.gls<-
-      {state.gls with it =
-	  {state.gls.it with evar_hyps = 
-	      Environ.push_named_context_val (id,None,typ) 
-		state.gls.it.evar_hyps}};
-    id
-
-let complete_one_class state i=
-  match (get_representative state.uf i).inductive_status with
-      Partial pac ->
-	let rec app t typ n = 
-	  if n<=0 then t else
-	    let _,etyp,rest= destProd typ in
-	    let id = new_state_var etyp state in
-		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-	let _c = pf_type_of state.gls
-	  (constr_of_term (term state.uf pac.cnode)) in
-	let _args = 
-	  List.map (fun i -> constr_of_term (term state.uf  i)) 
-	    pac.args in
-	let typ = prod_applist _c (List.rev _args) in 
-	let ct = app (term state.uf i) typ pac.arity in
-	  state.uf.epsilons <- pac :: state.uf.epsilons; 
-	  ignore (add_term state ct)
-    | _ -> anomaly "wrong incomplete class" 
-
-let complete state =
-  Intset.iter (complete_one_class state) state.pa_classes
-
-type matching_problem = 
-{mp_subst : int array;
- mp_inst : quant_eq;
- mp_stack : (ccpattern*int) list }
-
-let make_fun_table state =
-  let uf= state.uf in
-  let funtab=ref PafMap.empty in
-  Array.iteri 
-    (fun i inode -> if i < uf.size then
-       match inode.clas with
-	   Rep rep ->
-	     PafMap.iter 
-	       (fun paf _ -> 
-		  let elem = 
-		    try PafMap.find paf !funtab 
-		    with Not_found -> Intset.empty in
-		    funtab:= PafMap.add paf (Intset.add i elem) !funtab) 
-	       rep.functions
-	 | _ -> ()) state.uf.map;
-    !funtab
-  
-
-let rec do_match state res pb_stack =
-  let mp=Stack.pop pb_stack in
-    match mp.mp_stack with
-	[] -> 
-	  res:= (mp.mp_inst,mp.mp_subst) :: !res
-      | (patt,cl)::remains ->
-	  let uf=state.uf in
-	    match patt with
-		PVar i -> 
-		  if mp.mp_subst.(pred i)<0 then  
-		    begin
-		      mp.mp_subst.(pred i)<- cl; (* no aliasing problem here *)
-		      Stack.push {mp with mp_stack=remains} pb_stack
-		    end
-		  else
-		    if mp.mp_subst.(pred i) = cl then
-		      Stack.push {mp with mp_stack=remains} pb_stack
-		    else (* mismatch for non-linear variable in pattern *) ()
-	      | PApp (f,[]) ->
-		  begin
-		    try let j=Hashtbl.find uf.syms f in
-		      if find uf j =cl then
-			Stack.push {mp with mp_stack=remains} pb_stack
-		    with Not_found -> ()
-		  end
-	      | PApp(f, ((last_arg::rem_args) as args)) ->
-		  try 
-		    let j=Hashtbl.find uf.syms f in 
-		    let paf={fsym=j;fnargs=List.length args} in
-		    let rep=get_representative uf cl in
-		    let good_terms = PafMap.find paf rep.functions in
-		    let aux i = 
-		      let (s,t) = signature state.uf i in
-			Stack.push 
-			  {mp with 
-			     mp_subst=Array.copy mp.mp_subst;
-			     mp_stack=
-			      (PApp(f,rem_args),s) :: 
-				(last_arg,t) :: remains} pb_stack in
-		      Intset.iter aux good_terms
-		  with Not_found -> ()
-
-let paf_of_patt syms = function
-    PVar _ -> invalid_arg "paf_of_patt: pattern is trivial"
-  | PApp (f,args) ->
-      {fsym=Hashtbl.find syms f;
-       fnargs=List.length args}
-
-let init_pb_stack state = 
-  let syms= state.uf.syms in
-  let pb_stack = Stack.create () in
-  let funtab = make_fun_table state in
-  let aux inst =
-    begin
-      let good_classes =
-	match inst.qe_lhs_valid with
-	  Creates_variables -> Intset.empty
-	| Normal ->
-	    begin 
-	      try 
-		let paf= paf_of_patt syms inst.qe_lhs in
-		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
-	    end
-	| Trivial typ -> 
-	    begin 
-	      try 
-		Hashtbl.find state.by_type typ
-	      with Not_found -> Intset.empty
-	    end in
-	Intset.iter (fun i -> 
-		       Stack.push 
-			 {mp_subst = Array.make inst.qe_nvars (-1); 
-			  mp_inst=inst;
-			  mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
-    end;
-    begin 
-      let good_classes =
-	match inst.qe_rhs_valid with
-	  Creates_variables -> Intset.empty
-	| Normal ->
-	    begin 
-	      try 
-		let paf= paf_of_patt syms inst.qe_rhs in
-		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
-	    end
-	| Trivial typ -> 
-	    begin 
-	      try 
-		Hashtbl.find state.by_type typ
-	      with Not_found -> Intset.empty
-	    end in
-	Intset.iter (fun i -> 
-		       Stack.push 
-			 {mp_subst = Array.make inst.qe_nvars (-1); 
-			  mp_inst=inst;
-			  mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
-    end in
-    List.iter aux state.quant;
-    pb_stack
-
-let find_instances state = 
-  let pb_stack= init_pb_stack state in
-  let res =ref [] in
-  let _ =
-    debug msgnl (str "Running E-matching algorithm ... ");
-    try
-      while true do
-	check_for_interrupt ();
-	do_match state res pb_stack 
-      done;
-      anomaly "get out of here !"
-    with Stack.Empty -> () in
-    !res
-
-let rec execute first_run state =
-  debug msgnl (str "Executing ... ");
-  try
-    while 
-      check_for_interrupt ();
-      one_step state do ()
-    done;
-    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 
-	    if state.rew_depth>0 then
-	      let l=find_instances state in
-		List.iter (add_inst state) l;
-		if state.changed then 
-		  begin
-		    state.changed <- false;
-		    execute true state
-		  end
-		else
-	      begin 
-		debug msgnl (str "Out of instances ... ");
-		None
-	      end
-	    else 
-	      begin 
-		debug msgnl (str "Out of depth ... ");
-		None
-	      end
-      | Some dis -> Some
-	  begin
-	    if first_run then Contradiction dis
-	    else Incomplete
-	  end
-  with Discriminable(s,spac,t,tpac) -> Some
-    begin
-      if first_run then Discrimination (s,spac,t,tpac)
-      else Incomplete
-    end
-
-
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
deleted file mode 100644
index cdc0065e..00000000
--- a/contrib/cc/ccalgo.mli
+++ /dev/null
@@ -1,222 +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        *)
-(************************************************************************)
-
-(* $Id: ccalgo.mli 10579 2008-02-21 13:54:00Z corbinea $ *)
-
-open Util
-open Term
-open Names
-
-type cinfo =
-    {ci_constr: constructor; (* inductive type *)
-     ci_arity: int;     (* # args *)
-     ci_nhyps: int}     (* # projectable args *)
-
-type term =
-    Symb of constr
-  | Product of sorts_family * sorts_family
-  | Eps of identifier
-  | Appli of term*term
-  | Constructor of cinfo (* constructor arity + nhyps *)
-
-type patt_kind =
-    Normal 
-  | Trivial of types
-  | Creates_variables
-
-type ccpattern =
-    PApp of term * ccpattern list
-  | PVar of int 
-
-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 constr * bool 
-  | Injection of int * pa_constructor * int * pa_constructor * int
-
-type from=
-    Goal
-  | Hyp of constr
-  | HeqG of constr
-  | HeqnH of constr*constr 
-
-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 constr_of_term : term -> constr
-
-val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
-
-val forest : state -> forest
-
-val axioms : forest -> (constr, term * term) Hashtbl.t
-
-val epsilons : forest -> pa_constructor list
-
-val empty : int -> Proof_type.goal Tacmach.sigma -> state
-
-val add_term : state -> term -> int
-
-val add_equality : state -> constr -> term -> term -> unit
-
-val add_disequality : state -> from -> term -> term -> unit
-
-val add_quant : state -> identifier -> bool -> 
-  int * patt_kind * ccpattern * patt_kind * ccpattern -> 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
-
-type quant_eq=
-    {qe_hyp_id: identifier;
-     qe_pol: bool;
-     qe_nvars:int;
-     qe_lhs: ccpattern;
-     qe_lhs_valid:patt_kind;
-     qe_rhs: ccpattern;
-     qe_rhs_valid:patt_kind}
-
-
-type pa_fun=
-    {fsym:int;
-     fnargs:int}
-
-type matching_problem
- 
-module PafMap: Map.S with type key = pa_fun
-
-val make_fun_table : state -> Intset.t PafMap.t 
-
-val do_match :  state ->
-    (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
-
-val init_pb_stack : state -> matching_problem Stack.t
-
-val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun
-
-val find_instances : state -> (quant_eq * int array) 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
-
-type rule = 
-    Congruence 
-  | Axiom of Names.identifier
-  | Injection of int*int*int*int
-
-type equality =
-    {lhs : int; 
-     rhs : int; 
-     rule : rule}
-
-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
-  
-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 get_constructor : t -> int -> Names.constructor
-  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
-  val union : t -> int -> int -> equality -> int list * equality list
-  val join_path : t -> int -> int -> 
-    ((int*int)*equality) list*
-    ((int*int)*equality) list
-end
-  
-
-val combine_rec : UF.t -> int list -> equality list
-val process_rec : UF.t -> equality list -> int list
-
-val cc : UF.t -> unit
-  
-val make_uf :
-  (Names.identifier * (term * term)) list -> UF.t
-
-val add_one_diseq : UF.t -> (term * term) -> int * int
-
-val add_disaxioms : 
-  UF.t -> (Names.identifier * (term * term)) list -> 
-  (Names.identifier * (int * int)) list
-  
-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
deleted file mode 100644
index a459b18f..00000000
--- a/contrib/cc/ccproof.ml
+++ /dev/null
@@ -1,153 +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        *)
-(************************************************************************)
-
-(* $Id: ccproof.ml 9857 2007-05-24 14:21:08Z corbinea $ *)
-
-(* This file uses the (non-compressed) union-find structure to generate *) 
-(* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
-
-open Util
-open Names
-open Term
-open Ccalgo
-  
-type rule=
-    Ax of constr
-  | SymAx of constr
-  | Refl of term
-  | Trans of proof*proof
-  | Congr of proof*proof
-  | Inject of proof*constructor*int*int 
-and proof = 
-    {p_lhs:term;p_rhs:term;p_rule:rule}
-
-let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t}
-
-let pcongr p1 p2 = 
-  match p1.p_rule,p2.p_rule with 
-    Refl t1, Refl t2 -> prefl (Appli (t1,t2))
-  | _, _ -> 
-      {p_lhs=Appli (p1.p_lhs,p2.p_lhs);
-       p_rhs=Appli (p1.p_rhs,p2.p_rhs);
-       p_rule=Congr (p1,p2)}
-
-let rec ptrans p1 p3=
-  match p1.p_rule,p3.p_rule with
-      Refl _, _ ->p3
-    | _, Refl _ ->p1
-    | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
-    | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
-    | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
-	ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
-  | _, _ -> 
-      if p1.p_rhs = p3.p_lhs then 
-	{p_lhs=p1.p_lhs;
-	 p_rhs=p3.p_rhs;
-	 p_rule=Trans (p1,p3)}
-      else anomaly "invalid cc transitivity"
-	
-let rec psym p = 
-  match p.p_rule with 
-      Refl _ -> p 
-    | SymAx s ->
-	{p_lhs=p.p_rhs;
-	 p_rhs=p.p_lhs;
-	 p_rule=Ax s}
-    | Ax s->      
-	{p_lhs=p.p_rhs;
-	 p_rhs=p.p_lhs;
-	 p_rule=SymAx s}
-  | Inject (p0,c,n,a)-> 
-      {p_lhs=p.p_rhs;
-       p_rhs=p.p_lhs;
-       p_rule=Inject (psym p0,c,n,a)}
-  | Trans (p1,p2)-> ptrans (psym p2) (psym p1)
-  | Congr (p1,p2)-> pcongr (psym p1) (psym p2)
-
-let pax axioms s =
-  let l,r = Hashtbl.find axioms s in
-    {p_lhs=l;
-     p_rhs=r;
-     p_rule=Ax s}
-
-let psymax axioms s =
-  let l,r = Hashtbl.find axioms s in
-    {p_lhs=r;
-     p_rhs=l;
-     p_rule=SymAx s}
-
-let rec nth_arg t n=
-  match t with 
-      Appli (t1,t2)-> 
-	if n>0 then 
-	  nth_arg t1 (n-1)
-	else t2
-    | _ -> anomaly "nth_arg: not enough args"
-
-let pinject p c n a =
-  {p_lhs=nth_arg p.p_lhs (n-a);
-   p_rhs=nth_arg p.p_rhs (n-a);
-   p_rule=Inject(p,c,n,a)}
-
-let build_proof uf=
-
-  let axioms = axioms uf in
-
-  let rec equal_proof i j=
-    if i=j then prefl (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)=
-    let pi=equal_proof i eq.lhs in
-    let pj=psym (equal_proof j eq.rhs) in
-    let pij=
-      match eq.rule with 
-	  Axiom (s,reversed)->
-	    if reversed then psymax axioms s 
-	    else pax axioms s
-	| Congruence ->congr_proof eq.lhs eq.rhs
-	| Injection (ti,ipac,tj,jpac,k) ->
-	    let p=ind_proof ti ipac tj jpac in
-	    let cinfo= get_constructor_info uf ipac.cnode in
-	      pinject p cinfo.ci_constr cinfo.ci_nhyps k	
-    in  ptrans (ptrans pi pij) pj
-
-  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 (prefl targ))
-
-  and path_proof i=function
-      [] -> prefl (term uf i)
-    | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
-  
-  and congr_proof i j=
-    let (i1,i2) = subterms uf i
-    and (j1,j2) = subterms uf j in   
-      pcongr (equal_proof i1 j1) (equal_proof i2 j2)
-	
-  and ind_proof i ipac j jpac=
-    let p=equal_proof i j 
-    and p1=constr_proof i i ipac 
-    and p2=constr_proof j j jpac in
-      ptrans (psym p1) (ptrans p p2)
-  in
-    function
-	`Prove (i,j) -> equal_proof i j
-      | `Discr (i,ci,j,cj)-> ind_proof i ci j cj
-
-
-
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
deleted file mode 100644
index 0eb97efe..00000000
--- a/contrib/cc/ccproof.mli
+++ /dev/null
@@ -1,31 +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        *)
-(************************************************************************)
-
-(* $Id: ccproof.mli 9857 2007-05-24 14:21:08Z corbinea $ *)
-
-open Ccalgo
-open Names
-open Term
-
-type rule=
-    Ax of constr
-  | SymAx of constr
-  | Refl of term
-  | Trans of proof*proof
-  | Congr of proof*proof
-  | Inject of proof*constructor*int*int 
-and proof = 
-    private {p_lhs:term;p_rhs:term;p_rule:rule}
-
-val build_proof : 
-  forest -> 
-  [ `Discr of int * pa_constructor * int * pa_constructor
-  | `Prove of int * int ] -> proof
-
-
-
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
deleted file mode 100644
index 00cbbeee..00000000
--- a/contrib/cc/cctac.ml
+++ /dev/null
@@ -1,465 +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: cctac.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
-
-(* 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 Typing
-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 _refl_equal = constant ["Init";"Logic"] "refl_equal"
-
-let _sym_eq = constant ["Init";"Logic"] "sym_eq"
-
-let _trans_eq = constant ["Init";"Logic"] "trans_eq"
-
-let _eq = constant ["Init";"Logic"] "eq"
-
-let _False = constant ["Init";"Logic"] "False"
-
-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))
-
-(* decompose member of equality in an applicative format *)
-
-let sf_of env sigma c = family_of_sort (destSort (whd_delta env (type_of env sigma c)))
-
-let rec decompose_term env sigma t=
-    match kind_of_term (whd env t) with
-      App (f,args)->
-	let tf=decompose_term env sigma f in
-	let targs=Array.map (decompose_term env sigma) args in
-	  Array.fold_left (fun s t->Appli (s,t)) tf targs
-    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
-	let b = pop _b in
-	let sort_b = sf_of env sigma b in
-	let sort_a = sf_of env sigma a in
-	Appli(Appli(Product (sort_a,sort_b) ,
-		    decompose_term env sigma a),
-	      decompose_term env sigma b)
-    | 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}
-    | _ ->if closed0 t then (Symb t) else raise Not_found
-	
-(* decompose equality in members and type *)
-	
-let atom_of_constr env sigma 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 sigma args.(1), 
-		   decompose_term env sigma args.(2)) 
-	  else `Other (decompose_term env sigma term)
-    | _ -> `Other (decompose_term env sigma term)
-
-let rec pattern_of_constr env sigma c =
-  match kind_of_term (whd env c) with
-      App (f,args)->
-	let pf = decompose_term env sigma f in
-	let pargs,lrels = List.split 
-	  (array_map_to_list (pattern_of_constr env sigma) args) in
-	  PApp (pf,List.rev pargs),
-	List.fold_left Intset.union Intset.empty lrels
-    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
-	let b =pop _b in
-	let pa,sa = pattern_of_constr env sigma a in
-	let pb,sb = pattern_of_constr env sigma (pop b) in
-	let sort_b = sf_of env sigma b in
-	let sort_a = sf_of env sigma a in
-	  PApp(Product (sort_a,sort_b),
-	       [pa;pb]),(Intset.union sa sb)
-    | Rel i -> PVar i,Intset.singleton i
-    | _ -> 
-	let pf = decompose_term env sigma c in
-	  PApp (pf,[]),Intset.empty
-
-let non_trivial = function
-    PVar _ -> false
-  | _ -> true
-
-let patterns_of_constr env sigma nrels term=
-  let f,args= 
-    try destApp (whd_delta env term) with _ -> raise Not_found in
-	if eq_constr f (Lazy.force _eq) && (Array.length args)=3 
-	then 
-	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
-	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
-	  let valid1 = 
-	    if Intset.cardinal rels1 <> nrels then Creates_variables
-	    else if non_trivial patt1 then Normal
-	    else Trivial args.(0) 
-	  and valid2 =
-	    if Intset.cardinal rels2 <> nrels then Creates_variables
-	    else if non_trivial patt2 then Normal
-	    else Trivial args.(0) in
-	    if valid1 <> Creates_variables
-	      || valid2 <> Creates_variables  then 
-	      nrels,valid1,patt1,valid2,patt2
-	    else raise Not_found
-	else raise Not_found
-
-let rec quantified_atom_of_constr env sigma nrels term =
-  match kind_of_term (whd_delta env term) with
-      Prod (_,atom,ff) -> 
-	if eq_constr ff (Lazy.force _False) then
-	  let patts=patterns_of_constr env sigma nrels atom in
-	      `Nrule patts
-	else 
-	  quantified_atom_of_constr env sigma (succ nrels) ff
-    | _ ->  
-	let patts=patterns_of_constr env sigma nrels term in
-	    `Rule patts	  
-
-let litteral_of_constr env sigma 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 sigma atom) with
-	      `Eq(t,a,b) -> `Neq(t,a,b)
-	    | `Other(p) -> `Nother(p)
-	else
-	  begin
-	    try 
-	      quantified_atom_of_constr env sigma 1 ff  
-	    with Not_found ->
-	      `Other (decompose_term env sigma term)
-	  end
-    | _ -> 
-	atom_of_constr env sigma term
-	
-
-(* store all equalities from the context *)
-	
-let rec make_prb gls depth additionnal_terms =
-  let env=pf_env gls in
-  let sigma=sig_sig gls in
-  let state = empty depth gls in
-  let pos_hyps = ref [] in
-  let neg_hyps =ref [] in
-    List.iter
-      (fun c ->
-	 let t = decompose_term env sigma c in
-	   ignore (add_term state t)) additionnal_terms; 
-    List.iter 
-      (fun (id,_,e) ->
-	 begin
-	   let cid=mkVar id in
-	   match litteral_of_constr env sigma e with
-	       `Eq (t,a,b) -> add_equality state cid a b
-	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
-	     | `Other ph ->
-		 List.iter 
-		   (fun (cidn,nh) -> 
-		      add_disequality state (HeqnH (cid,cidn)) ph nh) 
-		   !neg_hyps;
-		 pos_hyps:=(cid,ph):: !pos_hyps
-	     | `Nother nh ->
-		 List.iter 
-		   (fun (cidp,ph) -> 
-		      add_disequality state (HeqnH (cidp,cid)) ph nh) 
-		   !pos_hyps;
-		 neg_hyps:=(cid,nh):: !neg_hyps
-	     | `Rule patts -> add_quant state id true patts
-	     | `Nrule patts -> add_quant state id false patts
-	 end) (Environ.named_context_of_val gls.it.evar_hyps);
-    begin
-      match atom_of_constr env sigma 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=pred (snd cstr) 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_case_info (pf_env gls) ind RegularStyle 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 _M =mkMeta
-
-let rec proof_tac p gls =
-  match p.p_rule with
-      Ax c -> exact_check c gls
-    | SymAx c -> 
-	let l=constr_of_term p.p_lhs and 
-	    r=constr_of_term p.p_rhs in
-        let typ = refresh_universes (pf_type_of gls l) in 	  
-	  exact_check
-	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
-    | Refl t ->
-	let lr = constr_of_term t in
-	let typ = refresh_universes (pf_type_of gls lr) in 
-	exact_check
-	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
-    | Trans (p1,p2)->
-	let t1 = constr_of_term p1.p_lhs and
-	    t2 = constr_of_term p1.p_rhs and
-	    t3 = constr_of_term p2.p_rhs in
-	let typ = refresh_universes (pf_type_of gls t2) in 
-	let prf = 
-	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
-	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
-    | Congr (p1,p2)->
-	let tf1=constr_of_term p1.p_lhs 
-	and tx1=constr_of_term p2.p_lhs 
-	and tf2=constr_of_term p1.p_rhs 
-	and tx2=constr_of_term p2.p_rhs in
-	let typf = refresh_universes (pf_type_of gls tf1) in
-	let typx = refresh_universes (pf_type_of gls tx1) in
-	let typfx = refresh_universes (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;_M 1|]) in
-	let lemma2=
-	  mkApp(Lazy.force _f_equal,
-		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
-	let prf = 
-	  mkApp(Lazy.force _trans_eq,
-		[|typfx;
-		  mkApp(tf1,[|tx1|]);
-		  mkApp(tf2,[|tx1|]);
-		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
-	  tclTHENS (refine prf)
-	    [tclTHEN (refine lemma1) (proof_tac p1);
-  	     tclFIRST
-	       [tclTHEN (refine lemma2) (proof_tac p2);
-		reflexivity;
-		fun gls ->
-		  errorlabstrm  "Congruence" 
-		    (Pp.str 
-		       "I don't know how to handle dependent equality")]] gls
-  | Inject (prf,cstr,nargs,argind) ->
-	 let ti=constr_of_term prf.p_lhs in
-	 let tj=constr_of_term prf.p_rhs in
-	 let default=constr_of_term p.p_lhs in
-	 let intype=refresh_universes (pf_type_of gls ti) in
-	 let outtype=refresh_universes (pf_type_of gls default) in
-	 let special=mkRel (1+nargs-argind) in
-	 let proj=build_projection intype outtype cstr special default gls in
-	 let injt=
-	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in 
-	   tclTHEN (refine injt) (proof_tac prf) gls
-
-let refute_tac c t1 t2 p gls =      
-  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype=refresh_universes (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 (c,[|mkVar hid|]) in
-    tclTHENS (assert_tac (Name hid) neweq)
-      [proof_tac p; simplest_elim false_t] gls
-
-let convert_to_goal_tac c t1 t2 p gls =
-  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort=refresh_universes (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;c;tt2;mkVar e|]) in
-    tclTHENS (assert_tac (Name e) neweq) 
-      [proof_tac p;exact_check endt] gls
-
-let convert_to_hyp_tac c1 t1 c2 t2 p gls =
-  let tt2=constr_of_term t2 in
-  let h=pf_get_new_id (id_of_string "H") gls in
-  let false_t=mkApp (c2,[|mkVar h|]) in
-    tclTHENS (assert_tac (Name h) tt2)
-      [convert_to_goal_tac c1 t1 t2 p;
-       simplest_elim false_t] gls
-  
-let discriminate_tac cstr p gls =
-  let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-  let intype=refresh_universes (pf_type_of gls t1) 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;t1;t2;mkVar hid|]) in   
-  let endt=mkApp (Lazy.force _eq_rect,
-		  [|outtype;trivial;pred;identity;concl;injt|]) in
-  let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
-    tclTHENS (assert_tac (Name hid) neweq) 
-      [proof_tac 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 -> constr_of_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 depth additionnal_terms gls=
-  Coqlib.check_required_library ["Coq";"Init";"Logic"];
-  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
-  let state = make_prb gls depth 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 (str "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 cstr p gls
-	    | Incomplete ->
-		let metacnt = ref 0 in
-		let newmeta _ = incr metacnt; _M !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 (str "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
-		  match dis.rule with
-		      Goal -> proof_tac p gls
-		    | Hyp id -> refute_tac id ta tb p gls
-		    | HeqG id -> 
-			convert_to_goal_tac id ta tb p gls
-		    | HeqnH (ida,idb) -> 
-			convert_to_hyp_tac ida ta idb tb p gls
-		    
-
-let cc_fail gls =
-  errorlabstrm  "Congruence" (Pp.str "congruence failed.")     
-
-let congruence_tac depth l = 
-  tclORELSE 
-    (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) 
-    cc_fail
-
-(* Beware: reflexivity = constructor 1 = apply refl_equal
-   might be slow now, let's rather do something equivalent
-   to a "simple apply refl_equal" *)
-
-let simple_reflexivity () = apply (Lazy.force _refl_equal)
-
-(* The [f_equal] tactic.
-
-   It mimics the use of lemmas [f_equal], [f_equal2], etc.
-   This isn't particularly related with congruence, apart from
-   the fact that congruence is called internally. 
-*)
-
-let f_equal gl = 
-  let cut_eq c1 c2 = 
-    let ty = refresh_universes (pf_type_of gl c1) in 
-    tclTHENTRY
-      (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
-      (simple_reflexivity ())
-  in 
-  try match kind_of_term (pf_concl gl) with 
-    | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> 
-	begin match kind_of_term t, kind_of_term t' with 
-	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
-	      let rec cuts i = 
-		if i < 0 then tclTRY (congruence_tac 1000 []) 
-		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
-	      in cuts (Array.length v - 1) gl
-	  | _ -> tclIDTAC gl
-	end
-    | _ -> tclIDTAC gl
-  with Type_errors.TypeError _ -> tclIDTAC gl
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
deleted file mode 100644
index 57ad0558..00000000
--- a/contrib/cc/cctac.mli
+++ /dev/null
@@ -1,22 +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        *)
-(************************************************************************)
-
-(* $Id: cctac.mli 10637 2008-03-07 23:52:56Z letouzey $ *)
-
-open Term 
-open Proof_type
-
-val proof_tac: Ccproof.proof -> Proof_type.tactic
-
-val cc_tactic : int -> constr list -> tactic
-
-val cc_fail : tactic
-
-val congruence_tac : int -> constr list -> tactic
-
-val f_equal : tactic
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4
deleted file mode 100644
index 9877e6fc..00000000
--- a/contrib/cc/g_congruence.ml4
+++ /dev/null
@@ -1,29 +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: g_congruence.ml4 10637 2008-03-07 23:52:56Z letouzey $ *)
-
-open Cctac
-open Tactics
-open Tacticals
-
-(* Tactic registration *)
-      
-TACTIC EXTEND cc
- [ "congruence" ] -> [ congruence_tac 1000 [] ]
- |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
- |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> 
-   [ congruence_tac n l ]
-END
-
-TACTIC EXTEND f_equal
- [ "f_equal" ] -> [ f_equal ]
-END