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

1 files changed, 411 insertions, 411 deletions

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 515b184da..c2a32471e 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -36,27 +36,27 @@ open Goptions
 
 let get_its_info gls = get_info gls.it
 
-let get_strictness,set_strictness = 
+let get_strictness,set_strictness =
   let strictness = ref false in
     (fun () -> (!strictness)),(fun b -> strictness:=b)
 
 let _ =
-  declare_bool_option 
+  declare_bool_option
     { optsync  = true;
       optname  = "strict mode";
       optkey   = ["Strict";"Proofs"];
       optread  = get_strictness;
       optwrite = set_strictness }
 
-let tcl_change_info_gen info_gen = 
+let tcl_change_info_gen info_gen =
   (fun gls ->
-  let gl =sig_it gls in  
-    {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, 
-  function 
+  let gl =sig_it gls in
+    {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls},
+  function
       [pftree] ->
 	{pftree with
 	   goal=gl;
-	   ref=Some (Prim Change_evars,[pftree])} 
+	   ref=Some (Prim Change_evars,[pftree])}
     | _ -> anomaly "change_info : Wrong number of subtrees")
 
 let tcl_change_info info gls =  tcl_change_info_gen (Some (pm_in info)) gls
@@ -78,27 +78,27 @@ let is_good_inductive env ind =
 let check_not_per pts =
   if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then
     match get_stack pts with
-	Per (_,_,_,_)::_ -> 
+	Per (_,_,_,_)::_ ->
 	  error "You are inside a proof per cases/induction.\n\
 Please \"suppose\" something or \"end\" it now."
       | _ -> ()
 
 let mk_evd metalist gls =
   let evd0= create_goal_evar_defs (sig_sig gls) in
-  let add_one (meta,typ) evd = 
+  let add_one (meta,typ) evd =
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
 
-let is_tmp id = (string_of_id id).[0] = '_'    
+let is_tmp id = (string_of_id id).[0] = '_'
 
-let tmp_ids gls = 
+let tmp_ids gls =
   let ctx = pf_hyps gls in
-    match ctx with 
+    match ctx with
 	[] -> []
-      | _::q -> List.filter is_tmp (ids_of_named_context q) 
+      | _::q -> List.filter is_tmp (ids_of_named_context q)
 
-let clean_tmp gls = 
-  let clean_id id0 gls0 = 
+let clean_tmp gls =
+  let clean_id id0 gls0 =
       tclTRY (clear [id0]) gls0 in
   let rec clean_all = function
       [] -> tclIDTAC
@@ -114,30 +114,30 @@ let assert_postpone id t =
 let start_proof_tac gls=
   let gl=sig_it gls in
   let info={pm_stack=[]} in
-    {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, 
-  function 
+    {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls},
+  function
       [pftree] ->
 	{pftree with
 	   goal=gl;
-	   ref=Some (Decl_proof true,[pftree])} 
+	   ref=Some (Decl_proof true,[pftree])}
     | _ -> anomaly "Dem : Wrong number of subtrees"
 
-let go_to_proof_mode () = 
-  Pfedit.mutate 
+let go_to_proof_mode () =
+  Pfedit.mutate
     (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts))
 
 (* closing gaps *)
 
 let daimon_tac gls =
   set_daimon_flag ();
-  ({it=[];sigma=sig_sig gls}, 
-   function 
+  ({it=[];sigma=sig_sig gls},
+   function
        [] ->
 	 {open_subgoals=0;
 	    goal=sig_it gls;
-	    ref=Some (Daimon,[])} 
+	    ref=Some (Daimon,[])}
      | _ -> anomaly "Daimon: Wrong number of subtrees")
-    
+
 let daimon _ pftree =
   set_daimon_flag ();
   {pftree with
@@ -150,7 +150,7 @@ let daimon_subtree = map_pftreestate (fun _ ->  frontier_mapi daimon )
 
 let rec is_focussing_instr = function
     Pthus i | Pthen i | Phence i -> is_focussing_instr i
-  | Pescape | Pper _ | Pclaim _ | Pfocus _ 
+  | Pescape | Pper _ | Pclaim _ | Pfocus _
   | Psuppose _ | Pcase (_,_,_)  -> true
   | _ -> false
 
@@ -158,7 +158,7 @@ let mark_rule_as_done = function
     Decl_proof true -> Decl_proof false
   | Decl_proof false ->
       anomaly "already marked as done"
-  | Nested(Proof_instr (lock_focus,instr),spfl) -> 
+  | Nested(Proof_instr (lock_focus,instr),spfl) ->
       if lock_focus then
 	Nested(Proof_instr (false,instr),spfl)
       else
@@ -168,34 +168,34 @@ let mark_rule_as_done = function
 let mark_proof_tree_as_done pt =
   match pt.ref with
       None -> anomaly "mark_proof_tree_as_done"
-    | Some (r,spfl) -> 
+    | Some (r,spfl) ->
 	{pt with ref= Some (mark_rule_as_done r,spfl)}
 
-let mark_as_done pts = 
-  map_pftreestate 
-    (fun _ -> mark_proof_tree_as_done) 
+let mark_as_done pts =
+  map_pftreestate
+    (fun _ -> mark_proof_tree_as_done)
     (up_to_matching_rule is_focussing_command pts)
 
 (* post-instruction focus management *)
 
 let goto_current_focus pts = up_until_matching_rule is_focussing_command pts
 
-let goto_current_focus_or_top pts = 
-  try 
+let goto_current_focus_or_top pts =
+  try
     up_until_matching_rule is_focussing_command pts
   with Not_found -> top_of_tree pts
 
 (* return *)
 
 let close_tactic_mode pts =
-    let pts1=  
-      try goto_current_focus pts 
-      with Not_found -> 
+    let pts1=
+      try goto_current_focus pts
+      with Not_found ->
 	error "\"return\" cannot be used outside of Declarative Proof Mode." in
     let pts2 = daimon_subtree pts1 in
-    let pts3 = mark_as_done pts2 in 
-      goto_current_focus pts3 
-	  
+    let pts3 = mark_as_done pts2 in
+      goto_current_focus pts3
+
 let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode
 
 (* end proof/claim *)
@@ -207,11 +207,11 @@ let close_block bt pts =
     else
       get_stack pts in
     match bt,stack with
-	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> 
+	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
 	  daimon_subtree (goto_current_focus pts)
-      | _, Claim::_ -> 
+      | _, Claim::_ ->
 	  error "\"end claim\" expected."
-      | _, Focus_claim::_ -> 
+      | _, Focus_claim::_ ->
 	  error "\"end focus\" expected."
       | _, [] ->
  	  error "\"end proof\" expected."
@@ -225,18 +225,18 @@ let close_block bt pts =
 
 (* utility for suppose / suppose it is *)
 
-let close_previous_case pts = 
-  if 
-    Proof_trees.is_complete_proof (proof_of_pftreestate pts) 
+let close_previous_case pts =
+  if
+    Proof_trees.is_complete_proof (proof_of_pftreestate pts)
   then
     match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..."  
-      | Suppose_case :: Per (et,_,_,_) :: _ -> 
+	Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..."
+      | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus (mark_as_done pts)
-      | _ -> error "Not inside a proof per cases or induction."   
+      | _ -> error "Not inside a proof per cases or induction."
   else
     match get_stack pts with
-	Per (et,_,_,_) :: _ -> pts 
+	Per (et,_,_,_) :: _ -> pts
       | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus (mark_as_done (daimon_subtree pts))
       | _ -> error "Not inside a proof per cases or induction."
@@ -246,10 +246,10 @@ let close_previous_case pts =
 (* automation *)
 
 let filter_hyps f gls =
-  let filter_aux (id,_,_) = 
-    if f id then 
+  let filter_aux (id,_,_) =
+    if f id then
       tclIDTAC
-    else 
+    else
       tclTRY (clear [id])  in
     tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls
 
@@ -257,16 +257,16 @@ let local_hyp_prefix = id_of_string "___"
 
 let add_justification_hyps keep items gls =
   let add_aux c gls=
-    match kind_of_term c with 
-	Var id -> 
+    match kind_of_term c with
+	Var id ->
 	  keep:=Idset.add id !keep;
-	  tclIDTAC gls 
-      | _ -> 
-	  let id=pf_get_new_id local_hyp_prefix gls in 
-	    keep:=Idset.add id !keep; 
+	  tclIDTAC gls
+      | _ ->
+	  let id=pf_get_new_id local_hyp_prefix gls in
+	    keep:=Idset.add id !keep;
 	    tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere)
-              (thin_body [id]) gls in 
-    tclMAP add_aux items gls   
+              (thin_body [id]) gls in
+    tclMAP add_aux items gls
 
 let prepare_goal items gls =
   let tokeep = ref Idset.empty in
@@ -275,18 +275,18 @@ let prepare_goal items gls =
      [ (fun _ -> auxres);
        filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls
 
-let my_automation_tac = ref 
+let my_automation_tac = ref
   (fun gls -> anomaly "No automation registered")
 
 let register_automation_tac tac = my_automation_tac:= tac
 
 let automation_tac gls = !my_automation_tac gls
 
-let justification tac gls= 
-    tclORELSE 
-      (tclSOLVE [tclTHEN tac assumption]) 
-      (fun gls -> 
-	 if get_strictness () then 
+let justification tac gls=
+    tclORELSE
+      (tclSOLVE [tclTHEN tac assumption])
+      (fun gls ->
+	 if get_strictness () then
 	   error "Insufficient justification."
 	 else
 	   begin
@@ -340,44 +340,44 @@ let enstack_subsubgoals env se stack gls=
 	    Inductive.lookup_mind_specif env ind in
           let gentypes=
             Inductive.arities_of_constructors ind (mib,oib) in
-	  let process i gentyp = 
-	    let constructor = mkConstruct(ind,succ i) 
+	  let process i gentyp =
+	    let constructor = mkConstruct(ind,succ i)
 	      (* constructors numbering*) in
 	    let appterm = applist (constructor,params) in
 	    let apptype = Term.prod_applist gentyp params in
 	    let rc,_ = Reduction.dest_prod env apptype in
-	    let rec meta_aux last lenv = function 
+	    let rec meta_aux last lenv = function
 		[] -> (last,lenv,[])
 	      | (nam,_,typ)::q ->
 		  let nlast=succ last in
 		  let (llast,holes,metas) =
 		    meta_aux nlast (mkMeta nlast :: lenv) q in
 		    (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
-	    let (nlast,holes,nmetas) = 
+	    let (nlast,holes,nmetas) =
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
-	    let evd = meta_assign se.se_meta 
+	    let evd = meta_assign se.se_meta
               (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in
-	    let ncreated = replace_in_list 
+	    let ncreated = replace_in_list
 	      se.se_meta nmetas se.se_meta_list in
-	    let evd0 = List.fold_left 
-	      (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in  
-	      List.iter (fun (m,typ) -> 
-			   Stack.push 
+	    let evd0 = List.fold_left
+	      (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in
+	      List.iter (fun (m,typ) ->
+			   Stack.push
 			     {se_meta=m;
 			      se_type=typ;
 			      se_evd=evd0;
 			      se_meta_list=ncreated;
-			      se_last_meta=nlast} stack) (List.rev nmetas) 
+			      se_last_meta=nlast} stack) (List.rev nmetas)
 	  in
 	    Array.iteri process gentypes
       | _ -> ()
 
-let rec nf_list evd = 
+let rec nf_list evd =
   function
-      [] -> []  
-    | (m,typ)::others -> 
-	if meta_defined evd m then 
+      [] -> []
+    | (m,typ)::others ->
+	if meta_defined evd m then
 	    nf_list evd others
 	else
 	  (m,nf_meta evd typ)::nf_list evd others
@@ -387,29 +387,29 @@ let find_subsubgoal c ctyp skip submetas gls =
   let concl = pf_concl gls in
   let evd = mk_evd ((0,concl)::submetas) gls in
   let stack = Stack.create () in
-  let max_meta = 
+  let max_meta =
       List.fold_left (fun a (m,_) -> max a m) 0 submetas in
-  let _ = Stack.push 
+  let _ = Stack.push
 		{se_meta=0;
 		 se_type=concl;
 		 se_last_meta=max_meta;
 		 se_meta_list=[0,concl];
 		 se_evd=evd} stack  in
-  let rec dfs n = 
+  let rec dfs n =
     let se = Stack.pop stack in
-      try 
-	let unifier = 
-	  Unification.w_unify true env Reduction.CUMUL 
+      try
+	let unifier =
+	  Unification.w_unify true env Reduction.CUMUL
 	    ctyp se.se_type se.se_evd in
-	  if n <= 0 then 
-	      {se with 
+	  if n <= 0 then
+	      {se with
 		 se_evd=meta_assign se.se_meta
                   (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier;
-	         se_meta_list=replace_in_list 
+	         se_meta_list=replace_in_list
 		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
-      with _ -> 
+      with _ ->
 	begin
 	  enstack_subsubgoals env se stack gls;
 	  dfs n
@@ -421,20 +421,20 @@ let concl_refiner metas body gls =
   let concl = pf_concl gls in
   let evd = sig_sig gls in
   let env = pf_env gls in
-  let sort = family_of_sort (Typing.sort_of env evd concl) in  
+  let sort = family_of_sort (Typing.sort_of env evd concl) in
   let rec aux env avoid subst = function
       [] -> anomaly "concl_refiner: cannot happen"
     | (n,typ)::rest ->
-	let _A = subst_meta subst typ in 
-	let x = id_of_name_using_hdchar env _A Anonymous in 
+	let _A = subst_meta subst typ in
+	let x = id_of_name_using_hdchar env _A Anonymous in
 	let _x = fresh_id avoid x gls in
 	let nenv = Environ.push_named (_x,None,_A) env in
 	let asort = family_of_sort (Typing.sort_of nenv evd _A) in
 	let nsubst = (n,mkVar _x)::subst in
-	  if rest = [] then 
+	  if rest = [] then
 	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
 	  else
-	    let bsort,_B,nbody = 
+	    let bsort,_B,nbody =
 	      aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in
 	    let body = mkNamedLambda _x _A nbody in
 	      if occur_term (mkVar _x) _B then
@@ -450,7 +450,7 @@ let concl_refiner metas body gls =
 			let _P0 = mkLambda(Anonymous,_AxB,concl) in
 			  InType,_AxB,
 			mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|])
-		    | _,_ -> 
+		    | _,_ ->
 			let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in
 			let _P0 = mkLambda(Anonymous,_AxB,concl) in
 			  InType,_AxB,
@@ -473,23 +473,23 @@ let concl_refiner metas body gls =
   let (_,_,prf) = aux env [] [] metas in
     mkApp(prf,[|mkMeta 1|])
 
-let thus_tac c ctyp submetas gls =  
-  let list,proof = 
+let thus_tac c ctyp submetas gls =
+  let list,proof =
     try
       find_subsubgoal c ctyp 0 submetas gls
-    with Not_found -> 
+    with Not_found ->
       error "I could not relate this statement to the thesis." in
   if list = [] then
-    exact_check proof gls 
+    exact_check proof gls
   else
     let refiner = concl_refiner list proof gls in
       Tactics.refine refiner gls
 
 (* general forward step *)
 
-let mk_stat_or_thesis info gls = function  
+let mk_stat_or_thesis info gls = function
     This c -> c
-  | Thesis (For _ ) -> 
+  | Thesis (For _ ) ->
       error "\"thesis for ...\" is not applicable here."
   | Thesis Plain -> pf_concl gls
 
@@ -497,34 +497,34 @@ let just_tac _then cut info gls0 =
   let items_tac gls =
     match cut.cut_by with
 	None -> tclIDTAC gls
-      | Some items -> 
-	  let items_ = 
-	    if _then then 
+      | Some items ->
+	  let items_ =
+	    if _then then
 	      let last_id = get_last (pf_env gls) in
 		(mkVar last_id)::items
-	    else items 
+	    else items
 	  in prepare_goal items_ gls in
-  let method_tac gls = 
+  let method_tac gls =
     match cut.cut_using with
-        None ->	
+        None ->
 	  automation_tac gls
-      | Some tac -> 
+      | Some tac ->
 	  (Tacinterp.eval_tactic tac) gls in
     justification (tclTHEN items_tac method_tac) gls0
-			
-let instr_cut mkstat _thus _then cut gls0 = 
-  let info = get_its_info gls0 in 
+
+let instr_cut mkstat _thus _then cut gls0 =
+  let info = get_its_info gls0 in
   let stat = cut.cut_stat in
-  let (c_id,_) = match stat.st_label with 
-      Anonymous -> 
-	pf_get_new_id (id_of_string "_fact") gls0,false 
+  let (c_id,_) = match stat.st_label with
+      Anonymous ->
+	pf_get_new_id (id_of_string "_fact") gls0,false
     | Name id -> id,true in
   let c_stat = mkstat info gls0 stat.st_it in
-  let thus_tac gls= 
-    if _thus then 
+  let thus_tac gls=
+    if _thus then
       thus_tac (mkVar c_id) c_stat [] gls
     else tclIDTAC gls in
-    tclTHENS (assert_postpone c_id c_stat) 
+    tclTHENS (assert_postpone c_id c_stat)
       [tclTHEN tcl_erase_info (just_tac _then cut info);
        thus_tac] gls0
 
@@ -538,162 +538,162 @@ let decompose_eq id gls =
   let whd =  (special_whd gls typ) in
     match kind_of_term whd with
 	App (f,args)->
-	  if eq_constr f _eq && (Array.length args)=3 
+	  if eq_constr f _eq && (Array.length args)=3
 	  then (args.(0),
-		args.(1), 
-		args.(2)) 
+		args.(1),
+		args.(2))
 	  else error "Previous step is not an equality."
       | _ -> error "Previous step is not an equality."
-	  
-let instr_rew _thus rew_side cut gls0 = 
-  let last_id = 
+
+let instr_rew _thus rew_side cut gls0 =
+  let last_id =
     try get_last (pf_env gls0) with _ -> error "No previous equality." in
-  let typ,lhs,rhs = decompose_eq last_id gls0 in  
+  let typ,lhs,rhs = decompose_eq last_id gls0 in
   let items_tac gls =
     match cut.cut_by with
 	None -> tclIDTAC gls
       | Some items -> prepare_goal items gls in
-  let method_tac gls = 
+  let method_tac gls =
     match cut.cut_using with
-        None ->	
+        None ->
 	  automation_tac gls
-      | Some tac -> 
+      | Some tac ->
 	  (Tacinterp.eval_tactic tac) gls in
   let just_tac gls =
     justification (tclTHEN items_tac method_tac) gls in
-  let (c_id,_) = match cut.cut_stat.st_label with 
-      Anonymous -> 
-	pf_get_new_id (id_of_string "_eq") gls0,false 
+  let (c_id,_) = match cut.cut_stat.st_label with
+      Anonymous ->
+	pf_get_new_id (id_of_string "_eq") gls0,false
     | Name id -> id,true in
-  let thus_tac new_eq gls= 
-    if _thus then 
+  let thus_tac new_eq gls=
+    if _thus then
       thus_tac (mkVar c_id) new_eq [] gls
     else tclIDTAC gls in
-    match rew_side with 
+    match rew_side with
 	Lhs ->
 	  let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
-	    tclTHENS (assert_postpone c_id new_eq) 
-	      [tclTHEN tcl_erase_info 
-		 (tclTHENS (transitivity lhs) 
+	    tclTHENS (assert_postpone c_id new_eq)
+	      [tclTHEN tcl_erase_info
+		 (tclTHENS (transitivity lhs)
 		    [just_tac;exact_check (mkVar last_id)]);
 	       thus_tac new_eq] gls0
       | Rhs ->
 	  let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
-	    tclTHENS (assert_postpone c_id new_eq) 
-	      [tclTHEN tcl_erase_info 
-		 (tclTHENS (transitivity rhs) 
+	    tclTHENS (assert_postpone c_id new_eq)
+	      [tclTHEN tcl_erase_info
+		 (tclTHENS (transitivity rhs)
 		    [exact_check (mkVar last_id);just_tac]);
 	       thus_tac new_eq] gls0
-	      
+
 
 
 (* tactics for claim/focus *)
 
-let instr_claim _thus st gls0 = 
-  let info = get_its_info gls0 in  
-  let (id,_) = match st.st_label with 
-      Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false 
+let instr_claim _thus st gls0 =
+  let info = get_its_info gls0 in
+  let (id,_) = match st.st_label with
+      Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false
     | Name id -> id,true in
-  let thus_tac gls= 
-    if _thus then 
+  let thus_tac gls=
+    if _thus then
       thus_tac (mkVar id) st.st_it [] gls
     else tclIDTAC gls in
   let ninfo1 = {pm_stack=
       (if _thus then Focus_claim else Claim)::info.pm_stack} in
-    tclTHENS (assert_postpone id st.st_it) 
+    tclTHENS (assert_postpone id st.st_it)
       [tcl_change_info ninfo1;
        thus_tac] gls0
 
 (* tactics for assume *)
 
-let push_intro_tac coerce nam gls = 
+let push_intro_tac coerce nam gls =
       let (hid,_) =
-	match nam with 
-	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false 
+	match nam with
+	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false
 	  | Name id -> id,true in
-	tclTHENLIST 
+	tclTHENLIST
 	  [intro_mustbe_force hid;
 	   coerce hid]
-	  gls 
-
-let assume_tac hyps gls = 
-  List.fold_right 
-    (fun (Hvar st | Hprop st) -> 
-       tclTHEN 
-	 (push_intro_tac 
-	    (fun id -> 
+	  gls
+
+let assume_tac hyps gls =
+  List.fold_right
+    (fun (Hvar st | Hprop st) ->
+       tclTHEN
+	 (push_intro_tac
+	    (fun id ->
 	       convert_hyp (id,None,st.st_it)) st.st_label))
-	 hyps tclIDTAC gls 
-
-let assume_hyps_or_theses hyps gls = 
-  List.fold_right 
-    (function 
-	 (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> 
-	   tclTHEN 
-	     (push_intro_tac 
-		(fun id -> 
+	 hyps tclIDTAC gls
+
+let assume_hyps_or_theses hyps gls =
+  List.fold_right
+    (function
+	 (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) ->
+	   tclTHEN
+	     (push_intro_tac
+		(fun id ->
 		   convert_hyp (id,None,c)) nam)
-       | Hprop {st_label=nam;st_it=Thesis (tk)} -> 
-	   tclTHEN 
-	     (push_intro_tac 
+       | Hprop {st_label=nam;st_it=Thesis (tk)} ->
+	   tclTHEN
+	     (push_intro_tac
 		(fun id -> tclIDTAC) nam))
-    hyps tclIDTAC gls 
+    hyps tclIDTAC gls
 
-let assume_st hyps gls = 
-  List.fold_right 
-    (fun st -> 
-       tclTHEN 
-	 (push_intro_tac 
+let assume_st hyps gls =
+  List.fold_right
+    (fun st ->
+       tclTHEN
+	 (push_intro_tac
 	    (fun id -> convert_hyp (id,None,st.st_it)) st.st_label))
-	 hyps tclIDTAC gls 
-
-let assume_st_letin hyps gls = 
-  List.fold_right 
-    (fun st -> 
-       tclTHEN 
-	 (push_intro_tac 
-	    (fun id -> 
+	 hyps tclIDTAC gls
+
+let assume_st_letin hyps gls =
+  List.fold_right
+    (fun st ->
+       tclTHEN
+	 (push_intro_tac
+	    (fun id ->
 	       convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
-	 hyps tclIDTAC gls 
+	 hyps tclIDTAC gls
 
 (* suffices *)
 
-let rec metas_from n hyps = 
+let rec metas_from n hyps =
   match hyps with
       _ :: q -> n :: metas_from (succ n) q
     | [] -> []
- 
+
 let rec build_product args body =
-  match args with 
-      (Hprop st| Hvar st )::rest -> 
+  match args with
+      (Hprop st| Hvar st )::rest ->
 	let pprod= lift 1 (build_product rest body) in
 	let lbody =
 	  match st.st_label with
 	      Anonymous -> pprod
 	    | Name id -> subst_term (mkVar id) pprod in
 	  mkProd (st.st_label, st.st_it, lbody)
-    | [] -> body 
+    | [] -> body
 
 let rec build_applist prod = function
     [] -> [],prod
-  | n::q -> 
+  | n::q ->
       let (_,typ,_) = destProd prod in
       let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
 	(n,typ)::ctx,head
 
-let instr_suffices _then cut gls0 = 
-  let info = get_its_info gls0 in 
-  let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in 
+let instr_suffices _then cut gls0 =
+  let info = get_its_info gls0 in
+  let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in
   let ctx,hd = cut.cut_stat in
   let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in
   let metas = metas_from 1 ctx in
   let c_ctx,c_head = build_applist c_stat metas in
-  let c_term = applist (mkVar c_id,List.map mkMeta metas) in  
-  let thus_tac gls= 
+  let c_term = applist (mkVar c_id,List.map mkMeta metas) in
+  let thus_tac gls=
     thus_tac c_term c_head c_ctx gls in
-   tclTHENS (assert_postpone c_id c_stat) 
-     [tclTHENLIST 
-	 [ assume_tac ctx;   
+   tclTHENS (assert_postpone c_id c_stat)
+     [tclTHENLIST
+	 [ assume_tac ctx;
 	   tcl_erase_info;
 	   just_tac _then cut info];
       thus_tac] gls0
@@ -703,7 +703,7 @@ let instr_suffices _then cut gls0 =
 let conjunction_arity id gls =
   let typ = pf_get_hyp_typ gls id  in
   let hd,params = decompose_app (special_whd gls typ) in
-  let env =pf_env gls in 
+  let env =pf_env gls in
     match kind_of_term hd with
 	Ind ind when is_good_inductive env ind ->
 	  let mib,oib=
@@ -716,70 +716,70 @@ let conjunction_arity id gls =
 	    List.length rc
       | _ -> raise Not_found
 
-let rec intron_then n ids ltac gls = 
-  if n<=0 then 
+let rec intron_then n ids ltac gls =
+  if n<=0 then
     ltac ids gls
-  else  
-    let id = pf_get_new_id (id_of_string "_tmp") gls in 
-      tclTHEN 
-	(intro_mustbe_force id) 
-	(intron_then (pred n) (id::ids) ltac) gls 
+  else
+    let id = pf_get_new_id (id_of_string "_tmp") gls in
+      tclTHEN
+	(intro_mustbe_force id)
+	(intron_then (pred n) (id::ids) ltac) gls
 
 
 let rec consider_match may_intro introduced available expected gls =
-  match available,expected with 
+  match available,expected with
       [],[] ->
 	  tclIDTAC gls
     | _,[] -> error "Last statements do not match a complete hypothesis."
 	(* should tell which ones *)
-    | [],hyps -> 
+    | [],hyps ->
 	if may_intro then
 	  begin
  	    let id = pf_get_new_id (id_of_string "_tmp") gls in
-	      tclIFTHENELSE 
+	      tclIFTHENELSE
 		(intro_mustbe_force id)
-		(consider_match true [] [id] hyps) 
-		(fun _ -> 
+		(consider_match true [] [id] hyps)
+		(fun _ ->
 		   error "Not enough sub-hypotheses to match statements.")
-		gls 
-          end 
+		gls
+          end
 	else
 	  error "Not enough sub-hypotheses to match statements."
 	    (* should tell which ones *)
     | id::rest_ids,(Hvar st | Hprop st)::rest ->
 	tclIFTHENELSE (convert_hyp (id,None,st.st_it))
 	  begin
-	    match st.st_label with 
-		Anonymous -> 
+	    match st.st_label with
+		Anonymous ->
 		  consider_match may_intro ((id,false)::introduced) rest_ids rest
-	      | Name hid -> 
-		  tclTHENLIST 
+	      | Name hid ->
+		  tclTHENLIST
 		    [rename_hyp [id,hid];
 		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
 	  end
 	  begin
-	    (fun gls -> 
+	    (fun gls ->
 	       let nhyps =
-		 try conjunction_arity id gls with 
-		     Not_found -> error "Matching hypothesis not found." in 
-		 tclTHENLIST 
+		 try conjunction_arity id gls with
+		     Not_found -> error "Matching hypothesis not found." in
+		 tclTHENLIST
 		   [general_case_analysis false (mkVar id,NoBindings);
 		    intron_then nhyps []
-		      (fun l -> consider_match may_intro introduced 
+		      (fun l -> consider_match may_intro introduced
 			 (List.rev_append l rest_ids) expected)] gls)
 	  end
 	  gls
-	  
+
 let consider_tac c hyps gls =
   match kind_of_term (strip_outer_cast c) with
       Var id ->
-	consider_match false [] [id] hyps gls 
-    | _ -> 
+	consider_match false [] [id] hyps gls
+    | _ ->
 	let id = pf_get_new_id (id_of_string "_tmp") gls in
-	tclTHEN 
+	tclTHEN
 	  (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c)
- 	  (consider_match false [] [id] hyps) gls 
-	  
+ 	  (consider_match false [] [id] hyps) gls
+
 
 let given_tac hyps gls =
   consider_match true [] [] hyps gls
@@ -789,22 +789,22 @@ let given_tac hyps gls =
 let rec take_tac wits gls =
   match wits with
       [] -> tclIDTAC gls
-    | wit::rest ->  
-	let typ = pf_type_of gls wit in  
+    | wit::rest ->
+	let typ = pf_type_of gls wit in
 	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
 (* tactics for define *)
 
 let rec build_function args body =
-  match args with 
-      st::rest -> 
+  match args with
+      st::rest ->
 	let pfun= lift 1 (build_function rest body) in
 	let id = match st.st_label with
 	    Anonymous -> assert false
 	  | Name id -> id in
 	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
-    | [] -> body 
+    | [] -> body
 
 let define_tac id args body gls =
   let t = build_function args body in
@@ -812,37 +812,37 @@ let define_tac id args body gls =
 
 (* tactics for reconsider *)
 
-let cast_tac id_or_thesis typ gls = 
+let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
       This id ->
 	let (_,body,_) = pf_get_hyp gls id in
 	  convert_hyp (id,body,typ) gls
-    | Thesis (For _ ) -> 
+    | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
-    | Thesis Plain ->    
+    | Thesis Plain ->
           convert_concl typ DEFAULTcast gls
-      
+
 (* per cases *)
 
 let is_rec_pos (main_ind,wft) =
   match main_ind with
       None -> false
-    | Some index -> 
+    | Some index ->
 	match fst (Rtree.dest_node wft) with
 	    Mrec i when i = index -> true
 	  | _ -> false
 
 let rec constr_trees (main_ind,wft) ind =
     match Rtree.dest_node wft with
-      Norec,_ -> 
-	let itree = 
-	  (snd (Global.lookup_inductive ind)).mind_recargs in 
+      Norec,_ ->
+	let itree =
+	  (snd (Global.lookup_inductive ind)).mind_recargs in
 	  constr_trees (None,itree) ind
     | _,constrs -> main_ind,constrs
 
 let ind_args rp ind =
     let main_ind,constrs = constr_trees rp ind in
-    let args ctree =     
+    let args ctree =
       Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in
       Array.map args constrs
 
@@ -853,7 +853,7 @@ let init_tree ids ind rp nexti =
 
 let map_tree_rp rp id_fun mapi = function
     Split_patt (ids,ind,branches) ->
-  let indargs = ind_args rp ind in 
+  let indargs = ind_args rp ind in
   let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in
     Split_patt (id_fun ids,ind,Array.mapi do_i branches)
   | _ -> failwith "map_tree_rp: not a splitting node"
@@ -865,19 +865,19 @@ let map_tree id_fun mapi = function
   | _ -> failwith "map_tree: not a splitting node"
 
 
-let start_tree env ind rp = 
+let start_tree env ind rp =
   init_tree Idset.empty ind rp (fun _ _ -> None)
 
-let build_per_info etype casee gls = 
+let build_per_info etype casee gls =
   let concl=pf_concl gls in
   let env=pf_env gls in
   let ctyp=pf_type_of gls casee in
-  let is_dep = dependent casee concl in 
+  let is_dep = dependent casee concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
-  let ind = 
+  let ind =
     try
-      destInd hd 
-    with _ -> 
+      destInd hd
+    with _ ->
       error "Case analysis must be done on an inductive object." in
   let mind,oind = Global.lookup_inductive ind in
   let nparams,index =
@@ -885,10 +885,10 @@ let build_per_info etype casee gls =
 	ET_Induction -> mind.mind_nparams_rec,Some (snd ind)
       | _ -> mind.mind_nparams,None in
   let params,real_args = list_chop nparams args in
-  let abstract_obj c body = 
-    let typ=pf_type_of gls c in 
+  let abstract_obj c body =
+    let typ=pf_type_of gls c in
       lambda_create env (typ,subst_term c body) in
-  let pred= List.fold_right abstract_obj    
+  let pred= List.fold_right abstract_obj
     real_args (lambda_create env (ctyp,subst_term casee concl)) in
     is_dep,
   {per_casee=casee;
@@ -897,7 +897,7 @@ let build_per_info etype casee gls =
    per_pred=pred;
    per_args=real_args;
    per_params=params;
-   per_nparams=nparams;   
+   per_nparams=nparams;
    per_wf=index,oind.mind_recargs}
 
 let per_tac etype casee gls=
@@ -906,25 +906,25 @@ let per_tac etype casee gls=
     match casee with
 	Real c ->
 	  let is_dep,per_info = build_per_info etype c gls in
-	  let ek = 
+	  let ek =
 	    if is_dep then
 	      EK_dep (start_tree env per_info.per_ind per_info.per_wf)
 	    else EK_unknown in
-	    tcl_change_info 
+	    tcl_change_info
 	      {pm_stack=
 		  Per(etype,per_info,ek,[])::info.pm_stack} gls
       | Virtual cut ->
 	  assert (cut.cut_stat.st_label=Anonymous);
 	  let id = pf_get_new_id (id_of_string "anonymous_matched") gls in
 	  let c = mkVar id in
-	  let modified_cut = 
+	  let modified_cut =
 	    {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
-	    tclTHEN 
+	    tclTHEN
 	      (instr_cut (fun _ _ c -> c) false false modified_cut)
 	      (fun gls0 ->
 		 let is_dep,per_info = build_per_info etype c gls0 in
 		   assert (not is_dep);
-		   tcl_change_info 
+		   tcl_change_info
 		     {pm_stack=
 			 Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
 	      gls
@@ -941,7 +941,7 @@ let register_nodep_subcase id= function
       end
   | _ -> anomaly "wrong stack state"
 
-let suppose_tac hyps gls0 = 
+let suppose_tac hyps gls0 =
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
   let id = pf_get_new_id (id_of_string "subcase_") gls0 in
@@ -949,13 +949,13 @@ let suppose_tac hyps gls0 =
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let old_clauses,stack = register_nodep_subcase id info.pm_stack in
   let ninfo2 = {pm_stack=stack} in
-    tclTHENS (assert_postpone id clause) 
+    tclTHENS (assert_postpone id clause)
       [tclTHENLIST [tcl_change_info ninfo1;
 		    assume_tac hyps;
 		    clear old_clauses];
        tcl_change_info ninfo2] gls0
 
-(* suppose it is ... *) 
+(* suppose it is ... *)
 
 (* pattern matching compiling *)
 
@@ -966,20 +966,20 @@ let rec skip_args rest ids n =
     Skip_patt (ids,skip_args rest ids (pred n))
 
 let rec tree_of_pats ((id,_) as cpl) pats =
-  match pats with 
+  match pats with
       [] -> End_patt cpl
     | args::stack ->
 	match args with
 	    [] -> Close_patt (tree_of_pats cpl stack)
 	  | (patt,rp) :: rest_args ->
 	      match patt with
-		  PatVar (_,v) -> 
+		  PatVar (_,v) ->
 		    Skip_patt (Idset.singleton id,
 			       tree_of_pats cpl (rest_args::stack))
 		| PatCstr (_,(ind,cnum),args,nam) ->
 		    let nexti i ati =
-		      if i = pred cnum then 
-			let nargs = 
+		      if i = pred cnum then
+			let nargs =
 			  list_map_i (fun j a -> (a,ati.(j))) 0 args in
 			  Some (Idset.singleton id,
 				tree_of_pats cpl (nargs::rest_args::stack))
@@ -987,49 +987,49 @@ let rec tree_of_pats ((id,_) as cpl) pats =
 		      in init_tree Idset.empty ind rp nexti
 
 let rec add_branch ((id,_) as cpl) pats tree=
-  match pats with 
-      [] -> 
+  match pats with
+      [] ->
 	begin
 	  match tree with
-	      End_patt cpl0 -> End_patt cpl0 
-		(* this ensures precedence for overlapping patterns *) 
+	      End_patt cpl0 -> End_patt cpl0
+		(* this ensures precedence for overlapping patterns *)
 	    | _ -> anomaly "tree is expected to end here"
 	end
     | args::stack ->
-	match args with 
+	match args with
 	    [] ->
 	      begin
 		match tree with
-		   Close_patt t -> 
+		   Close_patt t ->
 		     Close_patt (add_branch cpl stack t)
-		  | _ -> anomaly "we should pop here" 
+		  | _ -> anomaly "we should pop here"
 	      end
 	  | (patt,rp) :: rest_args ->
 	      match patt with
 		  PatVar (_,v) ->
 		    begin
-		      match tree with 
-			  Skip_patt (ids,t) -> 
+		      match tree with
+			  Skip_patt (ids,t) ->
 			    Skip_patt (Idset.add id ids,
 				       add_branch cpl (rest_args::stack) t)
 			| Split_patt (_,_,_) ->
 			    map_tree (Idset.add id)
-			      (fun i bri ->  
-				 append_branch cpl 1 (rest_args::stack) bri) 
+			      (fun i bri ->
+				 append_branch cpl 1 (rest_args::stack) bri)
 			      tree
-			| _ -> anomaly "No pop/stop expected here"  
+			| _ -> anomaly "No pop/stop expected here"
 		    end
 		| PatCstr (_,(ind,cnum),args,nam) ->
 		      match tree with
 			Skip_patt (ids,t) ->
 			  let nexti i ati =
-			    if i = pred cnum then 
-			      let nargs = 
+			    if i = pred cnum then
+			      let nargs =
 				list_map_i (fun j a -> (a,ati.(j))) 0 args in
 				Some (Idset.add id ids,
 				      add_branch cpl (nargs::rest_args::stack)
 					(skip_args t ids (Array.length ati)))
-			    else 
+			    else
 			      Some (ids,
 				    skip_args t ids (Array.length ati))
 			  in init_tree ids ind rp nexti
@@ -1038,30 +1038,30 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			    (* this can happen with coercions *)
 	                    "Case pattern belongs to wrong inductive type.";
 			  let mapi i ati bri =
-			    if i = pred cnum then 
-			      let nargs = 
+			    if i = pred cnum then
+			      let nargs =
 				list_map_i (fun j a -> (a,ati.(j))) 0 args in
-				append_branch cpl 0 
+				append_branch cpl 0
 				  (nargs::rest_args::stack) bri
 			    else bri in
 			    map_tree_rp rp (fun ids -> ids) mapi tree
 		      | _ -> anomaly "No pop/stop expected here"
 and append_branch ((id,_) as cpl) depth pats = function
-    Some (ids,tree) -> 
+    Some (ids,tree) ->
       Some (Idset.add id ids,append_tree cpl depth pats tree)
   | None ->
       Some (Idset.singleton id,tree_of_pats cpl pats)
 and append_tree ((id,_) as cpl) depth pats tree =
   if depth<=0 then add_branch cpl pats tree
   else match tree with
-      Close_patt t -> 
+      Close_patt t ->
 	Close_patt (append_tree cpl (pred depth) pats t)
-    | Skip_patt (ids,t) -> 
+    | Skip_patt (ids,t) ->
 	Skip_patt (Idset.add id ids,append_tree cpl depth pats t)
     | End_patt _ -> anomaly "Premature end of branch"
-    | Split_patt (_,_,_) -> 
-	map_tree (Idset.add id) 
-	  (fun i bri -> append_branch cpl (succ depth) pats bri) tree 
+    | Split_patt (_,_,_) ->
+	map_tree (Idset.add id)
+	  (fun i bri -> append_branch cpl (succ depth) pats bri) tree
 
 (* suppose it is *)
 
@@ -1075,22 +1075,22 @@ let thesis_for obj typ per_info env=
   let cind,all_args=decompose_app typ in
   let ind = destInd cind in
   let _ = if ind <> per_info.per_ind then
-    errorlabstrm "thesis_for" 
-      ((Printer.pr_constr_env env obj) ++ spc () ++ 
-	 str"cannot give an induction hypothesis (wrong inductive type).") in  
+    errorlabstrm "thesis_for"
+      ((Printer.pr_constr_env env obj) ++ spc () ++
+	 str"cannot give an induction hypothesis (wrong inductive type).") in
   let params,args = list_chop per_info.per_nparams all_args in
   let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
-    errorlabstrm "thesis_for" 
-      ((Printer.pr_constr_env env obj) ++ spc () ++ 
+    errorlabstrm "thesis_for"
+      ((Printer.pr_constr_env env obj) ++ spc () ++
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
     compose_prod rc (whd_beta Evd.empty hd2)
 
 let rec build_product_dep pat_info per_info args body gls =
-  match args with 
-      (Hprop {st_label=nam;st_it=This c} 
-      | Hvar {st_label=nam;st_it=c})::rest -> 
-	let pprod= 
+  match args with
+      (Hprop {st_label=nam;st_it=This c}
+      | Hvar {st_label=nam;st_it=c})::rest ->
+	let pprod=
 	  lift 1 (build_product_dep pat_info per_info rest body gls) in
 	let lbody =
 	  match nam with
@@ -1098,7 +1098,7 @@ let rec build_product_dep pat_info per_info args body gls =
 	    | Name id -> subst_var id pprod in
 	  mkProd (nam,c,lbody)
     | Hprop ({st_it=Thesis tk} as st)::rest ->
-	let pprod= 
+	let pprod=
 	  lift 1 (build_product_dep pat_info per_info rest body gls) in
 	let lbody =
 	  match st.st_label with
@@ -1108,14 +1108,14 @@ let rec build_product_dep pat_info per_info args body gls =
 	  match tk with
 	      For id ->
 		let obj = mkVar id in
-		let typ = 
-		  try st_assoc (Name id) pat_info.pat_vars 
-		  with Not_found -> 
+		let typ =
+		  try st_assoc (Name id) pat_info.pat_vars
+		  with Not_found ->
 		    snd (st_assoc (Name id) pat_info.pat_aliases) in
 		  thesis_for obj typ per_info (pf_env gls)
 	    | Plain -> pf_concl gls in
 	  mkProd (st.st_label,ptyp,lbody)
-    | [] -> body 
+    | [] -> body
 
 let build_dep_clause params pat_info per_info hyps gls =
   let concl=
@@ -1129,35 +1129,35 @@ let build_dep_clause params pat_info per_info hyps gls =
   let let_one_in st body =
     match st.st_label with
 	Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body)
-      | Name id -> 
+      | Name id ->
 	  mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in
-  let aliased_clause = 
+  let aliased_clause =
     List.fold_right let_one_in pat_info.pat_aliases open_clause in
     List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause
 
 let rec register_dep_subcase id env per_info pat = function
     EK_nodep -> error  "Only \"suppose it is\" can be used here."
-  | EK_unknown -> 
+  | EK_unknown ->
       register_dep_subcase id env per_info pat
 	(EK_dep (start_tree env per_info.per_ind per_info.per_wf))
   | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
-  
+
 let case_tac params pat_info hyps gls0 =
   let info = get_its_info gls0 in
   let id = pf_get_new_id (id_of_string "subcase_") gls0 in
   let et,per_info,ek,old_clauses,rest =
     match info.pm_stack with
-	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) 
+	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest)
       | _ -> anomaly "wrong place for cases" in
   let clause = build_dep_clause params pat_info per_info hyps gls0 in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
-  let nek = 
-    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info 
-      pat_info.pat_pat ek in  
+  let nek =
+    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info
+      pat_info.pat_pat ek in
   let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
-    tclTHENS (assert_postpone id clause) 
-      [tclTHENLIST 
-	 [tcl_change_info ninfo1; 
+    tclTHENS (assert_postpone id clause)
+      [tclTHENLIST
+	 [tcl_change_info ninfo1;
 	  assume_st (params@pat_info.pat_vars);
 	  assume_st_letin pat_info.pat_aliases;
 	  assume_hyps_or_theses hyps;
@@ -1172,23 +1172,23 @@ type instance_stack =
 let initial_instance_stack ids =
   List.map (fun id -> id,[None,[]]) ids
 
-let push_one_arg arg = function 
+let push_one_arg arg = function
     [] -> anomaly "impossible"
-  | (head,args) :: ctx -> 
+  | (head,args) :: ctx ->
       ((head,(arg::args)) :: ctx)
 
 let push_arg arg stacks =
   List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks
-  
 
-let push_one_head c ids (id,stack) = 
+
+let push_one_head c ids (id,stack) =
   let head = if Idset.mem id ids then Some c else None in
     id,(head,[]) :: stack
 
 let push_head c ids stacks =
   List.map (push_one_head c ids) stacks
 
-let pop_one (id,stack) =  
+let pop_one (id,stack) =
   let nstack=
     match stack with
 	[] -> anomaly "impossible"
@@ -1209,30 +1209,30 @@ let hrec_for fix_id per_info gls obj_id =
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
   let ind = destInd cind in assert (ind=per_info.per_ind);
-  let params,args= list_chop per_info.per_nparams all_args in 
+  let params,args= list_chop per_info.per_nparams all_args in
   assert begin
-    try List.for_all2 eq_constr params per_info.per_params with 
+    try List.for_all2 eq_constr params per_info.per_params with
         Invalid_argument _ -> false end;
-  let hd2 = applist (mkVar fix_id,args@[obj]) in 
+  let hd2 = applist (mkVar fix_id,args@[obj]) in
     compose_lam rc (whd_beta gls.sigma hd2)
 
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
-      Close_patt t,_ ->  
-	let args0 = pop_stacks args in	
+      Close_patt t,_ ->
+	let args0 = pop_stacks args in
 	  execute_cases fix_name per_info tacnext args0 objs nhrec t gls
-    | Skip_patt (_,t),skipped::next_objs -> 
+    | Skip_patt (_,t),skipped::next_objs ->
 	let args0 = push_arg skipped args in
 	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
-    | End_patt (id,nhyps),[] -> 
+    | End_patt (id,nhyps),[] ->
 	begin
 	  match List.assoc id args with
-	      [None,br_args] -> 
-		let metas = 
+	      [None,br_args] ->
+		let metas =
 		  list_tabulate (fun n -> mkMeta (succ n)) nhyps in
 		  tclTHEN
 		    (tclDO nhrec introf)
-		    (tacnext 
+		    (tacnext
 		       (applist (mkVar id,List.rev_append br_args metas))) gls
 	    | _ -> anomaly "wrong stack size"
 	end
@@ -1245,111 +1245,111 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let _ = assert (destInd hd = ind) in (* just in case *)
 	let params,real_args = list_chop nparams all_args in
-	let abstract_obj c body = 
-	  let typ=pf_type_of gls c in 
+	let abstract_obj c body =
+	  let typ=pf_type_of gls c in
 	    lambda_create env (typ,subst_term c body) in
-	let elim_pred = List.fold_right abstract_obj    
+	let elim_pred = List.fold_right abstract_obj
 	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
 	let case_info = Inductiveops.make_case_info env ind RegularStyle in
 	let gen_arities = Inductive.arities_of_constructors ind spec in
-	let f_ids typ = 
-	  let sign = 
+	let f_ids typ =
+	  let sign =
 	    (prod_assum (Term.prod_applist typ params)) in
 	    find_intro_names sign gls in
 	let constr_args_ids = Array.map f_ids gen_arities in
-	let case_term =	 
+	let case_term =
 	  mkCase(case_info,elim_pred,casee,
 		 Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in
 	let branch_tac i (recargs,bro) gls0 =
 	  let args_ids = constr_args_ids.(i) in
 	  let rec aux n = function
-	      [] -> 
-		assert (n=Array.length recargs); 
+	      [] ->
+		assert (n=Array.length recargs);
 		next_objs,[],nhrec
-	    | id :: q -> 
+	    | id :: q ->
 		let objs,recs,nrec = aux (succ n) q in
-		  if recargs.(n) 
-		  then (mkVar id::objs),(id::recs),succ nrec 
+		  if recargs.(n)
+		  then (mkVar id::objs),(id::recs),succ nrec
 		  else (mkVar id::objs),recs,nrec in
 	  let objs,recs,nhrec = aux 0 args_ids in
 	    tclTHENLIST
 	      [tclMAP intro_mustbe_force args_ids;
 	       begin
-		 fun gls1 -> 
-		   let hrecs = 
-		     List.map 
-		       (fun id -> 
-			  hrec_for (out_name fix_name) per_info gls1 id) 
+		 fun gls1 ->
+		   let hrecs =
+		     List.map
+		       (fun id ->
+			  hrec_for (out_name fix_name) per_info gls1 id)
 		       recs in
 		     generalize hrecs gls1
 	       end;
 	       match bro with
-		   None -> 
+		   None ->
 		     msg_warning (str "missing case");
 		     tacnext (mkMeta 1)
 		 | Some (sub_ids,tree) ->
 		     let br_args =
-		       List.filter 
-			 (fun (id,_) -> Idset.mem id sub_ids) args in 
-		     let construct = 
+		       List.filter
+			 (fun (id,_) -> Idset.mem id sub_ids) args in
+		     let construct =
 		       applist (mkConstruct(ind,succ i),params) in
-		     let p_args = 
+		     let p_args =
 		       push_head construct ids br_args in
-		       execute_cases fix_name per_info tacnext 
+		       execute_cases fix_name per_info tacnext
 			 p_args objs nhrec tree] gls0 in
-	  tclTHENSV 
+	  tclTHENSV
 	    (refine case_term)
 	    (Array.mapi branch_tac br) gls
-    | Split_patt (_, _, _) , [] -> 
+    | Split_patt (_, _, _) , [] ->
 	anomaly "execute_cases : Nothing to split"
-    | Skip_patt _ , [] -> 
+    | Skip_patt _ , [] ->
 	anomaly "execute_cases : Nothing to skip"
-    | End_patt (_,_) , _ :: _  -> 
+    | End_patt (_,_) , _ :: _  ->
 	anomaly "execute_cases : End of branch with garbage left"
 
 
 
 (* end focus/claim *)
-		
+
 let end_tac et2 gls =
   let info = get_its_info gls in
-  let et1,pi,ek,clauses = 
+  let et1,pi,ek,clauses =
     match info.pm_stack with
-	Suppose_case::_ -> 
+	Suppose_case::_ ->
 	  anomaly "This case should already be trapped"
-      | Claim::_ ->  
+      | Claim::_ ->
 	  error "\"end claim\" expected."
       | Focus_claim::_ ->
 	  error "\"end focus\" expected."
-      | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) 
-      | [] -> 
+      | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses)
+      | [] ->
 	  anomaly "This case should already be trapped" in
-  let et = 
+  let et =
     if et1 <> et2 then
-      match et1 with 
-	  ET_Case_analysis -> 
+      match et1 with
+	  ET_Case_analysis ->
 	    error "\"end cases\" expected."
 	| ET_Induction ->
 	    error "\"end induction\" expected."
     else et1 in
-    tclTHEN 
+    tclTHEN
       tcl_erase_info
       begin
 	match et,ek with
-	    _,EK_unknown -> 
-	      tclSOLVE [simplest_elim pi.per_casee]	
+	    _,EK_unknown ->
+	      tclSOLVE [simplest_elim pi.per_casee]
 	  | ET_Case_analysis,EK_nodep ->
-	      tclTHEN 
+	      tclTHEN
 		(general_case_analysis false (pi.per_casee,NoBindings))
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
-		[generalize (pi.per_args@[pi.per_casee]); 
+		[generalize (pi.per_args@[pi.per_casee]);
 		 simple_induct (AnonHyp (succ (List.length pi.per_args)));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
-		 execute_cases Anonymous pi 
-		   (fun c -> tclTHENLIST 
+		 execute_cases Anonymous pi
+		   (fun c -> tclTHENLIST
 		      [refine c;
 		       clear clauses;
 		       justification assumption])
@@ -1358,25 +1358,25 @@ let end_tac et2 gls =
 	      let nargs = (List.length pi.per_args) in
 		tclTHEN (generalize (pi.per_args@[pi.per_casee]))
 		  begin
-		    fun gls0 -> 
-		      let fix_id = 
+		    fun gls0 ->
+		      let fix_id =
 			pf_get_new_id (id_of_string "_fix") gls0 in
-		      let c_id = 
+		      let c_id =
 			pf_get_new_id (id_of_string "_main_arg") gls0 in
 			tclTHENLIST
 			  [fix (Some fix_id) (succ nargs);
 			   tclDO nargs introf;
 			   intro_mustbe_force c_id;
-			   execute_cases (Name fix_id) pi 
+			   execute_cases (Name fix_id) pi
 			     (fun c ->
-				tclTHENLIST 
+				tclTHENLIST
 				  [clear [fix_id];
 				   refine c;
 				   clear clauses;
 				   justification assumption])
-			     (initial_instance_stack clauses) 
+			     (initial_instance_stack clauses)
 			     [mkVar c_id]  0 tree] gls0
-		  end	
+		  end
       end gls
 
 (* escape *)
@@ -1385,21 +1385,21 @@ let escape_tac gls =  tcl_erase_info gls
 
 (* General instruction engine *)
 
-let rec do_proof_instr_gen _thus _then instr = 
-  match instr with 
-      Pthus i -> 
+let rec do_proof_instr_gen _thus _then instr =
+  match instr with
+      Pthus i ->
 	assert (not _thus);
 	do_proof_instr_gen true _then i
-    | Pthen i -> 	
+    | Pthen i ->
 	assert (not _then);
 	do_proof_instr_gen _thus true i
-    | Phence i -> 
+    | Phence i ->
 	assert (not (_then || _thus));
 	do_proof_instr_gen true true i
     | Pcut c ->
 	instr_cut mk_stat_or_thesis _thus _then c
     | Psuffices c ->
-	instr_suffices _then c 
+	instr_suffices _then c
     | Prew (s,c) ->
 	assert (not _then);
 	instr_rew _thus s c
@@ -1407,75 +1407,75 @@ let rec do_proof_instr_gen _thus _then instr =
     | Pgiven hyps            -> given_tac hyps
     | Passume hyps           -> assume_tac hyps
     | Plet hyps              -> assume_tac hyps
-    | Pclaim st              -> instr_claim false st 
+    | Pclaim st              -> instr_claim false st
     | Pfocus st              -> instr_claim true st
     | Ptake witl             -> take_tac witl
     | Pdefine (id,args,body) -> define_tac id args body
-    | Pcast (id,typ)         -> cast_tac id typ 
-    | Pper (et,cs)           -> per_tac et cs 
+    | Pcast (id,typ)         -> cast_tac id typ
+    | Pper (et,cs)           -> per_tac et cs
     | Psuppose hyps      -> suppose_tac hyps
     | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
     | Pend (B_elim et) -> end_tac et
     | Pend _ -> anomaly "Not applicable"
     | Pescape -> escape_tac
- 
+
 let eval_instr {instr=instr} =
-  do_proof_instr_gen false false instr   
+  do_proof_instr_gen false false instr
 
 let rec preprocess pts instr =
   match instr with
     Phence i |Pthus i | Pthen i -> preprocess pts i
-  | Psuffices _ | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
-  | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ 
+  | Psuffices _ | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _
+  | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _
   | Pdefine (_,_,_) | Pper _ | Prew _ ->
       check_not_per pts;
       true,pts
-  | Pescape -> 
+  | Pescape ->
       check_not_per pts;
       true,pts
-  | Pcase _ | Psuppose _ | Pend (B_elim _) -> 
+  | Pcase _ | Psuppose _ | Pend (B_elim _) ->
       true,close_previous_case pts
-  | Pend bt -> 
-      false,close_block bt pts 
-      
-let rec postprocess pts instr = 
+  | Pend bt ->
+      false,close_block bt pts
+
+let rec postprocess pts instr =
   match instr with
       Phence i | Pthus i | Pthen i -> postprocess pts i
     | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
-    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ 
+    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _
     | Pescape -> nth_unproven 1 pts
     | Pend (B_elim ET_Induction) ->
   	begin
 	  let pf = proof_of_pftreestate pts in
 	  let (pfterm,_) = extract_open_pftreestate pts in
 	  let env =  Evd.evar_env (goal_of_proof pf) in
-	    try 
+	    try
 	      Inductiveops.control_only_guard env pfterm;
 	      goto_current_focus_or_top (mark_as_done pts)
- 	    with 
+ 	    with
 		Type_errors.TypeError(env,
 				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
 		  anomaly "\"end induction\" generated an ill-formed fixpoint"
 	end
-    | Pend _ -> 
+    | Pend _ ->
 	goto_current_focus_or_top (mark_as_done pts)
 
 let do_instr raw_instr pts =
   let has_tactic,pts1 = preprocess pts raw_instr.instr in
-  let pts2 = 
+  let pts2 =
     if has_tactic then
       let gl = nth_goal_of_pftreestate 1 pts1 in
       let env=  pf_env gl in
       let sigma= project gl in
-      let ist = {ltacvars = ([],[]); ltacrecvars = []; 
+      let ist = {ltacvars = ([],[]); ltacrecvars = [];
 		 gsigma = sigma; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
-      let instr = 
+      let instr =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
       let lock_focus = is_focussing_instr instr.instr in
       let marker= Proof_instr (lock_focus,instr) in
-	solve_nth_pftreestate 1 
+	solve_nth_pftreestate 1
 	  (abstract_operation marker (tclTHEN (eval_instr instr) clean_tmp)) pts1
     else pts1 in
       postprocess pts2 raw_instr.instr
@@ -1486,8 +1486,8 @@ let proof_instr raw_instr =
 (*
 
 (* STUFF FOR ITERATED RELATIONS *)
-let decompose_bin_app t= 
-  let hd,args = destApp 
+let decompose_bin_app t=
+  let hd,args = destApp
 
 let identify_transitivity_lemma c =
   let varx,tx,c1 = destProd c in
@@ -1498,4 +1498,4 @@ let identify_transitivity_lemma c =
   let p2=pop lp2 in
   let p3=pop lp3 in
 *)
-    
+