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

20 files changed, 381 insertions, 381 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 87dd26779..bdc1f6b66 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -30,24 +30,24 @@ open Pattern
 open Tacexpr
 open Clenv
 
-    
+
 (* This function put casts around metavariables whose type could not be
  * infered by the refiner, that is head of applications, predicates and
  * subject of Cases.
  * Does check that the casted type is closed. Anyway, the refiner would
  * fail in this case... *)
 
-let clenv_cast_meta clenv = 
+let clenv_cast_meta clenv =
   let rec crec u =
     match kind_of_term u with
       | App _ | Case _ -> crec_hd u
       | Cast (c,_,_) when isMeta c -> u
       | _  -> map_constr crec u
-	    
+
   and crec_hd u =
     match kind_of_term (strip_outer_cast u) with
       | Meta mv ->
-	  (try 
+	  (try
             let b = Typing.meta_type clenv.evd mv in
 	    assert (not (occur_meta b));
 	    if occur_meta b then u
@@ -57,7 +57,7 @@ let clenv_cast_meta clenv =
       | Case(ci,p,c,br) ->
 	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
       | _ -> u
-  in 
+  in
   crec
 
 let clenv_value_cast_meta clenv =
@@ -73,14 +73,14 @@ let clenv_pose_dependent_evars with_evars clenv =
 
 let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
-  let evd' = 
-    if with_classes then 
-      Typeclasses.resolve_typeclasses ~fail:(not with_evars) 
-	clenv.env clenv.evd 
+  let evd' =
+    if with_classes then
+      Typeclasses.resolve_typeclasses ~fail:(not with_evars)
+	clenv.env clenv.evd
     else clenv.evd
   in
   tclTHEN
-    (tclEVARS evd') 
+    (tclEVARS evd')
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
@@ -105,7 +105,7 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
 open Unification
 
 let fail_quick_unif_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state; 
+  modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = false;
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
@@ -113,7 +113,7 @@ let fail_quick_unif_flags = {
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = 
+let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
   let evd' = w_unify false env CONV ~flags m n evd in
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index d02060fc0..20a95dabf 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -12,7 +12,7 @@ open Names
 open Util
 open Tacexpr
 
-type 'it statement = 
+type 'it statement =
     {st_label:name;
      st_it:'it}
 
@@ -41,12 +41,12 @@ type ('it,'constr,'tac) cut =
      cut_by: 'constr list option;
      cut_using: 'tac option}
 
-type ('var,'constr) hyp = 
-    Hvar of 'var 
+type ('var,'constr) hyp =
+    Hvar of 'var
   | Hprop of 'constr statement
 
-type ('constr,'tac) casee = 
-    Real of 'constr 
+type ('constr,'tac) casee =
+    Real of 'constr
   | Virtual of ('constr statement,'constr,'tac) cut
 
 type ('hyp,'constr,'pat,'tac) bare_proof_instr =
@@ -64,9 +64,9 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr =
   | Pfocus of 'constr statement
   | Pdefine of identifier * 'hyp list * 'constr
   | Pcast of identifier or_thesis * 'constr
-  | Psuppose of ('hyp,'constr) hyp list 
-  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) 
-  | Ptake of 'constr list 
+  | Psuppose of ('hyp,'constr) hyp list
+  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+  | Ptake of 'constr list
   | Pper of elim_type * ('constr,'tac) casee
   | Pend of block_type
   | Pescape
@@ -86,11 +86,11 @@ type raw_proof_instr =
 
 type glob_proof_instr =
     ((identifier*(Genarg.rawconstr_and_expr option)) located,
-     Genarg.rawconstr_and_expr,  
+     Genarg.rawconstr_and_expr,
      Topconstr.cases_pattern_expr,
      Tacexpr.glob_tactic_expr) gen_proof_instr
 
-type proof_pattern = 
+type proof_pattern =
     {pat_vars: Term.types statement list;
      pat_aliases: (Term.constr*Term.types) statement list;
      pat_constr: Term.constr;
@@ -100,6 +100,6 @@ type proof_pattern =
 
 type proof_instr =
     (Term.constr statement,
-     Term.constr, 
+     Term.constr,
      proof_pattern,
      Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index cdb7b0675..a32b9777b 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -15,9 +15,9 @@ open Util
 
 let daimon_flag = ref false
 
-let set_daimon_flag () = daimon_flag:=true 
+let set_daimon_flag () = daimon_flag:=true
 let clear_daimon_flag () = daimon_flag:=false
-let get_daimon_flag () = !daimon_flag 
+let get_daimon_flag () = !daimon_flag
 
 type command_mode =
     Mode_tactic
@@ -27,12 +27,12 @@ type command_mode =
 let mode_of_pftreestate pts =
   let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
     if goal.evar_extra = None then
-      Mode_tactic 
+      Mode_tactic
     else
       Mode_proof
-	  
+
 let get_current_mode () =
-  try 
+  try
     mode_of_pftreestate (Pfedit.get_pftreestate ())
   with _ -> Mode_none
 
@@ -42,7 +42,7 @@ let check_not_proof_mode str =
 
 type split_tree=
     Skip_patt of Idset.t * split_tree
-  | Split_patt of Idset.t * inductive * 
+  | Split_patt of Idset.t * inductive *
 		(bool array * (Idset.t * split_tree) option) array
   | Close_patt of split_tree
   | End_patt of (identifier * int)
@@ -54,7 +54,7 @@ type elim_kind =
 
 type recpath = int option*Declarations.wf_paths
 
-type per_info = 
+type per_info =
     {per_casee:constr;
      per_ctype:types;
      per_ind:inductive;
@@ -64,7 +64,7 @@ type per_info =
      per_nparams:int;
      per_wf:recpath}
 
-type stack_info = 
+type stack_info =
     Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
   | Suppose_case
   | Claim
@@ -73,7 +73,7 @@ type stack_info =
 type pm_info =
     { pm_stack : stack_info list}
 
-let pm_in,pm_out = Dyn.create "pm_info" 
+let pm_in,pm_out = Dyn.create "pm_info"
 
 let get_info gl=
   match gl.evar_extra with
@@ -81,30 +81,30 @@ let get_info gl=
     | Some extra ->
 	try pm_out extra with _ -> invalid_arg "get_info"
 
-let get_stack pts = 
+let get_stack pts =
   let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
     info.pm_stack
 
-let get_top_stack pts = 
+let get_top_stack pts =
   let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
     info.pm_stack
 
 let get_end_command pts =
-  match mode_of_pftreestate pts with 
+  match mode_of_pftreestate pts with
       Mode_proof ->
-	Some 
+	Some
 	  begin
 	    match get_top_stack pts with
 		[] -> "\"end proof\""
 	      | Claim::_ -> "\"end claim\""
 	      | Focus_claim::_-> "\"end focus\""
-	      | (Suppose_case :: Per (et,_,_,_) :: _ 
-		| Per (et,_,_,_) :: _ ) -> 
+	      | (Suppose_case :: Per (et,_,_,_) :: _
+		| Per (et,_,_,_) :: _ ) ->
 		  begin
 		    match et with
-			Decl_expr.ET_Case_analysis -> 
+			Decl_expr.ET_Case_analysis ->
 			  "\"end cases\" or start a new case"
-		      | Decl_expr.ET_Induction -> 
+		      | Decl_expr.ET_Induction ->
 			  "\"end induction\" or start a new case"
 		  end
 	      | _ -> anomaly "lonely suppose"
@@ -112,7 +112,7 @@ let get_end_command pts =
     | Mode_tactic ->
 	begin
 	  try
-	    ignore 
+	    ignore
 	      (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
 	    Some "\"return\""
 	  with Not_found -> None
@@ -120,7 +120,7 @@ let get_end_command pts =
     | Mode_none ->
         error "no proof in progress"
 
-let get_last env =  
-  try 
+let get_last env =
+  try
     let (id,_,_) =  List.hd (Environ.named_context env) in id
   with Invalid_argument _ -> error "no previous statement to use"
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index 6be3abdfe..e225c828d 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -23,7 +23,7 @@ type command_mode =
   | Mode_none
 
 val mode_of_pftreestate : pftreestate -> command_mode
-    
+
 val get_current_mode : unit -> command_mode
 
 val check_not_proof_mode : string -> unit
@@ -42,7 +42,7 @@ type elim_kind =
 
 type recpath = int option*Declarations.wf_paths
 
-type per_info = 
+type per_info =
     {per_casee:constr;
      per_ctype:types;
      per_ind:inductive;
@@ -52,7 +52,7 @@ type per_info =
      per_nparams:int;
      per_wf:recpath}
 
-type stack_info = 
+type stack_info =
     Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
   | Suppose_case
   | Claim
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d7a1232ad..25c668f5d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -29,7 +29,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
-      user_err_loc 
+      user_err_loc
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
@@ -37,10 +37,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
 
 (* vernac command Existential *)
 
-let instantiate_pf_com n com pfts = 
+let instantiate_pf_com n com pfts =
   let gls = top_goal_of_pftreestate pfts in
-  let sigma = gls.sigma in 
-  let (evk,evi) = 
+  let sigma = gls.sigma in
+  let (evk,evi) =
     let evl = Evarutil.non_instantiated sigma in
       if (n <= 0) then
 	error "incorrect existential variable index"
@@ -48,8 +48,8 @@ let instantiate_pf_com n com pfts =
 	  error "not so many uninstantiated existential variables"
       else
 	List.nth evl (n-1)
-  in 
+  in
   let env = Evd.evar_env evi in
-  let rawc = Constrintern.intern_constr sigma env com in 
+  let rawc = Constrintern.intern_constr sigma env com in
   let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
   change_constraints_pftreestate sigma' pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a35a9b58b..ab0fdf831 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -20,10 +20,10 @@ open Rawterm
 
 (* Refinement of existential variables. *)
 
-val w_refine : evar * evar_info -> 
+val w_refine : evar * evar_info ->
   (var_map * unbound_ltac_var_map) * rawconstr -> evar_defs -> evar_defs
 
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate
 
-(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) 
+(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f1f33930e..eddf387f9 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -28,7 +28,7 @@ open Type_errors
 open Retyping
 open Evarutil
 open Tacexpr
- 
+
 type refiner_error =
 
   (* Errors raised by the refiner *)
@@ -50,7 +50,7 @@ open Pretype_errors
 let rec catchable_exception = function
   | Stdpp.Exc_located(_,e) -> catchable_exception e
   | LtacLocated(_,e) -> catchable_exception e
-  | Util.UserError _ | TypeError _ 
+  | Util.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
   (* unification errors *)
@@ -58,7 +58,7 @@ let rec catchable_exception = function
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
-  | Typeclasses_errors.TypeClassError 
+  | Typeclasses_errors.TypeClassError
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
   | _ -> false
 
@@ -73,19 +73,19 @@ let with_check = Flags.with_option check
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
 let apply_to_hyp sign id f =
-  try apply_to_hyp sign id f 
-  with Hyp_not_found -> 
+  try apply_to_hyp sign id f
+  with Hyp_not_found ->
     if !check then error "No such assumption."
     else sign
 
 let apply_to_hyp_and_dependent_on sign id f g =
-  try apply_to_hyp_and_dependent_on sign id f g 
-  with Hyp_not_found -> 
+  try apply_to_hyp_and_dependent_on sign id f g
+  with Hyp_not_found ->
     if !check then error "No such assumption."
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = type_of env sigma c in () 
+  if !check then let _ = type_of env sigma c in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -111,7 +111,7 @@ let recheck_typability (what,id) env sigma t =
       | Some id -> "hypothesis "^(string_of_id id) in
     error
       ("The correctness of "^s^" relies on the body of "^(string_of_id id))
-  
+
 let remove_hyp_body env sigma id =
   let sign =
     apply_to_hyp_and_dependent_on (named_context_val env) id
@@ -121,7 +121,7 @@ let remove_hyp_body env sigma id =
 	| Some c ->(id,None,t))
       (fun (id',c,t as d) sign ->
 	(if !check then
-	  begin 
+	  begin
 	    let env = reset_with_named_context sign env in
 	    match c with
 	    | None ->  recheck_typability (Some id',id) env sigma t
@@ -130,7 +130,7 @@ let remove_hyp_body env sigma id =
 		recheck_typability (Some id',id) env sigma b'
 	  end;d))
   in
-  reset_with_named_context sign env 
+  reset_with_named_context sign env
 
 (* Reordering of the context *)
 
@@ -138,7 +138,7 @@ let remove_hyp_body env sigma id =
 (* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
 (* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
 (* reculees par rapport aux autres (faire le contraire!) *)
- 
+
 let mt_q = (Idmap.empty,[])
 let push_val y = function
     (_,[] as q) -> q
@@ -211,8 +211,8 @@ let check_decl_position env sign (x,_,_ as d) =
 (* Auxiliary functions for primitive MOVE tactic
  *
  * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
- * hyp [hfrom] at location [hto] which belongs to the hyps on the 
- * left side [left] of the full signature if [toleft=true] or to the hyps 
+ * hyp [hfrom] at location [hto] which belongs to the hyps on the
+ * left side [left] of the full signature if [toleft=true] or to the hyps
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
@@ -228,17 +228,17 @@ let split_sign hfrom hto l =
   let rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
     | (hyp,c,typ) as d :: right ->
-      	if hyp = hfrom then 
+      	if hyp = hfrom then
 	  (left,right,d, toleft or hto = MoveToEnd true)
       	else
-	  splitrec (d::left) 
+	  splitrec (d::left)
 	    (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp)
 	    right
-  in 
+  in
     splitrec [] false l
 
 let hyp_of_move_location = function
-  | MoveAfter id -> id 
+  | MoveAfter id -> id
   | MoveBefore id -> id
   | _ -> assert false
 
@@ -258,12 +258,12 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	List.rev first @ List.rev middle @ right
     | (hyp,_,_) as d :: right ->
 	let (first',middle') =
-      	  if List.exists (test_dep d) middle then 
-	    if with_dep & hto <> MoveAfter hyp then 
+      	  if List.exists (test_dep d) middle then
+	    if with_dep & hto <> MoveAfter hyp then
 	      (first, d::middle)
-            else 
+            else
 	      errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++
-	        pr_move_location pr_id hto ++ 
+	        pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
           else
@@ -271,16 +271,16 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	in
       	if hto = MoveAfter hyp then
 	  List.rev first' @ List.rev middle' @ right
-      	else 
+      	else
 	  moverec first' middle' right
   in
-  if toleft then 
-    let right = 
+  if toleft then
+    let right =
       List.fold_right push_named_context_val right empty_named_context_val in
     List.fold_left (fun sign d -> push_named_context_val d sign)
-      right (moverec [] [declfrom] left) 
-  else 
-    let right = 
+      right (moverec [] [declfrom] left)
+  else
+    let right =
       List.fold_right push_named_context_val
 	(moverec [] [declfrom] right) empty_named_context_val in
     List.fold_left (fun sign d -> push_named_context_val d sign)
@@ -295,7 +295,7 @@ let rename_hyp id1 id2 sign =
 (************************************************************************)
 (* Implementation of the logical rules *)
 
-(* Will only be used on terms given to the Refine rule which have meta 
+(* Will only be used on terms given to the Refine rule which have meta
 variables only in Application and Case *)
 
 let error_unsupported_deep_meta c =
@@ -303,7 +303,7 @@ let error_unsupported_deep_meta c =
     strbrk "form contains metavariables deep inside the term is not " ++
     strbrk "supported; try \"refine\" instead.")
 
-let collect_meta_variables c = 
+let collect_meta_variables c =
   let rec collrec deep acc c = match kind_of_term c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
@@ -312,12 +312,12 @@ let collect_meta_variables c =
   in
   List.rev (collrec false [] c)
 
-let check_meta_variables c = 
+let check_meta_variables c =
   if not (list_distinct (collect_meta_variables c)) then
     raise (RefinerError (NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
-  if !check & not (is_conv_leq env sigma ty conclty) then 
+  if !check & not (is_conv_leq env sigma ty conclty) then
     raise (RefinerError (BadType (arg,ty,conclty)))
 
 let goal_type_of env sigma c =
@@ -329,7 +329,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
 (*
    if  not (occur_meta trm) then
-    let t'ty = (unsafe_machine env sigma trm).uj_type in 	
+    let t'ty = (unsafe_machine env sigma trm).uj_type in
     let _ = conv_leq_goal env sigma trm t'ty conclty in
       (goalacc,t'ty)
   else
@@ -352,9 +352,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	    | Ind _ | Const _
 		when (isInd f or has_polymorphic_type (destConst f)) ->
 		(* Sort-polymorphism of definition and inductive types *)
-		goalacc, 
+		goalacc,
                 type_of_global_reference_knowing_conclusion env sigma f conclty
-	    | _ -> 
+	    | _ ->
 		mk_hdgoals sigma goal goalacc f
 	in
 	let (acc'',conclty') =
@@ -365,14 +365,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | Case (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	check_conv_leq_goal env sigma trm conclty' conclty;
-	let acc'' = 
+	let acc'' =
 	  array_fold_left2
             (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
-            acc' lbrty lf 
+            acc' lbrty lf
 	in
 	(acc'',conclty')
 
-    | _ -> 
+    | _ ->
 	if occur_meta trm then
 	  anomaly "refiner called with a meta in non app/case subterm";
 
@@ -397,8 +397,8 @@ and mk_hdgoals sigma goal goalacc trm =
 	mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-	let (acc',hdty) = 
-	  if isInd f or isConst f 
+	let (acc',hdty) =
+	  if isInd f or isConst f
 	     & not (array_exists occur_meta l) (* we could be finer *)
 	  then
 	    (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
@@ -408,10 +408,10 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | Case (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
-	let acc'' = 
+	let acc'' =
 	  array_fold_left2
             (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
-            acc' lbrty lf 
+            acc' lbrty lf
 	in
 	(acc'',conclty')
 
@@ -434,7 +434,7 @@ and mk_arggoals sigma goal goalacc funty = function
 
 and mk_casegoals sigma goal goalacc p c =
   let env = evar_env goal in
-  let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
+  let (acc',ct) = mk_hdgoals sigma goal goalacc c in
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let indspec =
     try find_mrectype env sigma ct
@@ -466,7 +466,7 @@ let norm_goal sigma gl =
   let red_fun = Evarutil.nf_evar sigma in
   let ncl = red_fun gl.evar_concl in
   let ngl =
-    { gl with 
+    { gl with
 	evar_concl = ncl;
 	evar_hyps = map_named_val red_fun gl.evar_hyps } in
     if Evd.eq_evar_info ngl gl then None else Some ngl
@@ -499,7 +499,7 @@ let prim_refiner r sigma goal =
 	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
-	
+
     | Cut (b,replace,id,t) ->
         let sg1 = mk_goal sign (nf_betaiota sigma t) in
 	let sign,cl,sigma =
@@ -517,52 +517,52 @@ let prim_refiner r sigma goal =
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
     | FixRule (f,n,rest,j) ->
-     	let rec check_ind env k cl = 
-          match kind_of_term (strip_outer_cast cl) with 
-            | Prod (na,c1,b) -> 
-            	if k = 1 then 
-		  try 
+     	let rec check_ind env k cl =
+          match kind_of_term (strip_outer_cast cl) with
+            | Prod (na,c1,b) ->
+            	if k = 1 then
+		  try
 		    fst (find_inductive env sigma c1)
-		  with Not_found -> 
+		  with Not_found ->
 		    error "Cannot do a fixpoint on a non inductive type."
-            	else 
+            	else
 		  check_ind (push_rel (na,None,c1) env) (k-1) b
             | _ -> error "Not enough products."
 	in
 	let (sp,_) = check_ind env n cl in
 	let firsts,lasts = list_chop j rest in
 	let all = firsts@(f,n,cl)::lasts in
-     	let rec mk_sign sign = function 
+     	let rec mk_sign sign = function
 	  | (f,n,ar)::oth ->
-	      let (sp',_)  = check_ind env n ar in 
-	      if not (sp=sp') then 
-		error ("Fixpoints should be on the same " ^ 
+	      let (sp',_)  = check_ind env n ar in
+	      if not (sp=sp') then
+		error ("Fixpoints should be on the same " ^
 		       "mutual inductive declaration.");
 	      if !check && mem_named_context f (named_context_of_val sign) then
 		error
 		  ("Name "^string_of_id f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
-	  | [] -> 
+	  | [] ->
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
-	in 
+	in
 	  (mk_sign sign all, sigma)
-	
+
     | Cofix (f,others,j) ->
-     	let rec check_is_coind env cl = 
+     	let rec check_is_coind env cl =
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
             | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
-            | _ -> 
-		try 
+            | _ ->
+		try
 		  let _ = find_coinductive env sigma b in ()
-                with Not_found -> 
+                with Not_found ->
 		  error ("All methods must construct elements " ^
 			  "in coinductive types.")
 	in
 	let firsts,lasts = list_chop j others in
 	let all = firsts@(f,cl)::lasts in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
-        let rec mk_sign sign = function 
+        let rec mk_sign sign = function
           | (f,ar)::oth ->
 	      (try
                 (let _ = lookup_named_val f sign in
@@ -571,7 +571,7 @@ let prim_refiner r sigma goal =
               |	Not_found ->
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
 	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
-     	in 
+     	in
 	  (mk_sign sign all, sigma)
 
     | Refine c ->
@@ -586,17 +586,17 @@ let prim_refiner r sigma goal =
 	if (not !check) || is_conv_leq env sigma cl' cl then
           let sg = mk_goal sign cl' in
           ([sg], sigma)
-	else 
+	else
 	  error "convert-concl rule passed non-converting term"
 
     | Convert_hyp (id,copt,ty) ->
 	([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
 
     (* And now the structural rules *)
-    | Thin ids -> 
+    | Thin ids ->
 	let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
 	  ([mk_goal hyps concl], nsigma)
-	
+
     | ThinBody ids ->
 	let clear_aux env id =
           let env' = remove_hyp_body env sigma id in
@@ -608,9 +608,9 @@ let prim_refiner r sigma goal =
      	  ([sg], sigma)
 
     | Move (withdep, hfrom, hto) ->
-  	let (left,right,declfrom,toleft) = 
+  	let (left,right,declfrom,toleft) =
 	  split_sign hfrom hto (named_context_of_val sign) in
-  	let hyps' = 
+  	let hyps' =
 	  move_hyp withdep toleft (left,declfrom,right) hto in
   	  ([mk_goal hyps' cl], sigma)
 
@@ -641,7 +641,7 @@ type variable_proof_status = ProofVar | SectionVar of identifier
 
 type proof_variable = name * variable_proof_status
 
-let subst_proof_vars = 
+let subst_proof_vars =
   let rec aux p vars =
     let _,subst =
       List.fold_left (fun (n,l) var ->
@@ -652,22 +652,22 @@ let subst_proof_vars =
         (n+1,t)) (p,[]) vars
     in replace_vars (List.rev subst)
   in aux 1
-         
+
 let rec rebind id1 id2 = function
   | [] -> [Name id2,SectionVar id1]
-  | (na,k as x)::l -> 
+  | (na,k as x)::l ->
       if na = Name id1 then (Name id2,k)::l else
         let l' = rebind id1 id2 l in
         if na = Name id2 then (Anonymous,k)::l' else x::l'
 
 let add_proof_var id vl = (Name id,ProofVar)::vl
 
-let proof_variable_index x = 
+let proof_variable_index x =
   let rec aux n = function
     | (Name id,ProofVar)::l when x = id -> n
     | _::l ->  aux (n+1) l
     | [] -> raise Not_found
-  in 
+  in
   aux 1
 
 let prim_extractor subfun vl pft =
@@ -683,7 +683,7 @@ let prim_extractor subfun vl pft =
 		let cty = subst_proof_vars vl ty in
 		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
 	    | _ -> error "Incomplete proof!")
-	    
+
       | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) ->
           let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
 	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
@@ -698,7 +698,7 @@ let prim_extractor subfun vl pft =
 	  let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
             (add_proof_var f vl) others in
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkFix ((vn,j),(names,lcty,lfix))	
+	    mkFix ((vn,j),(names,lcty,lfix))
 
       | Some (Prim (Cofix (f,others,j)),spfl) ->
 	  let firsts,lasts = list_chop j others in
@@ -706,14 +706,14 @@ let prim_extractor subfun vl pft =
 	  let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
 	  let names  = Array.map (fun (f,_) -> Name f) all in
 	  let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
-            (add_proof_var f vl) others in 
+            (add_proof_var f vl) others in
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
 	    mkCoFix (j,(names,lcty,lfix))
-	      
+
       | Some (Prim (Refine c),spfl) ->
 	  let mvl = collect_meta_variables c in
 	  let metamap = List.combine mvl (List.map (subfun vl) spfl) in
-	  let cc = subst_proof_vars vl c in 
+	  let cc = subst_proof_vars vl c in
 	    plain_instance metamap cc
 
       (* Structural and conversion rules do not produce any proof *)
@@ -726,10 +726,10 @@ let prim_extractor subfun vl pft =
       | Some (Prim (Thin _),[pf]) ->
 	  (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
 	  subfun vl pf
-	    
+
       | Some (Prim (ThinBody _),[pf]) ->
 	  subfun vl pf
-	    
+
       | Some (Prim (Move _|Order _),[pf]) ->
 	  subfun vl pf
 
@@ -742,4 +742,4 @@ let prim_extractor subfun vl pft =
       | Some _ -> anomaly "prim_extractor"
 
       | None-> error "prim_extractor handed incomplete proof"
-	  
+
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 8bc48ed54..0d56da382 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -26,9 +26,9 @@ val with_check    : tactic -> tactic
   [Intro]: no check that the name does not exist\\
   [Intro_after]: no check that the name does not exist and that variables in
      its type does not escape their scope\\
-  [Intro_replacing]: no check that the name does not exist and that 
+  [Intro_replacing]: no check that the name does not exist and that
      variables in its type does not escape their scope\\
-  [Convert_hyp]: 
+  [Convert_hyp]:
   no check that the name exist and that its type is convertible\\
 *)
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 62668f7f3..11324ede9 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -81,26 +81,26 @@ let get_current_goal_context () = get_goal_context 1
 
 let set_current_proof = Edit.focus proof_edits
 
-let resume_proof (loc,id) = 
-  try 
+let resume_proof (loc,id) =
+  try
     Edit.focus proof_edits id
   with Invalid_argument "Edit.focus" ->
     user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
 
 let suspend_proof () =
-  try 
+  try
     Edit.unfocus proof_edits
   with Invalid_argument "Edit.unfocus" ->
     errorlabstrm "Pfedit.suspend_current_proof"
       (str"No active proof" ++ (msg_proofs true))
-      
+
 let resume_last_proof () =
   match (Edit.last_focused proof_edits) with
     | None ->
         errorlabstrm "resume_last" (str"No proof-editing in progress.")
-    | Some p -> 
+    | Some p ->
 	Edit.focus proof_edits p
-	  
+
 let get_current_proof_name () =
   match Edit.read proof_edits with
     | None ->
@@ -114,14 +114,14 @@ let add_proof (na,pfs,ts) =
 let delete_proof_gen = Edit.delete proof_edits
 
 let delete_proof (loc,id) =
-  try 
+  try
     delete_proof_gen id
   with (UserError ("Edit.delete",_)) ->
     user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
-      
+
 let mutate f =
-  try 
+  try
     Edit.mutate proof_edits (fun _ pfs -> f pfs)
   with Invalid_argument "Edit.mutate" ->
     errorlabstrm "Pfedit.mutate"
@@ -131,31 +131,31 @@ let start (na,ts) =
   let pfs = mk_pftreestate ts.top_goal in
   let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
   add_proof(na,pfs,ts)
-    
+
 let restart_proof () =
   match Edit.read proof_edits with
-    | None -> 
+    | None ->
 	errorlabstrm "Pfedit.restart"
           (str"No focused proof to restart" ++ msg_proofs true)
-    | Some(na,_,ts) -> 
+    | Some(na,_,ts) ->
 	delete_proof_gen na;
         start (na,ts);
         set_current_proof na
 
 let proof_term () =
   extract_pftreestate (get_pftreestate())
-    
+
 (* Detect is one has completed a subtree of the initial goal *)
-let subtree_solved () = 
+let subtree_solved () =
   let pts = get_pftreestate () in
-  is_complete_proof (proof_of_pftreestate pts) & 
+  is_complete_proof (proof_of_pftreestate pts) &
   not (is_top_pftreestate pts)
 
-let tree_solved () = 
+let tree_solved () =
   let pts = get_pftreestate () in
   is_complete_proof (proof_of_pftreestate pts)
 
-let top_tree_solved () = 
+let top_tree_solved () =
   let pts = get_pftreestate () in
   is_complete_proof (proof_of_pftreestate (top_of_tree pts))
 
@@ -165,19 +165,19 @@ let top_tree_solved () =
 
 let set_undo = function
   | None -> undo_limit := undo_default
-  | Some n -> 
-      if n>=0 then 
+  | Some n ->
+      if n>=0 then
 	undo_limit := n
-      else 
+      else
 	error "Cannot set a negative undo limit"
 
 let get_undo () = Some !undo_limit
 
 let undo n =
-  try 
-    Edit.undo proof_edits n; 
-       (* needed because the resolution of a subtree is done in 2 steps 
-       then a sequence of undo can lead to a focus on a completely solved 
+  try
+    Edit.undo proof_edits n;
+       (* needed because the resolution of a subtree is done in 2 steps
+       then a sequence of undo can lead to a focus on a completely solved
        subtree - this solution only works properly if undoing one step *)
     if subtree_solved() then  Edit.undo proof_edits 1
   with (Invalid_argument "Edit.undo") ->
@@ -186,14 +186,14 @@ let undo n =
 (* Undo current focused proof to reach depth [n]. This is used in
    [vernac_backtrack]. *)
 let undo_todepth n =
-  try 
+  try
     Edit.undo_todepth proof_edits n
   with (Invalid_argument "Edit.undo") ->
     errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
 
 (* Return the depth of the current focused proof stack, this is used
    to put informations in coq prompt (in emacs mode). *)
-let current_proof_depth() = 
+let current_proof_depth() =
   try
     Edit.depth proof_edits
   with (Invalid_argument "Edit.depth") -> -1
@@ -206,7 +206,7 @@ let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
 
 let cook_proof k =
-  let (pfs,ts) = get_state() 
+  let (pfs,ts) = get_state()
   and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal
   and strength = ts.top_strength in
@@ -220,19 +220,19 @@ let cook_proof k =
       const_entry_boxed = false},
     ts.top_compute_guard, strength, ts.top_hook))
 
-let current_proof_statement () = 
+let current_proof_statement () =
   let ts = get_topstate() in
-  (get_current_proof_name (), ts.top_strength, 
+  (get_current_proof_name (), ts.top_strength,
    ts.top_goal.evar_concl, ts.top_hook)
 
 (*********************************************************************)
 (*              Abort   functions                                    *)
 (*********************************************************************)
- 
+
 let refining () = [] <> (Edit.dom proof_edits)
 
 let check_no_pending_proofs () =
-  if refining () then 
+  if refining () then
     errorlabstrm "check_no_pending_proofs"
       (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
          str"Use \"Abort All\" first or complete proof(s).")
@@ -254,7 +254,7 @@ let set_end_tac tac =
 
 let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
   let top_goal = mk_goal sign concl None in
-  let ts = { 
+  let ts = {
     top_end_tac = None;
     top_init_tac = init_tac;
     top_compute_guard = compute_guard;
@@ -269,7 +269,7 @@ let solve_nth k tac =
   let pft = get_pftreestate () in
   if not (List.mem (-1) (cursor_of_pftreestate pft)) then
     mutate (solve_nth_pftreestate k tac)
-  else 
+  else
     error "cannot apply a tactic when we are descended behind a tactic-node"
 
 let by tac = mutate (solve_pftreestate tac)
@@ -278,7 +278,7 @@ let instantiate_nth_evar_com n c =
   mutate (Evar_refiner.instantiate_pf_com n c)
 
 let traverse n = mutate (traverse n)
- 
+
 (* [traverse_to path]
 
    Traverses the current proof to get to the location specified by
@@ -296,7 +296,7 @@ let common_ancestor l1 l2 =
       | _, _ -> List.rev l1, List.length l2
   in
   common_aux (List.rev l1) (List.rev l2)
-      
+
 let rec traverse_up = function
   | 0 -> (function pf -> pf)
   | n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf))
@@ -326,11 +326,11 @@ let make_focus n = focus_n := n
 let focus () = !focus_n
 let focused_goal () = let n = !focus_n in if n=0 then 1 else n
 
-let reset_top_of_tree () = 
+let reset_top_of_tree () =
   mutate top_of_tree
- 
-let reset_top_of_script () = 
-  mutate (fun pts -> 
+
+let reset_top_of_script () =
+  mutate (fun pts ->
 	try
 	 up_until_matching_rule is_proof_instr pts
 	with Not_found -> top_of_tree pts)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9a40ba319..8dcd8edc2 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -78,7 +78,7 @@ val get_undo : unit -> int option
     systematically apply at initialization time (e.g. to start the
     proof of mutually dependent theorems) *)
 
-val start_proof : 
+val start_proof :
   identifier -> goal_kind -> named_context_val -> constr ->
     ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
 
@@ -107,7 +107,7 @@ val suspend_proof : unit -> unit
     it fails if there is no current proof of if it is not completed;
     it also tells if the guardness condition has to be inferred. *)
 
-val cook_proof : (Refiner.pftreestate -> unit) -> 
+val cook_proof : (Refiner.pftreestate -> unit) ->
   identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 2e2f23065..b5f46d788 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -33,8 +33,8 @@ let is_bind = function
 
 (* Functions on goals *)
 
-let mk_goal hyps cl extra = 
-  { evar_hyps = hyps; evar_concl = cl; 
+let mk_goal hyps cl extra =
+  { evar_hyps = hyps; evar_concl = cl;
     evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
     evar_body = Evar_empty; evar_extra = extra }
 
@@ -48,9 +48,9 @@ let ref_of_proof pf =
 let rule_of_proof pf =
   let (r,_) = ref_of_proof pf in r
 
-let children_of_proof pf = 
+let children_of_proof pf =
   let (_,cl) = ref_of_proof pf in cl
-				    
+
 let goal_of_proof pf = pf.goal
 
 let subproof_of_proof pf = match pf.ref with
@@ -74,7 +74,7 @@ let pf_lookup_name_as_renamed env ccl s =
 let pf_lookup_index_as_renamed env ccl n =
   Detyping.lookup_index_as_renamed env ccl n
 
-(* Functions on rules (Proof mode) *) 
+(* Functions on rules (Proof mode) *)
 
 let is_dem_rule  = function
     Decl_proof _  -> true
@@ -85,9 +85,9 @@ let is_proof_instr = function
   | _ -> false
 
 let is_focussing_command = function
-    Decl_proof b -> b 
-  | Nested (Proof_instr (b,_),_) -> b 
-  | _ -> false   
+    Decl_proof b -> b
+  | Nested (Proof_instr (b,_),_) -> b
+  | _ -> false
 
 
 (*********************************************************************)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 8a466d8df..29417e8b6 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -48,11 +48,11 @@ type proof_tree = {
 
 and rule =
   | Prim of prim_rule
-  | Nested of compound_rule * proof_tree 
+  | Nested of compound_rule * proof_tree
   | Decl_proof of bool
   | Daimon
 
-and compound_rule=  
+and compound_rule=
   | Tactic of tactic_expr * bool
   | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
 
@@ -92,7 +92,7 @@ and tactic_arg =
    glob_tactic_expr)
      Tacexpr.gen_tactic_arg
 
-type ltac_call_kind = 
+type ltac_call_kind =
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9db87d22e..4a7cb2f93 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -32,7 +32,7 @@ type prim_rule =
   | FixRule of identifier * int * (identifier * int * constr) list * int
   | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
-  | Convert_concl of types * cast_kind 
+  | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
   | Thin of identifier list
   | ThinBody of identifier list
@@ -58,7 +58,7 @@ type prim_rule =
                                     lc     : [Set of evars occurring
                                               in the type of evar] } };
                ...
-               number of last evar, 
+               number of last evar,
                it = { evar_concl = [the type of evar]
                       evar_hyps = [the context of the evar]
                       evar_body = [the body of the Evar if any]
@@ -69,11 +69,11 @@ type prim_rule =
 \end{verbatim}
 *)
 
-(*s Proof trees. 
-  [ref] = [None] if the goal has still to be proved, 
+(*s Proof trees.
+  [ref] = [None] if the goal has still to be proved,
   and [Some (r,l)] if the rule [r] was applied to the goal
-  and gave [l] as subproofs to be completed. 
-  if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof 
+  and gave [l] as subproofs to be completed.
+  if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
   that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
   open_subgoals : int;
@@ -82,11 +82,11 @@ type proof_tree = {
 
 and rule =
   | Prim of prim_rule
-  | Nested of compound_rule * proof_tree 
+  | Nested of compound_rule * proof_tree
   | Decl_proof of bool
   | Daimon
 
-and compound_rule= 
+and compound_rule=
   (* the boolean of Tactic tells if the default tactic is used *)
   | Tactic of tactic_expr * bool
   | Proof_instr of bool * proof_instr
@@ -127,7 +127,7 @@ and tactic_arg =
    glob_tactic_expr)
      Tacexpr.gen_tactic_arg
 
-type ltac_call_kind = 
+type ltac_call_kind =
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8efc26631..880efc2d0 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -40,14 +40,14 @@ let set_strategy_one ref l  =
         let cb = Global.lookup_constant sp in
         if cb.const_body <> None & cb.const_opaque then
           errorlabstrm "set_transparent_const"
-            (str "Cannot make" ++ spc () ++ 
+            (str "Cannot make" ++ spc () ++
             Nametab.pr_global_env Idset.empty (ConstRef sp) ++
             spc () ++ str "transparent because it was declared opaque.");
         Csymtable.set_transparent_const sp
     | _ -> ()
 
 let cache_strategy (_,str) =
-  List.iter 
+  List.iter
     (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
     str
 
@@ -62,7 +62,7 @@ let subst_strategy (_,subs,(local,obj)) =
 
 let map_strategy f l =
   let l'  = List.fold_right
-    (fun (lev,ql) str -> 
+    (fun (lev,ql) str ->
       let ql' = List.fold_right
         (fun q ql ->
           match f q with
@@ -77,12 +77,12 @@ let export_strategy (local,obj) =
       EvalVarRef _ -> None
     | EvalConstRef _ as q -> Some q) obj
 
-let classify_strategy (local,_ as obj) = 
+let classify_strategy (local,_ as obj) =
   if local then Dispose else Substitute obj
 
 let disch_ref ref =
   match ref with
-      EvalConstRef c -> 
+      EvalConstRef c ->
         let c' = Lib.discharge_con c in
         if c==c' then Some ref else Some (EvalConstRef c')
     | _ -> Some ref
@@ -104,7 +104,7 @@ let (inStrategy,outStrategy) =
 let set_strategy local str =
   Lib.add_anonymous_leaf (inStrategy (local,str))
 
-let _ = 
+let _ =
   Summary.declare_summary "Transparent constants and variables"
     { Summary.freeze_function = Conv_oracle.freeze;
       Summary.unfreeze_function = Conv_oracle.unfreeze;
@@ -139,13 +139,13 @@ let make_flag f =
 	  f.rConst red
   in red
 
-let is_reference c = 
+let is_reference c =
   try let _ref = global_of_constr c in true with _ -> false
 
 let red_expr_tab = ref Stringmap.empty
 
 let declare_red_expr s f =
-  try 
+  try
     let _ = Stringmap.find s !red_expr_tab in
     error ("There is already a reduction expression of name "^s)
   with Not_found ->
@@ -159,8 +159,8 @@ let out_with_occurrences ((b,l),c) =
   ((b,List.map out_arg l), c)
 
 let reduction_of_red_expr = function
-  | Red internal -> 
-      if internal then (try_red_product,DEFAULTcast) 
+  | Red internal ->
+      if internal then (try_red_product,DEFAULTcast)
       else (red_product,DEFAULTcast)
   | Hnf -> (hnf_constr,DEFAULTcast)
   | Simpl (Some (_,c as lp)) ->
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8b3789c3b..c66e9c84b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -49,7 +49,7 @@ let descend n p =
     | None        -> error "It is a leaf."
     | Some(r,pfl) ->
     	if List.length pfl >= n then
-	  (match list_chop (n-1) pfl with 
+	  (match list_chop (n-1) pfl with
 	     | left,(wanted::right) ->
 		 (wanted,
 		  (fun pfl' ->
@@ -58,11 +58,11 @@ let descend n p =
                     let pf'       = List.hd pfl' in
                     let spfl      = left@(pf'::right) in
                     let newstatus = and_status (List.map pf_status spfl) in
-                    { p with 
+                    { p with
 			open_subgoals = newstatus;
 			ref           = Some(r,spfl) }))
 	     | _ -> assert false)
-    	else 
+    	else
 	  error "Too few subproofs"
 
 
@@ -72,28 +72,28 @@ let descend n p =
    (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ]
  *)
 
-let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) 
+let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
                     (l : proof_tree list) =
   match nl with
     | [] -> []
     | h::t ->
-	let m,l = list_chop h l in 
+	let m,l = list_chop h l in
 	(List.hd fl m) :: (mapshape t (List.tl fl) l)
 
 (* [frontier : proof_tree -> goal list * validation]
    given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals
-   to be solved to complete the proof, and [v] is the corresponding 
+   to be solved to complete the proof, and [v] is the corresponding
    validation *)
-   
+
 let rec frontier p =
   match p.ref with
-    | None -> 
+    | None ->
 	([p.goal],
-	 (fun lp' -> 
+	 (fun lp' ->
 	    let p' = List.hd lp' in
-            if Evd.eq_evar_info p'.goal p.goal then 
+            if Evd.eq_evar_info p'.goal p.goal then
 	      p'
-            else 
+            else
 	      errorlabstrm "Refiner.frontier"
                 (str"frontier was handed back a ill-formed proof.")))
     | Some(r,pfl) ->
@@ -115,14 +115,14 @@ let set_solve_hook = (:=) solve_hook
 let rec frontier_map_rec f n p =
   if n < 1 || n > p.open_subgoals then p else
   match p.ref with
-    | None -> 
+    | None ->
         let p' = f p in
         if Evd.eq_evar_info p'.goal p.goal then
 	  begin
 	    !solve_hook p';
 	    p'
 	  end
-        else 
+        else
 	  errorlabstrm "Refiner.frontier_map"
             (str"frontier_map was handed back a ill-formed proof.")
     | Some(r,pfl) ->
@@ -139,20 +139,20 @@ let frontier_map f n p =
   let nmax = p.open_subgoals in
   let n = if n < 0 then nmax + n + 1 else n in
   if n < 1 || n > nmax then
-    errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); 
+    errorlabstrm "Refiner.frontier_map" (str "No such subgoal");
   frontier_map_rec f n p
 
 let rec frontier_mapi_rec f i p =
   if p.open_subgoals = 0 then p else
   match p.ref with
-    | None -> 
+    | None ->
         let p' = f i p in
         if Evd.eq_evar_info p'.goal p.goal then
 	  begin
 	    !solve_hook p';
 	    p'
 	  end
-        else 
+        else
 	  errorlabstrm "Refiner.frontier_mapi"
             (str"frontier_mapi was handed back a ill-formed proof.")
     | Some(r,pfl) ->
@@ -161,7 +161,7 @@ let rec frontier_mapi_rec f i p =
             (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
             (i,[]) pfl in
         let pfl' = List.rev rpfl' in
-        { p with 
+        { p with
 	    open_subgoals = and_status (List.map pf_status pfl');
             ref = Some(r,pfl')}
 
@@ -176,7 +176,7 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
 
 (* leaf g is the canonical incomplete proof of a goal g *)
 
-let leaf g = 
+let leaf g =
   { open_subgoals = 1;
     goal = g;
     ref = None }
@@ -197,20 +197,20 @@ let abstract_operation syntax semantics gls =
       ref = Some(Nested(syntax,hidden_proof),spfl)})
 
 let abstract_tactic_expr ?(dflt=false) te tacfun gls =
-  abstract_operation (Tactic(te,dflt)) tacfun gls	
+  abstract_operation (Tactic(te,dflt)) tacfun gls
 
 let abstract_tactic ?(dflt=false) te =
   !abstract_tactic_box := Some te;
   abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
 
-let abstract_extended_tactic ?(dflt=false) s args = 
+let abstract_extended_tactic ?(dflt=false) s args =
   abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
 
 let refiner = function
   | Prim pr as r ->
       let prim_fun = prim_refiner pr in
 	(fun goal_sigma ->
-          let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in 
+          let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
 	    ({it=sgl; sigma = sigma'},
             (fun spfl ->
 	      assert (check_subproof_connection sgl spfl);
@@ -219,15 +219,15 @@ let refiner = function
 		ref = Some(r,spfl) })))
 
 
-  | Nested (_,_) | Decl_proof _ -> 
+  | Nested (_,_) | Decl_proof _ ->
       failwith "Refiner: should not occur"
-      
+
 	(* Daimon is a canonical unfinished proof *)
 
-  | Daimon -> 
-      fun gls -> 
-	({it=[];sigma=gls.sigma},  
-	 fun spfl -> 
+  | Daimon ->
+      fun gls ->
+	({it=[];sigma=gls.sigma},
+	 fun spfl ->
 	   assert (spfl=[]);
 	   { open_subgoals = 0;
              goal = gls.it;
@@ -250,10 +250,10 @@ let norm_evar_proof sigma pf =
    Their proof should be completed in order to complete the initial proof *)
 
 let extract_open_proof sigma pf =
-  let next_meta = 
+  let next_meta =
     let meta_cnt = ref 0 in
     let rec f () =
-      incr meta_cnt; 
+      incr meta_cnt;
       if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
       else !meta_cnt
     in f
@@ -261,14 +261,14 @@ let extract_open_proof sigma pf =
   let open_obligations = ref [] in
   let rec proof_extractor vl = function
     | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
-	  
+
     | {ref=Some(Nested(_,hidden_proof),spfl)} ->
 	let sgl,v = frontier hidden_proof in
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
- 
+
     | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
-	  
+
     | {ref=(None|Some(Daimon,[]));goal=goal} ->
 	let visible_rels =
           map_succeed
@@ -287,13 +287,13 @@ let extract_open_proof sigma pf =
         let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
         let meta = next_meta () in
 	open_obligations := (meta,abs_concl):: !open_obligations;
-	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) 
-	  
+	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
+
     | _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
   in
   let pfterm = proof_extractor [] pf in
   (pfterm, List.rev !open_obligations)
-  
+
 (*********************)
 (*   Tacticals       *)
 (*********************)
@@ -301,7 +301,7 @@ let extract_open_proof sigma pf =
 (* unTAC : tactic -> goal sigma -> proof sigma *)
 
 let unTAC tac g =
-  let (gl_sigma,v) = tac g in 
+  let (gl_sigma,v) = tac g in
   { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
 
 let unpackage glsig = (ref (glsig.sigma)),glsig.it
@@ -309,8 +309,8 @@ let unpackage glsig = (ref (glsig.sigma)),glsig.it
 let repackage r v = {it=v;sigma = !r}
 
 let apply_sig_tac r tac g =
-  check_for_interrupt (); (* Breakpoint *) 
-  let glsigma,v = tac (repackage r g) in 
+  check_for_interrupt (); (* Breakpoint *)
+  let glsigma,v = tac (repackage r g) in
   r := glsigma.sigma;
   (glsigma.it,v)
 
@@ -328,7 +328,7 @@ let tclNORMEVAR = norm_evar_tac
 let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
 
 (* the message printing identity tactic *)
-let tclIDTAC_MESSAGE s gls = 
+let tclIDTAC_MESSAGE s gls =
   msg (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
@@ -356,7 +356,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
   if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll,pl =
     List.split
-      (list_map_i (fun i -> 
+      (list_map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
   (sigr, List.flatten gll,
@@ -390,7 +390,7 @@ let theni_tac i tac ((_,gl,_) as subgoals) =
     thensf_tac
       (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC
       subgoals
-  else non_existent_goal k 
+  else non_existent_goal k
 
 (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
@@ -448,17 +448,17 @@ let rec tclTHENLIST = function
   | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
 
 (* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
-let tclMAP tacfun l = 
+let tclMAP tacfun l =
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
 (* various progress criterions *)
-let same_goal gl subgoal = 
+let same_goal gl subgoal =
   eq_constr (conclusion subgoal) (conclusion gl) &&
   eq_named_context_val (hypotheses subgoal) (hypotheses gl)
 
 
 let weak_progress gls ptree =
-  (List.length gls.it <> 1) || 
+  (List.length gls.it <> 1) ||
   (not (same_goal (List.hd gls.it) ptree.it))
 
 let progress gls ptree =
@@ -473,7 +473,7 @@ let tclPROGRESS tac ptree =
   if progress (fst rslt) ptree then rslt
   else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
 
-(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails 
+(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails
    if tac leaves the goal unchanged, possibly modifying sigma *)
 let tclWEAK_PROGRESS tac ptree =
   let rslt = tac ptree in
@@ -487,14 +487,14 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
   let rslt = tac goal in
   let gls = (fst rslt).it in
   if List.exists (same_goal goal.it) gls
-  then errorlabstrm "Refiner.tclNOTSAMEGOAL" 
+  then errorlabstrm "Refiner.tclNOTSAMEGOAL"
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
 let catch_failerror e =
   if catchable_exception e then check_for_interrupt ()
   else match e with
-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) 
+  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
   | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
       check_for_interrupt ()
   | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
@@ -507,18 +507,18 @@ let catch_failerror e =
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
 let tclORELSE0 t1 t2 g =
-  try 
+  try
     t1 g
   with (* Breakpoint *)
     | e -> catch_failerror e; t2 g
 
-(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
+(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
 let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 
 (* applies t1;t2then if t1 succeeds or t2else if t1 fails
    t2* are called in terminal position (unless t1 produces more than
-   1 subgoal!) *) 
+   1 subgoal!) *)
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
@@ -526,7 +526,7 @@ let tclORELSE_THEN t1 t2then t2else gls =
   with
     | None -> t2else gls
     | Some (sgl,v) ->
-        let (sigr,gl) = unpackage sgl in 
+        let (sigr,gl) = unpackage sgl in
         finish_tac (then_tac t2then  (sigr,gl,v))
 
 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
@@ -546,16 +546,16 @@ let ite_gen tcal tac_if continue tac_else gl=
     let result=tac_if gl in
       success:=true;result in
   let tac_else0 e gl=
-    if !success then 
-      raise e 
-    else 
+    if !success then
+      raise e
+    else
       tac_else gl in
-    try 
+    try
       tcal tac_if0 continue gl
     with (* Breakpoint *)
       | e -> catch_failerror e; tac_else0 e gl
 
-(* Try the first tactic and, if it succeeds, continue with 
+(* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)
 
 let tclIFTHENELSE=ite_gen tclTHEN
@@ -566,7 +566,7 @@ let tclIFTHENSELSE=ite_gen tclTHENS
 
 let tclIFTHENSVELSE=ite_gen tclTHENSV
 
-let tclIFTHENTRYELSEMUST tac1 tac2 gl = 
+let tclIFTHENTRYELSEMUST tac1 tac2 gl =
   tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
 
 (* Fails if a tactic did not solve the goal *)
@@ -575,17 +575,17 @@ let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
 (* Try the first thats solves the current goal *)
 let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
-			   
+
 (* Iteration tacticals *)
 
-let tclDO n t = 
-  let rec dorec k = 
+let tclDO n t =
+  let rec dorec k =
     if k < 0 then errorlabstrm "Refiner.tclDO"
       (str"Wrong argument : Do needs a positive integer.");
     if k = 0 then tclIDTAC
     else if k = 1 then t else (tclTHEN t (dorec (k-1)))
-  in 
-  dorec n 
+  in
+  dorec n
 
 
 (* Beware: call by need of CAML, g is needed *)
@@ -612,52 +612,52 @@ let tclIDTAC_list gls = (gls, fun x -> x)
 
 (* first_goal : goal list sigma -> goal sigma *)
 
-let first_goal gls = 
-  let gl = gls.it and sig_0 = gls.sigma in 
-  if gl = [] then error "first_goal"; 
+let first_goal gls =
+  let gl = gls.it and sig_0 = gls.sigma in
+  if gl = [] then error "first_goal";
   { it = List.hd gl; sigma = sig_0 }
 
 (* goal_goal_list : goal sigma -> goal list sigma *)
 
-let goal_goal_list gls = 
+let goal_goal_list gls =
   let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
 
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
 
-let apply_tac_list tac glls = 
+let apply_tac_list tac glls =
   let (sigr,lg) = unpackage glls in
   match lg with
   | (g1::rest) ->
       let (gl,p) = apply_sig_tac sigr tac g1 in
-      let n = List.length gl in 
-      (repackage sigr (gl@rest), 
+      let n = List.length gl in
+      (repackage sigr (gl@rest),
        fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
   | _ -> error "apply_tac_list"
-	  
-let then_tactic_list tacl1 tacl2 glls = 
+
+let then_tactic_list tacl1 tacl2 glls =
   let (glls1,pl1) = tacl1 glls in
   let (glls2,pl2) = tacl2 glls1 in
   (glls2, compose pl1 pl2)
 
 (* Transform a tactic_list into a tactic *)
 
-let tactic_list_tactic tac gls = 
+let tactic_list_tactic tac gls =
     let (glres,vl) = tac (goal_goal_list gls) in
     (glres, compose idtac_valid vl)
 
 
 
-(* The type of proof-trees state and a few utilities 
+(* The type of proof-trees state and a few utilities
    A proof-tree state is built from a proof-tree, a set of global
    constraints, and a stack which allows to navigate inside the
    proof-tree remembering how to rebuild the global proof-tree
    possibly after modification of one of the focused children proof-tree.
-   The number in the stack corresponds to 
+   The number in the stack corresponds to
    either the selected subtree and the validation is a function from a
    proof-tree list consisting only of one proof-tree to the global
-   proof-tree 
+   proof-tree
    or -1 when the move is done behind a registered tactic in which
-   case the validation corresponds to a constant function giving back 
+   case the validation corresponds to a constant function giving back
    the original proof-tree. *)
 
 type pftreestate = {
@@ -666,11 +666,11 @@ type pftreestate = {
   tstack   : (int * validation) list }
 
 let proof_of_pftreestate pts = pts.tpf
-let is_top_pftreestate pts = pts.tstack = [] 
+let is_top_pftreestate pts = pts.tstack = []
 let cursor_of_pftreestate pts = List.map fst pts.tstack
 let evc_of_pftreestate pts = pts.tpfsigma
 
-let top_goal_of_pftreestate pts = 
+let top_goal_of_pftreestate pts =
   { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
 
 let nth_goal_of_pftreestate n pts =
@@ -678,7 +678,7 @@ let nth_goal_of_pftreestate n pts =
   try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
   with Invalid_argument _ | Failure _ -> non_existent_goal n
 
-let traverse n pts = match n with 
+let traverse n pts = match n with
   | 0 -> (* go to the parent *)
       (match  pts.tstack with
 	 | [] -> error "traverse: no ancestors"
@@ -691,13 +691,13 @@ let traverse n pts = match n with
   | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
       (match pts.tpf.ref with
 	 | Some (Nested (_,spf),_) ->
-	     let v = (fun pfl -> pts.tpf) in 
+	     let v = (fun pfl -> pts.tpf) in
 	     { tpf = spf;
                tstack = (-1,v)::pts.tstack;
                tpfsigma = pts.tpfsigma }
 	 | _ -> error "traverse: not a tactic-node")
   | n -> (* when n>0, go to the nth child *)
-      let (npf,v) = descend n pts.tpf in 
+      let (npf,v) = descend n pts.tpf in
       { tpf = npf;
         tpfsigma = pts.tpfsigma;
         tstack = (n,v):: pts.tstack }
@@ -723,9 +723,9 @@ let map_pftreestate f pts =
 (* solve the nth subgoal with tactic tac *)
 
 let solve_nth_pftreestate n tac =
-  map_pftreestate 
+  map_pftreestate
     (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
- 
+
 let solve_pftreestate = solve_nth_pftreestate 1
 
 (* This function implements a poor man's undo at the current goal.
@@ -771,78 +771,78 @@ let extract_pftreestate pts =
 (* Focus on the first leaf proof in a proof-tree state *)
 
 let rec first_unproven pts =
-  let pf = (proof_of_pftreestate pts) in 
+  let pf = (proof_of_pftreestate pts) in
   if is_complete_proof pf then
     errorlabstrm "first_unproven" (str"No unproven subgoals");
   if is_leaf_proof pf then
     pts
   else
     let childnum =
-      list_try_find_i 
-	(fun n pf -> 
+      list_try_find_i
+	(fun n pf ->
 	   if not(is_complete_proof pf) then n else failwith "caught")
 	1 (children_of_proof pf)
-    in 
+    in
     first_unproven (traverse childnum pts)
 
 (* Focus on the last leaf proof in a proof-tree state *)
 
 let rec last_unproven pts =
-  let pf = proof_of_pftreestate pts in 
+  let pf = proof_of_pftreestate pts in
   if is_complete_proof pf then
     errorlabstrm "last_unproven" (str"No unproven subgoals");
   if is_leaf_proof pf then
     pts
-  else 
+  else
     let children = (children_of_proof pf) in
     let nchilds = List.length children in
     let childnum =
-      list_try_find_i 
+      list_try_find_i
         (fun n pf ->
            if not(is_complete_proof pf) then n else failwith "caught")
         1 (List.rev children)
-    in 
+    in
     last_unproven (traverse (nchilds-childnum+1) pts)
-      
+
 let rec nth_unproven n pts =
-  let pf = proof_of_pftreestate pts in 
+  let pf = proof_of_pftreestate pts in
   if is_complete_proof pf then
     errorlabstrm "nth_unproven" (str"No unproven subgoals");
   if is_leaf_proof pf then
-    if n = 1 then 
-      pts 
+    if n = 1 then
+      pts
     else
       errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
-  else 
+  else
     let children = children_of_proof pf in
     let rec process i k = function
-      | [] -> 
+      | [] ->
 	  errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
-      | pf1::rest -> 
-	  let k1 = nb_unsolved_goals pf1 in 
-	  if k1 < k then 
+      | pf1::rest ->
+	  let k1 = nb_unsolved_goals pf1 in
+	  if k1 < k then
 	    process (i+1) (k-k1) rest
-	  else 
+	  else
 	    nth_unproven k (traverse i pts)
-    in 
+    in
     process 1 n children
 
 let rec node_prev_unproven loc pts =
-  let pf = proof_of_pftreestate pts in 
+  let pf = proof_of_pftreestate pts in
   match cursor_of_pftreestate pts with
     | [] -> last_unproven pts
     | n::l ->
 	if is_complete_proof pf or loc = 1 then
           node_prev_unproven n (traverse 0 pts)
-	else 
+	else
 	  let child = List.nth (children_of_proof pf) (loc - 2) in
 	  if is_complete_proof child then
 	    node_prev_unproven (loc - 1) pts
-	  else 
+	  else
 	    first_unproven (traverse (loc - 1) pts)
 
 let rec node_next_unproven loc pts =
-  let pf = proof_of_pftreestate pts in 
+  let pf = proof_of_pftreestate pts in
   match cursor_of_pftreestate pts with
     | [] -> first_unproven pts
     | n::l ->
@@ -851,35 +851,35 @@ let rec node_next_unproven loc pts =
              node_next_unproven n (traverse 0 pts)
 	else if is_complete_proof (List.nth (children_of_proof pf) loc) then
 	  node_next_unproven (loc + 1) pts
-	else 
+	else
 	  last_unproven(traverse (loc + 1) pts)
 
 let next_unproven pts =
-  let pf = proof_of_pftreestate pts in 
+  let pf = proof_of_pftreestate pts in
   if is_leaf_proof pf then
     match cursor_of_pftreestate pts with
       | [] -> error "next_unproven"
       | n::_ -> node_next_unproven n (traverse 0 pts)
-  else 
+  else
     node_next_unproven (List.length (children_of_proof pf)) pts
 
 let prev_unproven pts =
-  let pf = proof_of_pftreestate pts in 
+  let pf = proof_of_pftreestate pts in
   if is_leaf_proof pf then
     match cursor_of_pftreestate pts with
       | [] -> error "prev_unproven"
       | n::_ -> node_prev_unproven n (traverse 0 pts)
-  else 
+  else
     node_prev_unproven 1 pts
 
-let rec top_of_tree pts = 
+let rec top_of_tree pts =
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
 (* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
 let change_rule f pts =
   let mark_top _ pt =
     match pt.ref with
-	Some (oldrule,l) -> 
+	Some (oldrule,l) ->
 	  {pt with ref=Some (f oldrule,l)}
       | _ -> invalid_arg "change_rule" in
     map_pftreestate mark_top pts
@@ -889,21 +889,21 @@ let match_rule p pts =
       Some (r,_) -> p r
     | None -> false
 
-let rec up_until_matching_rule p pts = 
-  if is_top_pftreestate pts then 
+let rec up_until_matching_rule p pts =
+  if is_top_pftreestate pts then
     raise Not_found
   else
     let one_up = traverse 0 pts in
-      if match_rule p one_up then 
+      if match_rule p one_up then
 	pts
       else
 	up_until_matching_rule p one_up
 
-let rec up_to_matching_rule p pts = 
-  if match_rule p pts then 
+let rec up_to_matching_rule p pts =
+  if match_rule p pts then
     pts
   else
-    if is_top_pftreestate pts then 
+    if is_top_pftreestate pts then
       raise Not_found
     else
       let one_up = traverse 0 pts in
@@ -917,14 +917,14 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 let pp_info = ref (fun _ _ _ -> assert false)
 let set_info_printer f = pp_info := f
 
-let tclINFO (tac : tactic) gls = 
-  let (sgl,v) as res = tac gls in 
-  begin try 
+let tclINFO (tac : tactic) gls =
+  let (sgl,v) as res = tac gls in
+  begin try
     let pf = v (List.map leaf (sig_it sgl)) in
     let sign = named_context_of_val (sig_it gls).evar_hyps in
     msgnl (hov 0 (str" == " ++
                   !pp_info (project gls) sign pf))
-  with e when catchable_exception e -> 
+  with e when catchable_exception e ->
     msgnl (hov 0 (str "Info failed to apply validation"))
   end;
   res
@@ -935,7 +935,7 @@ let set_proof_printer f = pp_proof := f
 let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } =
   (if stack = []
    then str "Rooted proof tree is:"
-   else (str "Proof tree at occurrence [" ++ 
+   else (str "Proof tree at occurrence [" ++
          prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n)
            (List.rev stack) ++ str "] is:")) ++ fnl() ++
   !pp_proof sigma (Global.named_context()) pf ++
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9a587a965..ff902d880 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -159,14 +159,14 @@ val tclNOTSAMEGOAL   : tactic -> tactic
 val tclINFO          : tactic -> tactic
 
 (* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
-   if it succeeds, applies [tac2] to the resulting subgoals, 
+   if it succeeds, applies [tac2] to the resulting subgoals,
    and if not applies [tac3] to the initial goal [gls] *)
 val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
 val tclIFTHENSELSE   : tactic -> tactic list -> tactic ->tactic
 val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
 
 (* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
-   has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. 
+   has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
    Equivalent to [(tac1;try tac2)||tac2] *)
 
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
@@ -199,7 +199,7 @@ val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
 val traverse : int -> pftreestate -> pftreestate
-val map_pftreestate : 
+val map_pftreestate :
   (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
 val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate : tactic -> pftreestate -> pftreestate
@@ -221,12 +221,12 @@ val next_unproven : pftreestate -> pftreestate
 val prev_unproven : pftreestate -> pftreestate
 val top_of_tree : pftreestate -> pftreestate
 val match_rule : (rule -> bool) -> pftreestate -> bool
-val up_until_matching_rule : (rule -> bool) -> 
+val up_until_matching_rule : (rule -> bool) ->
   pftreestate -> pftreestate
-val up_to_matching_rule : (rule -> bool) -> 
+val up_to_matching_rule : (rule -> bool) ->
   pftreestate -> pftreestate
 val change_rule : (rule -> rule) -> pftreestate -> pftreestate
-val change_constraints_pftreestate 
+val change_constraints_pftreestate
   : evar_map -> pftreestate -> pftreestate
 
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f53327249..ba3c27e63 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -51,12 +51,12 @@ let make_red_flag =
 	if red.rConst <> [] & not red.rDelta then
 	  error
 	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag 
+        add_flag
 	  { red with rConst = list_union red.rConst l; rDelta = true }
 	  lf
   in
   add_flag
-    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} 
+    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
 
 type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
 
@@ -85,7 +85,7 @@ type inversion_kind =
   | FullInversionClear
 
 type ('c,'id) inversion_strength =
-  | NonDepInversion of 
+  | NonDepInversion of
       inversion_kind * 'id list * intro_pattern_expr located option
   | DepInversion of
       inversion_kind * 'c option * intro_pattern_expr located option
@@ -115,12 +115,12 @@ let goal_location_of = function
 | _ ->
     error "Not a simple \"in\" clause (one hypothesis or the conclusion)"
 
-type ('constr,'id) induction_clause = 
-    ('constr with_bindings induction_arg list * 'constr with_bindings option * 
+type ('constr,'id) induction_clause =
+    ('constr with_bindings induction_arg list * 'constr with_bindings option *
      (intro_pattern_expr located option * intro_pattern_expr located option) *
      'id gclause option)
 
-type multi = 
+type multi =
   | Precisely of int
   | UpTo of int
   | RepeatStar
@@ -150,15 +150,15 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
-  | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * 
+  | TacApply of advanced_flag * evars_flag * 'constr with_bindings list *
       ('id * intro_pattern_expr located option) option
-  | TacElim of evars_flag * 'constr with_bindings * 
+  | TacElim of evars_flag * 'constr with_bindings *
       'constr with_bindings option
   | TacElimType of 'constr
   | TacCase of evars_flag * 'constr with_bindings
   | TacCaseType of 'constr
   | TacFix of identifier option * int
-  | TacMutualFix of hidden_flag * identifier * int * (identifier * int * 
+  | TacMutualFix of hidden_flag * identifier * int * (identifier * int *
       'constr) list
   | TacCofix of identifier option
   | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
@@ -211,10 +211,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr option
 
   (* Equality and inversion *)
-  | TacRewrite of 
+  | TacRewrite of
       evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
-      
+
   (* For ML extensions *)
   | TacExtend of loc * string * 'constr generic_argument list
 
@@ -225,11 +225,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
-  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * 
+  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
 	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array *
 	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
 	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array
-  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * 
+  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
 	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
@@ -263,7 +263,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | Integer        of int
   | TacCall        of loc *
       'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
-  | TacExternal of loc * string * string * 
+  | TacExternal of loc * string * string *
       ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
   | TacFreshId     of string or_var list
   | Tacexp of 'tac
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 40917b085..0faba52ea 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -55,10 +55,10 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
-let pf_get_hyp gls id = 
-  try 
+let pf_get_hyp gls id =
+  try
     Sign.lookup_named id (pf_hyps gls)
-  with Not_found -> 
+  with Not_found ->
     error ("No such hypothesis: " ^ (string_of_id id))
 
 let pf_get_hyp_typ gls id =
@@ -67,7 +67,7 @@ let pf_get_hyp_typ gls id =
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
-let pf_get_new_id id gls = 
+let pf_get_new_id id gls =
   next_ident_away id (pf_ids_of_hyps gls)
 
 let pf_get_new_ids ids gls =
@@ -77,19 +77,19 @@ let pf_get_new_ids ids gls =
     ids []
 
 let pf_interp_constr gls c =
-  let evc = project gls in 
+  let evc = project gls in
   Constrintern.interp_constr evc (pf_env gls) c
 
 let pf_interp_type gls c =
-  let evc = project gls in 
+  let evc = project gls in
   Constrintern.interp_type evc (pf_env gls) c
 
 let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
-let pf_reduction_of_red_expr gls re c = 
-  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c 
+let pf_reduction_of_red_expr gls re c =
+  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
@@ -113,7 +113,7 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
-let pf_check_type gls c1 c2 = 
+let pf_check_type gls c1 c2 =
   ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
 
 let pf_is_matching              = pf_apply Matching.is_matching_conv
@@ -179,16 +179,16 @@ let refiner = refiner
 let introduction_no_check id =
   refiner (Prim (Intro id))
 
-let internal_cut_no_check replace id t gl = 
+let internal_cut_no_check replace id t gl =
   refiner (Prim (Cut (true,replace,id,t))) gl
 
-let internal_cut_rev_no_check replace id t gl = 
+let internal_cut_rev_no_check replace id t gl =
   refiner (Prim (Cut (false,replace,id,t))) gl
 
-let refine_no_check c gl = 
+let refine_no_check c gl =
   refiner (Prim (Refine c)) gl
 
-let convert_concl_no_check c sty gl = 
+let convert_concl_no_check c sty gl =
   refiner (Prim (Convert_concl (c,sty))) gl
 
 let convert_hyp_no_check d gl =
@@ -202,16 +202,16 @@ let thin_no_check ids gl =
 let thin_body_no_check ids gl =
   if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
 
-let move_hyp_no_check with_dep id1 id2 gl = 
+let move_hyp_no_check with_dep id1 id2 gl =
   refiner (Prim (Move (with_dep,id1,id2))) gl
 
 let order_hyps idl gl =
   refiner (Prim (Order idl)) gl
 
-let rec rename_hyp_no_check l gl = match l with 
-  | [] -> tclIDTAC gl 
-  | (id1,id2)::l -> 
-      tclTHEN (refiner (Prim (Rename (id1,id2)))) 
+let rec rename_hyp_no_check l gl = match l with
+  | [] -> tclIDTAC gl
+  | (id1,id2)::l ->
+      tclTHEN (refiner (Prim (Rename (id1,id2))))
 	(rename_hyp_no_check l) gl
 
 let mutual_fix f n others j gl =
@@ -219,10 +219,10 @@ let mutual_fix f n others j gl =
 
 let mutual_cofix f others j gl =
   with_check (refiner (Prim (Cofix (f,others,j)))) gl
-    
+
 (* Versions with consistency checks *)
 
-let introduction id    = with_check (introduction_no_check id) 
+let introduction id    = with_check (introduction_no_check id)
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
@@ -230,7 +230,7 @@ let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
 let thin c             = with_check (thin_no_check c)
 let thin_body c        = with_check (thin_body_no_check c)
-let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
+let move_hyp b id id'  = with_check (move_hyp_no_check b id id')
 let rename_hyp l       = with_check (rename_hyp_no_check l)
 
 (* Pretty-printers *)
@@ -249,4 +249,4 @@ let pr_gls gls =
 let pr_glls glls =
   hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
-  
+
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 581933c83..a808ca419 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -67,12 +67,12 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
-val pf_reduce : 
+val pf_reduce :
   (env -> evar_map -> constr -> constr) ->
     goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
-val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list 
+val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 6674d04ea..ea8ab5b62 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -68,11 +68,11 @@ let skip = ref 0
 
 (* Prints the run counter *)
 let run ini =
-  if not ini then 
+  if not ini then
     for i=1 to 2 do
       print_char (Char.chr 8);print_char (Char.chr 13)
     done;
-  msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ 
+  msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
        fnl() ++ fnl())
 
 (* Prints the prompt *)
@@ -168,7 +168,7 @@ let db_matching_failure debug =
 let db_eval_failure debug s =
   if debug <> DebugOff & !skip = 0 then
     let s = str "message \"" ++ s ++ str "\"" in
-    msgnl 
+    msgnl
       (str "This rule has failed due to \"Fail\" tactic (" ++
        s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")