Delete trailing whitespaces in all *.{v,ml*} files

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

7 files changed, 353 insertions, 353 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 418980c54b..9cc6f9de93 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -22,45 +22,45 @@ open Proof_type
 
 let init_size=5
 
-let cc_verbose=ref false 
+let cc_verbose=ref false
 
-let debug f x = 
+let debug f x =
   if !cc_verbose then f x
 
 let _=
   let gdopt=
     { optsync=true;
       optname="Congruence Verbose";
-      optkey=["Congruence";"Verbose"]; 
-      optread=(fun ()-> !cc_verbose); 
-      optwrite=(fun b -> cc_verbose := b)}  
+      optkey=["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 
+    if Hashtbl.mem st.toterm sign then
 	anomaly "enter: signature already entered"
-    else 
+    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;
@@ -69,7 +69,7 @@ module ST=struct
 	Not_found -> ()
 
   let rec delete_set st s = Intset.iter (delete st) s
-	  
+
 end
 
 type pa_constructor=
@@ -85,11 +85,11 @@ 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 PacMap=Map.Make(struct
+			 type t=pa_constructor
+			 let compare=Pervasives.compare end)
 
-module PafMap=Map.Make(struct 
+module PafMap=Map.Make(struct
 			 type t=pa_fun
 			 let compare=Pervasives.compare end)
 
@@ -107,11 +107,11 @@ type term=
 
 type ccpattern =
     PApp of term * ccpattern list (* arguments are reversed *)
-  | PVar of int 
+  | PVar of int
 
 type rule=
     Congruence
-  | Axiom of constr * bool 
+  | Axiom of constr * bool
   | Injection of int * pa_constructor * int * pa_constructor * int
 
 type from=
@@ -127,7 +127,7 @@ type equality = rule eq
 type disequality = from eq
 
 type patt_kind =
-    Normal 
+    Normal
   | Trivial of types
   | Creates_variables
 
@@ -146,7 +146,7 @@ let swap eq : equality =
     | 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
@@ -163,15 +163,15 @@ type representative=
      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 = 
+type vertex = Leaf| Node of (int*int)
+
+type node =
     {mutable clas:cl;
-     mutable cpath: int; 
+     mutable cpath: int;
      vertex:vertex;
      term:term}
-    
+
 type forest=
     {mutable max_size:int;
      mutable size:int;
@@ -180,11 +180,11 @@ type forest=
      mutable epsilons: pa_constructor list;
      syms:(term,int) Hashtbl.t}
 
-type state = 
+type state =
     {uf: forest;
      sigtable:ST.t;
-     mutable terms: Intset.t; 
-     combine: equality Queue.t; 
+     mutable terms: Intset.t;
+     combine: equality Queue.t;
      marks: (int * pa_mark) Queue.t;
      mutable diseq: disequality list;
      mutable quant: quant_eq list;
@@ -222,17 +222,17 @@ let empty depth gls:state =
   changed=false;
   gls=gls}
 
-let forest state = state.uf 
-       
+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 
+
+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
@@ -245,7 +245,7 @@ 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
 
@@ -264,36 +264,36 @@ let add_rfather uf i t=
     r.weight<-r.weight+1;
     r.fathers <-Intset.add t r.fathers
 
-exception Discriminable of int * pa_constructor * int * pa_constructor 
+exception Discriminable of int * pa_constructor * int * pa_constructor
 
 let append_pac t p =
-  {p with arity=pred p.arity;args=t::p.args} 
+  {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 = 
+  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
@@ -304,11 +304,11 @@ let next uf=
 	  uf.max_size<-newmax;
 	  Array.blit uf.map 0 newmap 0 size;
 	  uf.map<-newmap
-	end 
+	end
     else ();
-    uf.size<-nsize; 
+    uf.size<-nsize;
     size
-	
+
 let new_representative typ =
   {weight=0;
    lfathers=Intset.empty;
@@ -317,14 +317,14 @@ let new_representative typ =
    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 = 
+let cc_product s1 s2 =
   mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
 	   mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
 
@@ -332,27 +332,27 @@ 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 
+  | 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 
+    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 
+  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) -> 
+    PVar i ->
+      subst.(pred i)
+  | PApp (t, args) ->
       List.fold_right
 	(fun spat f -> Appli (f,inst_pattern subst spat))
-	   args t  
+	   args t
 
 let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
   Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
@@ -360,9 +360,9 @@ let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
 let pr_term t = str "[" ++
   Termops.print_constr (constr_of_term t) ++ str "]"
 
-let rec add_term state t= 
+let rec add_term state t=
   let uf=state.uf in
-    try Hashtbl.find uf.syms t with 
+    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
@@ -377,12 +377,12 @@ let rec add_term state t=
 		     cpath= -1;
 		     vertex= Leaf;
 		     term= t}
-	      | Eps id -> 
+	      | Eps id ->
 		  {clas= Rep (new_representative typ);
 		   cpath= -1;
 		   vertex= Leaf;
 		   term= t}
-	      | Appli (t1,t2) -> 
+	      | 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;
@@ -408,9 +408,9 @@ let rec add_term state 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 
+	    Hashtbl.replace state.by_type typ
+	      (Intset.add b
+		 (try Hashtbl.find state.by_type typ with
 		      Not_found -> Intset.empty));
 	    b
 
@@ -436,22 +436,22 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
      qe_rhs_valid=valid2}::state.quant
 
 let is_redundant state id args =
-  try  
+  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) 
+    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) = 
+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   
+  else
     begin
       Hashtbl.add state.q_history inst.qe_hyp_id int_subst;
       let subst = build_subst (forest state) int_subst in
@@ -459,149 +459,149 @@ let add_inst state (inst,int_subst) =
       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 
+	  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 
+		debug (fun () ->
+		  msgnl
 		   (str "Adding new equality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++ 
+	          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 
+		debug (fun () ->
+		  msgnl
 		   (str "Adding new disequality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++ 
+	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
-		add_disequality state (Hyp prf) s t 
+		add_disequality state (Hyp prf) s t
 	      end
   end
 
 let link uf i j eq = (* links i -> j *)
-  let node=uf.map.(i) in 
+  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) 
+  | (((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 ++ 
+  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 
+  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 
+    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) 
+      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)) 
+      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 
+      match r1.inductive_status,r2.inductive_status with
 	  Unknown,_ -> ()
-	| Partial pac,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) -> 
+	| Partial _ ,(Partial _ |Partial_applied) ->
 	    state.pa_classes<-Intset.remove i1 state.pa_classes
-	| Partial_applied,Unknown -> 
-	    r2.inductive_status<-Partial_applied	      
-	| Partial_applied,Partial _ -> 
+	| 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    
-	| _,_ -> () 
-            
+	| 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 ++ 
+  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 
+  let i=find uf eq.lhs
   and j=find uf eq.rhs in
-    if i<>j then 
+    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 
+  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 
+      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 
+    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 
+    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)) 
+	  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 
+	      if n > 0 then
 		match (oargs,args) with
 		    s1::q1,s2::q2->
-		      Queue.add 
+		      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" 
+		      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;
@@ -617,8 +617,8 @@ let process_constructor_mark t i rep pac state =
 	      state.pa_classes<- Intset.add i state.pa_classes
 	    end
 
-let process_mark t m state = 
-  debug (fun () -> msgnl 
+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
@@ -634,15 +634,15 @@ type explanation =
 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 
+      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 
+    | [] -> None
   in
     check_aux state.diseq
 
@@ -651,8 +651,8 @@ let one_step state =
       let eq = Queue.take state.combine in
 	merge eq state;
 	true
-    with Queue.Empty -> 
-      try 
+    with Queue.Empty ->
+      try
 	let (t,m) = Queue.take state.marks in
 	  process_mark t m state;
 	  true
@@ -664,40 +664,40 @@ let one_step state =
 	    true
 	with Not_found -> false
 
-let __eps__ = id_of_string "_eps_"  
+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 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 = 
+	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)) 
+	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 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; 
+	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
-    | _ -> anomaly "wrong incomplete class" 
+    | _ -> anomaly "wrong incomplete class"
 
 let complete state =
   Intset.iter (complete_one_class state) state.pa_classes
 
-type matching_problem = 
+type matching_problem =
 {mp_subst : int array;
  mp_inst : quant_eq;
  mp_stack : (ccpattern*int) list }
@@ -705,31 +705,31 @@ type matching_problem =
 let make_fun_table state =
   let uf= state.uf in
   let funtab=ref PafMap.empty in
-  Array.iteri 
+  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 
+	     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) 
+		    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  
+		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
@@ -746,18 +746,18 @@ let rec do_match state res pb_stack =
 		    with Not_found -> ()
 		  end
 	      | PApp(f, ((last_arg::rem_args) as args)) ->
-		  try 
-		    let j=Hashtbl.find uf.syms f in 
+		  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 aux i =
 		      let (s,t) = signature state.uf i in
-			Stack.push 
-			  {mp with 
+			Stack.push
+			  {mp with
 			     mp_subst=Array.copy mp.mp_subst;
 			     mp_stack=
-			      (PApp(f,rem_args),s) :: 
+			      (PApp(f,rem_args),s) ::
 				(last_arg,t) :: remains} pb_stack in
 		      Intset.iter aux good_terms
 		  with Not_found -> ()
@@ -768,7 +768,7 @@ let paf_of_patt syms = function
       {fsym=Hashtbl.find syms f;
        fnargs=List.length args}
 
-let init_pb_stack state = 
+let init_pb_stack state =
   let syms= state.uf.syms in
   let pb_stack = Stack.create () in
   let funtab = make_fun_table state in
@@ -778,51 +778,51 @@ let init_pb_stack state =
 	match inst.qe_lhs_valid with
 	  Creates_variables -> Intset.empty
 	| Normal ->
-	    begin 
-	      try 
+	    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 
+	| 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); 
+	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 
+    begin
       let good_classes =
 	match inst.qe_rhs_valid with
 	  Creates_variables -> Intset.empty
 	| Normal ->
-	    begin 
-	      try 
+	    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 
+	| 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); 
+	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 find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
@@ -830,7 +830,7 @@ let find_instances state =
     try
       while true do
 	check_for_interrupt ();
-	do_match state res pb_stack 
+	do_match state res pb_stack
       done;
       anomaly "get out of here !"
     with Stack.Empty -> () in
@@ -839,34 +839,34 @@ let find_instances state =
 let rec execute first_run state =
   debug msgnl (str "Executing ... ");
   try
-    while 
+    while
       check_for_interrupt ();
       one_step state do ()
     done;
     match check_disequalities state with
-	None -> 
+	None ->
 	  if not(Intset.is_empty state.pa_classes) then
-	    begin 
+	    begin
 	      debug msgnl (str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
-	  else 
+	  else
 	    if state.rew_depth>0 then
 	      let l=find_instances state in
 		List.iter (add_inst state) l;
-		if state.changed then 
+		if state.changed then
 		  begin
 		    state.changed <- false;
 		    execute true state
 		  end
 		else
-	      begin 
+	      begin
 		debug msgnl (str "Out of instances ... ");
 		None
 	      end
-	    else 
-	      begin 
+	    else
+	      begin
 		debug msgnl (str "Out of depth ... ");
 		None
 	      end
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3bd52b6e1d..5f56c7e69f 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -25,35 +25,35 @@ type term =
   | Constructor of cinfo (* constructor arity + nhyps *)
 
 type patt_kind =
-    Normal 
+    Normal
   | Trivial of types
   | Creates_variables
 
 type ccpattern =
     PApp of term * ccpattern list
-  | PVar of int 
+  | PVar of int
 
 type pa_constructor =
     { cnode : int;
       arity : int;
       args  : int list}
 
-module PacMap : Map.S with type key = pa_constructor  
+module PacMap : Map.S with type key = pa_constructor
 
 type forest
 
-type state 
+type state
 
 type rule=
     Congruence
-  | Axiom of constr * bool 
+  | 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 
+  | HeqnH of constr*constr
 
 type 'a eq = {lhs:int;rhs:int;rule:'a}
 
@@ -84,7 +84,7 @@ val add_equality : state -> constr -> term -> term -> unit
 
 val add_disequality : state -> from -> term -> term -> unit
 
-val add_quant : state -> identifier -> bool -> 
+val add_quant : state -> identifier -> bool ->
   int * patt_kind * ccpattern * patt_kind * ccpattern -> unit
 
 val tail_pac : pa_constructor -> pa_constructor
@@ -99,7 +99,7 @@ val get_constructor_info : forest -> int -> cinfo
 
 val subterms : forest -> int -> int * int
 
-val join_path : forest -> int -> int -> 
+val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
 type quant_eq=
@@ -117,10 +117,10 @@ type pa_fun=
      fnargs:int}
 
 type matching_problem
- 
+
 module PafMap: Map.S with type key = pa_fun
 
-val make_fun_table : state -> Intset.t PafMap.t 
+val make_fun_table : state -> Intset.t PafMap.t
 
 val do_match :  state ->
     (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
@@ -150,20 +150,20 @@ val execute : bool -> state -> explanation option
 
 module PacMap:Map.S with type key=pa_constructor
 
-type term = 
-    Symb of Term.constr 
+type term =
+    Symb of Term.constr
   | Eps
-  | Appli of term * term 
+  | Appli of term * term
   | Constructor of Names.constructor*int*int
 
-type rule = 
-    Congruence 
+type rule =
+    Congruence
   | Axiom of Names.identifier
   | Injection of int*int*int*int
 
 type equality =
-    {lhs : int; 
-     rhs : int; 
+    {lhs : int;
+     rhs : int;
      rule : rule}
 
 module ST :
@@ -175,47 +175,47 @@ sig
   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 
+  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 -> 
+  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 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 -> 
+  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 -> 
+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 -> 
+val find_contradiction : UF.t ->
+  (Names.identifier * (int * int)) list ->
   (Names.identifier * (int * int))
 *)
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 1e57aa6cb1..2a019ebfff 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -8,30 +8,30 @@
 
 (* $Id$ *)
 
-(* This file uses the (non-compressed) union-find structure to generate *) 
+(* 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 = 
+  | 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 
+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)}
@@ -44,25 +44,25 @@ let rec ptrans p1 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 
+  | _, _ ->
+      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 
+
+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->      
+    | Ax s->
 	{p_lhs=p.p_rhs;
 	 p_rhs=p.p_lhs;
 	 p_rule=SymAx s}
-  | Inject (p0,c,n,a)-> 
+  | Inject (p0,c,n,a)->
       {p_lhs=p.p_rhs;
        p_rhs=p.p_lhs;
        p_rule=Inject (psym p0,c,n,a)}
@@ -82,9 +82,9 @@ let psymax axioms s =
      p_rule=SymAx s}
 
 let rec nth_arg t n=
-  match t with 
-      Appli (t1,t2)-> 
-	if n>0 then 
+  match t with
+      Appli (t1,t2)->
+	if n>0 then
 	  nth_arg t1 (n-1)
 	else t2
     | _ -> anomaly "nth_arg: not enough args"
@@ -99,23 +99,23 @@ let build_proof uf=
   let axioms = axioms uf in
 
   let rec equal_proof i j=
-    if i=j then prefl (term uf i) else 
+    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 
+      match eq.rule with
 	  Axiom (s,reversed)->
-	    if reversed then psymax axioms s 
+	    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	
+	      pinject p cinfo.ci_constr cinfo.ci_nhyps k
     in  ptrans (ptrans pi pij) pj
 
   and constr_proof i t ipac=
@@ -133,15 +133,15 @@ let build_proof uf=
   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   
+    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 
+    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
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 7fd28390f6..2a0ca688c6 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -18,12 +18,12 @@ type rule=
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
-  | Inject of proof*constructor*int*int 
-and proof = 
+  | Inject of proof*constructor*int*int
+and proof =
     private {p_lhs:term;p_rhs:term;p_rule:rule}
 
-val build_proof : 
-  forest -> 
+val build_proof :
+  forest ->
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 515d4aa932..4e6ea8022e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -80,18 +80,18 @@ let rec decompose_term env sigma t=
 		       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 
+  let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3 
+	  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)) 
+		   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)
 
@@ -99,7 +99,7 @@ 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 
+	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
@@ -112,7 +112,7 @@ let rec pattern_of_constr env sigma c =
 	  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
 
@@ -121,58 +121,58 @@ let non_trivial = function
   | _ -> true
 
 let patterns_of_constr env sigma nrels term=
-  let f,args= 
+  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 
+	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 = 
+	  let valid1 =
 	    if Intset.cardinal rels1 <> nrels then Creates_variables
 	    else if non_trivial patt1 then Normal
-	    else Trivial args.(0) 
+	    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 
+	      || 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) -> 
+      Prod (_,atom,ff) ->
 	if eq_constr ff (Lazy.force _False) then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
-	else 
+	else
 	  quantified_atom_of_constr env sigma (succ nrels) ff
-    | _ ->  
+    | _ ->
 	let patts=patterns_of_constr env sigma nrels term in
-	    `Rule patts	  
+	    `Rule patts
 
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
-    | Prod (_,atom,ff) -> 
+    | 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  
+	    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
@@ -182,8 +182,8 @@ let rec make_prb gls depth additionnal_terms =
     List.iter
       (fun c ->
 	 let t = decompose_term env sigma c in
-	   ignore (add_term state t)) additionnal_terms; 
-    List.iter 
+	   ignore (add_term state t)) additionnal_terms;
+    List.iter
       (fun (id,_,e) ->
 	 begin
 	   let cid=mkVar id in
@@ -191,15 +191,15 @@ let rec make_prb gls depth additionnal_terms =
 	       `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) 
+		 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) 
+		 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
@@ -208,9 +208,9 @@ let rec make_prb gls depth additionnal_terms =
     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) -> 
+	|	`Other g ->
+		  List.iter
+	      (fun (idp,ph) ->
 		 add_disequality state (HeqG idp) ph g) !pos_hyps
     end;
     state
@@ -218,11 +218,11 @@ let rec make_prb gls depth additionnal_terms =
 (* 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 
+  let env=pf_env gls in
+  let (h,argv) =
+    try destApp intype with
 	Invalid_argument _ -> (intype,[||])  in
-  let ind=destInd h 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
@@ -230,16 +230,16 @@ let build_projection intype outtype (cstr:constructor) special default gls=
     let ti=Term.prod_appvect types.(i) argv in
     let rc=fst (decompose_prod_assum ti) in
     let head=
-      if i=ci then special else default in  
+      if i=ci then special else default in
       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     
+  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
@@ -247,29 +247,29 @@ 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 
+    | 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 	  
+        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 
+	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 = 
+	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 
+	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
@@ -282,7 +282,7 @@ let rec proof_tac p gls =
 	let lemma2=
 	  mkApp(Lazy.force _f_equal,
 		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
-	let prf = 
+	let prf =
 	  mkApp(Lazy.force _trans_eq,
 		[|typfx;
 		  mkApp(tf1,[|tx1|]);
@@ -294,8 +294,8 @@ let rec proof_tac p gls =
 	       [tclTHEN (refine lemma2) (proof_tac p2);
 		reflexivity;
 		fun gls ->
-		  errorlabstrm  "Congruence" 
-		    (Pp.str 
+		  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
@@ -306,10 +306,10 @@ let rec proof_tac p gls =
 	 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 
+	   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 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=
@@ -323,13 +323,13 @@ let refute_tac c t1 t2 p 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 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 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) 
+    tclTHENS (assert_tac (Name e) neweq)
       [proof_tac p;exact_check endt] gls
 
 let convert_to_hyp_tac c1 t1 c2 t2 p gls =
@@ -339,7 +339,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls =
     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
@@ -351,25 +351,25 @@ let discriminate_tac cstr p gls =
   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 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   
+		  [|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) 
+    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
@@ -379,7 +379,7 @@ let cc_tactic depth additionnal_terms gls=
   let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
   let uf=forest state in
     match sol with
-	None -> tclFAIL 0 (str "congruence failed") gls  
+	None -> tclFAIL 0 (str "congruence failed") gls
       | Some reason ->
 	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
 	  match reason with
@@ -390,22 +390,22 @@ let cc_tactic depth additionnal_terms 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 
+		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 
+		       begin
+			 str "\"congruence with (" ++
+			 prlist_with_sep
 			   (fun () -> str ")" ++ pr_spc () ++ str "(")
 			   (print_constr_env (pf_env gls))
-			   terms_to_complete ++ 
+			   terms_to_complete ++
 			 str ")\","
 		       end);
 		  Pp.msgnl
@@ -417,18 +417,18 @@ let cc_tactic depth additionnal_terms gls=
 		  match dis.rule with
 		      Goal -> proof_tac p gls
 		    | Hyp id -> refute_tac id ta tb p gls
-		    | HeqG id -> 
+		    | HeqG id ->
 			convert_to_goal_tac id ta tb p gls
-		    | HeqnH (ida,idb) -> 
+		    | HeqnH (ida,idb) ->
 			convert_to_hyp_tac ida ta idb tb p gls
-		    
+
 
 let cc_fail gls =
-  errorlabstrm  "Congruence" (Pp.str "congruence failed.")     
+  errorlabstrm  "Congruence" (Pp.str "congruence failed.")
 
-let congruence_tac depth l = 
-  tclORELSE 
-    (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) 
+let congruence_tac depth l =
+  tclORELSE
+    (tclTHEN (tclREPEAT introf) (cc_tactic depth l))
     cc_fail
 
 (* Beware: reflexivity = constructor 1 = apply refl_equal
@@ -441,22 +441,22 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
 
    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. 
+   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 
+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 
+  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 []) 
+	      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
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 7cdd46ab4a..7ed077bda1 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-open Term 
+open Term
 open Proof_type
 
 val proof_tac: Ccproof.proof -> Proof_type.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index f23ed49b6e..d9db927a37 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -15,12 +15,12 @@ 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" integer(n) "with" ne_constr_list(l) ] ->
    [ congruence_tac n l ]
 END