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, 584 insertions, 584 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9087f51798..90eb499422 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,8 +1,8 @@
 open Printer
 open Util
 open Term
-open Termops 
-open Names 
+open Termops
+open Names
 open Declarations
 open Pp
 open Entries
@@ -16,7 +16,7 @@ open Indfun_common
 open Libnames
 
 let msgnl = Pp.msgnl
-  
+
 
 let observe strm =
   if do_observe ()
@@ -35,11 +35,11 @@ let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
  with e ->
    let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
-   msgnl (str "observation "++ s++str " raised exception " ++ 
-	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
+   msgnl (str "observation "++ s++str " raised exception " ++
+	    Cerrors.explain_exn e ++ str " on goal " ++ goal );
    raise e;;
 
-let observe_tac_stream s tac g = 
+let observe_tac_stream s tac g =
   if do_observe ()
   then do_observe_tac  s tac g
   else tac g
@@ -52,54 +52,54 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
 (*   else tac *)
 
 
-let list_chop ?(msg="") n l = 
-  try 
-    list_chop n l 
-  with Failure (msg') -> 
+let list_chop ?(msg="") n l =
+  try
+    list_chop n l
+  with Failure (msg') ->
     failwith (msg ^ msg')
-  
+
 
 let make_refl_eq constructor type_of_t t  =
 (*   let refl_equal_term = Lazy.force refl_equal in *)
   mkApp(constructor,[|type_of_t;t|])
 
 
-type pte_info = 
-    { 
+type pte_info =
+    {
       proving_tac : (identifier list ->  Tacmach.tactic);
       is_valid : constr -> bool
     }
 
 type ptes_info = pte_info Idmap.t
 
-type 'a dynamic_info = 
-    { 
+type 'a dynamic_info =
+    {
       nb_rec_hyps : int;
-      rec_hyps : identifier list ; 
+      rec_hyps : identifier list ;
       eq_hyps : identifier list;
       info : 'a
     }
 
-type body_info = constr dynamic_info 
-      
+type body_info = constr dynamic_info
+
 
-let finish_proof dynamic_infos g = 
-  observe_tac "finish" 
+let finish_proof dynamic_infos g =
+  observe_tac "finish"
     ( h_assumption)
     g
-	  
 
-let refine c = 
+
+let refine c =
   Tacmach.refine_no_check c
 
-let thin l = 
+let thin l =
   Tacmach.thin_no_check l
-  
 
-let cut_replacing id t tac :tactic= 
+
+let cut_replacing id t tac :tactic=
   tclTHENS (cut t)
     [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
-      tac 
+      tac
     ]
 
 let intro_erasing id = tclTHEN (thin [id]) (introduction id)
@@ -108,54 +108,54 @@ let intro_erasing id = tclTHEN (thin [id]) (introduction id)
 
 let rec_hyp_id = id_of_string "rec_hyp"
 
-let is_trivial_eq t = 
-  let res =   try 
+let is_trivial_eq t =
+  let res =   try
     begin
-      match kind_of_term t with 
-	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+      match kind_of_term t with
+	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
 	    eq_constr t1 t2
 	| App(f,[|t1;a1;t2;a2|]) when eq_constr f (jmeq ())  ->
 	    eq_constr t1 t2 && eq_constr a1 a2
-	| _ -> false 
+	| _ -> false
     end
   with _ -> false
   in
 (*   observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
   res
 
-let rec incompatible_constructor_terms t1 t2 = 
-  let c1,arg1 = decompose_app t1 
-  and c2,arg2 = decompose_app t2 
-  in 
+let rec incompatible_constructor_terms t1 t2 =
+  let c1,arg1 = decompose_app t1
+  and c2,arg2 = decompose_app t2
+  in
   (not (eq_constr t1 t2)) &&
-    isConstruct c1 && isConstruct c2 && 
+    isConstruct c1 && isConstruct c2 &&
     (
-      not (eq_constr c1 c2) || 
+      not (eq_constr c1 c2) ||
 	List.exists2 incompatible_constructor_terms arg1 arg2
     )
 
-let is_incompatible_eq t = 
+let is_incompatible_eq t =
   let res =
     try
-      match kind_of_term t with 
-	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+      match kind_of_term t with
+	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
 	    incompatible_constructor_terms t1 t2
-	| App(f,[|u1;t1;u2;t2|]) when eq_constr f (jmeq ()) -> 
+	| App(f,[|u1;t1;u2;t2|]) when eq_constr f (jmeq ()) ->
 	    (eq_constr u1 u2 &&
 	       incompatible_constructor_terms t1 t2)
-	| _ -> false 
+	| _ -> false
     with _ -> false
-  in 
+  in
   if res then   observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
   res
 
-let change_hyp_with_using msg hyp_id t tac : tactic = 
-  fun g -> 
-    let prov_id = pf_get_new_id hyp_id g in 
+let change_hyp_with_using msg hyp_id t tac : tactic =
+  fun g ->
+    let prov_id = pf_get_new_id hyp_id g in
     tclTHENS
       ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
-      [tclTHENLIST 
-      [	
+      [tclTHENLIST
+      [
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
 	(* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id])
       ]] g
@@ -163,20 +163,20 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
 exception TOREMOVE
 
 
-let prove_trivial_eq h_id context (constructor,type_of_term,term) = 
-  let nb_intros = List.length context in 
+let prove_trivial_eq h_id context (constructor,type_of_term,term) =
+  let nb_intros = List.length context in
   tclTHENLIST
     [
       tclDO nb_intros intro; (* introducing context *)
-      (fun g -> 
-	 let context_hyps =  
-	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) 
+      (fun g ->
+	 let context_hyps =
+	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
 	 in
-	 let context_hyps' = 
+	 let context_hyps' =
 	   (mkApp(constructor,[|type_of_term;term|]))::
 	     (List.map mkVar context_hyps)
 	 in
-	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in 
+	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in
 	 refine to_refine g
       )
     ]
@@ -191,124 +191,124 @@ let find_rectype env c =
   | _ -> raise Not_found
 
 
-let isAppConstruct ?(env=Global.env ()) t = 
-  try 
-    let t',l = find_rectype (Global.env ()) t in 
+let isAppConstruct ?(env=Global.env ()) t =
+  try
+    let t',l = find_rectype (Global.env ()) t in
     observe (str "isAppConstruct : " ++ Printer.pr_lconstr t ++ str " -> " ++ Printer.pr_lconstr (applist  (t',l)));
     true
-  with Not_found -> false 
+  with Not_found -> false
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
     Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
   clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
-    
 
 
-let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  = 
-  let nochange ?t' msg  = 
-    begin 
+
+let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
+  let nochange ?t' msg  =
+    begin
       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
-      failwith "NoChange"; 
+      failwith "NoChange";
     end
-  in    
-  let eq_constr = Reductionops.is_conv env sigma in 
+  in
+  let eq_constr = Reductionops.is_conv env sigma in
   if not (noccurn 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp t) then nochange "not an equality";
     let f_eq,args = destApp t in
-    let constructor,t1,t2,t1_typ = 
-      try 
-	if (eq_constr f_eq (Lazy.force eq)) 
-	then 
+    let constructor,t1,t2,t1_typ =
+      try
+	if (eq_constr f_eq (Lazy.force eq))
+	then
 	  let t1 = (args.(1),args.(0))
-	  and t2 = (args.(2),args.(0)) 
+	  and t2 = (args.(2),args.(0))
 	  and t1_typ = args.(0)
 	  in
 	  (Lazy.force refl_equal,t1,t2,t1_typ)
 	else
-	  if (eq_constr f_eq (jmeq ())) 
-	  then 
+	  if (eq_constr f_eq (jmeq ()))
+	  then
 	    (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
 	  else nochange "not an equality"
       with _ -> nochange "not an equality"
-    in 
-    if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";    
-    let rec compute_substitution sub t1 t2 = 
+    in
+    if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
+    let rec compute_substitution sub t1 t2 =
 (*       observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *)
-      if isRel t2 
-      then 
-	let t2 = destRel t2  in 
-	begin 
-	  try 
-	    let t1' = Intmap.find t2 sub in 
+      if isRel t2
+      then
+	let t2 = destRel t2  in
+	begin
+	  try
+	    let t1' = Intmap.find t2 sub in
 	    if not (eq_constr t1 t1') then nochange "twice bound variable";
 	    sub
-	  with Not_found -> 
+	  with Not_found ->
 	    assert (closed0 t1);
 	    Intmap.add t2 t1 sub
 	end
-      else if isAppConstruct t1 && isAppConstruct t2 
-      then 
+      else if isAppConstruct t1 && isAppConstruct t2
+      then
 	begin
 	  let c1,args1 =  find_rectype env t1
 	  and c2,args2 = find_rectype env t2
-	  in 
+	  in
 	  if not (eq_constr c1 c2) then nochange "cannot solve (diff)";
 	  List.fold_left2 compute_substitution sub args1 args2
 	end
-      else 
+      else
 	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2)  "cannot solve (diff)"
     in
-    let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in 
+    let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
-    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) 
-    let new_end_of_type = 
-      (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 
+    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
+    let new_end_of_type =
+      (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
       *)
-      let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in 
-      let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in 
+      let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in
+      let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in
       List.fold_left (fun end_of_type (i,t)  -> lift 1 (substnl  [t] (i-1) end_of_type))
 	end_of_type_with_pop
 	sub''
     in
     let old_context_length = List.length context + 1 in
-    let witness_fun = 
+    let witness_fun =
       mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t,
 	       mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
 	      )
     in
-    let new_type_of_hyp,ctxt_size,witness_fun = 
-      list_fold_left_i 
-	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> 
-	   try 
-	     let witness = Intmap.find i sub in 
+    let new_type_of_hyp,ctxt_size,witness_fun =
+      list_fold_left_i
+	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
+	   try
+	     let witness = Intmap.find i sub in
 	     if b' <> None then anomaly "can not redefine a rel!";
 	     (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
-	   with Not_found  -> 
+	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
-	1 
+	1
 	(new_end_of_type,0,witness_fun)
 	context
     in
     let new_type_of_hyp =
-      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in 
-    let new_ctxt,new_end_of_type = 
-      decompose_prod_n_assum ctxt_size new_type_of_hyp 
-    in 
-    let prove_new_hyp : tactic = 
+      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
+    let new_ctxt,new_end_of_type =
+      decompose_prod_n_assum ctxt_size new_type_of_hyp
+    in
+    let prove_new_hyp : tactic =
       tclTHEN
 	(tclDO ctxt_size intro)
 	(fun g ->
-	   let all_ids = pf_ids_of_hyps g in 
-	   let new_ids,_  = list_chop ctxt_size all_ids in 
-	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in 
+	   let all_ids = pf_ids_of_hyps g in
+	   let new_ids,_  = list_chop ctxt_size all_ids in
+	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
 	   refine to_refine g
 	)
     in
-    let simpl_eq_tac = 
+    let simpl_eq_tac =
       change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp prove_new_hyp
     in
 (*     observe (str "In " ++ Ppconstr.pr_id hyp_id ++  *)
@@ -328,51 +328,51 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     new_ctxt,new_end_of_type,simpl_eq_tac
 
 
-let is_property ptes_info t_x full_type_of_hyp = 
-  if isApp t_x 
-  then 
-    let pte,args = destApp t_x in 
-    if isVar pte && array_for_all closed0 args 
-    then 
-      try 
-	let info = Idmap.find (destVar pte) ptes_info in 
-	info.is_valid full_type_of_hyp	  
-      with Not_found -> false 
-    else false 
-  else false 
+let is_property ptes_info t_x full_type_of_hyp =
+  if isApp t_x
+  then
+    let pte,args = destApp t_x in
+    if isVar pte && array_for_all closed0 args
+    then
+      try
+	let info = Idmap.find (destVar pte) ptes_info in
+	info.is_valid full_type_of_hyp
+      with Not_found -> false
+    else false
+  else false
 
-let isLetIn t = 
-  match kind_of_term t with 
-    | LetIn _ -> true 
-    | _ -> false 
+let isLetIn t =
+  match kind_of_term t with
+    | LetIn _ -> true
+    | _ -> false
 
 
-let h_reduce_with_zeta = 	 
-  h_reduce 
+let h_reduce_with_zeta =
+  h_reduce
     (Rawterm.Cbv
-       {Rawterm.all_flags 
-	with Rawterm.rDelta = false; 		 
+       {Rawterm.all_flags
+	with Rawterm.rDelta = false;
        })
-  
+
 
 
 let rewrite_until_var arg_num eq_ids : tactic =
-  (* tests if the declares recursive argument is neither a Constructor nor 
-     an applied Constructor since such a form for the recursive argument 
-     will break the Guard when trying to save the Lemma. 
+  (* tests if the declares recursive argument is neither a Constructor nor
+     an applied Constructor since such a form for the recursive argument
+     will break the Guard when trying to save the Lemma.
   *)
-  let test_var g = 
-    let _,args = destApp (pf_concl g) in 
+  let test_var g =
+    let _,args = destApp (pf_concl g) in
     not ((isConstruct args.(arg_num)) || isAppConstruct args.(arg_num))
   in
-  let rec do_rewrite eq_ids g  = 
-    if test_var g 
+  let rec do_rewrite eq_ids g  =
+    if test_var g
     then tclIDTAC g
     else
-      match eq_ids with 
+      match eq_ids with
 	| [] -> anomaly "Cannot find a way to prove recursive property";
-	| eq_id::eq_ids -> 
-	    tclTHEN 
+	| eq_id::eq_ids ->
+	    tclTHEN
 	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
 	      (do_rewrite eq_ids)
 	      g
@@ -380,50 +380,50 @@ let rewrite_until_var arg_num eq_ids : tactic =
   do_rewrite eq_ids
 
 
-let rec_pte_id = id_of_string "Hrec" 
-let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = 
-  let coq_False = Coqlib.build_coq_False () in 
-  let coq_True = Coqlib.build_coq_True () in 
-  let coq_I = Coqlib.build_coq_I () in 
-  let rec scan_type  context type_of_hyp : tactic = 
-    if isLetIn type_of_hyp then 
+let rec_pte_id = id_of_string "Hrec"
+let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
+  let coq_False = Coqlib.build_coq_False () in
+  let coq_True = Coqlib.build_coq_True () in
+  let coq_I = Coqlib.build_coq_I () in
+  let rec scan_type  context type_of_hyp : tactic =
+    if isLetIn type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
-      let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in 
+      let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
       (* length of context didn't change ? *)
-      let new_context,new_typ_of_hyp = 
+      let new_context,new_typ_of_hyp =
 	 decompose_prod_n_assum (List.length context) reduced_type_of_hyp
       in
-        tclTHENLIST 
+        tclTHENLIST
 	[
 	  h_reduce_with_zeta
 	    (Tacticals.onHyp hyp_id)
 	  ;
-	  scan_type new_context new_typ_of_hyp 
-	  
+	  scan_type new_context new_typ_of_hyp
+
 	]
-    else if isProd type_of_hyp 
-    then 
-      begin 
-	let (x,t_x,t') = destProd type_of_hyp in	
-	let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in 
+    else if isProd type_of_hyp
+    then
+      begin
+	let (x,t_x,t') = destProd type_of_hyp in
+	let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in
 	if is_property ptes_infos t_x actual_real_type_of_hyp then
 	  begin
-	    let pte,pte_args =  (destApp t_x) in 
-	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in 
-	    let popped_t' = pop t' in 
-	    let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in 
-	    let prove_new_type_of_hyp = 
-	      let context_length = List.length context in 
+	    let pte,pte_args =  (destApp t_x) in
+	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
+	    let popped_t' = pop t' in
+	    let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
+	    let prove_new_type_of_hyp =
+	      let context_length = List.length context in
 	      tclTHENLIST
-		[ 
-		  tclDO context_length intro; 
-		  (fun g ->  
-		     let context_hyps_ids = 
+		[
+		  tclDO context_length intro;
+		  (fun g ->
+		     let context_hyps_ids =
 		       fst (list_chop ~msg:"rec hyp : context_hyps"
 			      context_length (pf_ids_of_hyps g))
 		     in
-		     let rec_pte_id = pf_get_new_id rec_pte_id g in 
-		     let to_refine = 
+		     let rec_pte_id = pf_get_new_id rec_pte_id g in
+		     let to_refine =
 		       applist(mkVar hyp_id,
 			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
 			      )
@@ -440,39 +440,39 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		  )
 		]
 	    in
-	    tclTHENLIST 
+	    tclTHENLIST
 	      [
 (* 		observe_tac "hyp rec"  *)
 		  (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp);
 		scan_type context popped_t'
 	      ]
 	  end
-	else if eq_constr t_x coq_False then 
+	else if eq_constr t_x coq_False then
 	  begin
 (* 	    observe (str "Removing : "++ Ppconstr.pr_id hyp_id++  *)
 (* 		       str " since it has False in its preconds " *)
 (* 		    ); *)
 	    raise TOREMOVE;  (* False -> .. useless *)
 	  end
-	else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *) 
+	else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *)
 	else if eq_constr t_x coq_True  (* Trivial => we remove this precons *)
-	then 
+	then
 (* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
 (* 		       str " removing useless precond True" *)
 (* 		    );  *)
 	  let popped_t' = pop t' in
-	  let real_type_of_hyp = 
-	    it_mkProd_or_LetIn ~init:popped_t' context 
-	  in 
-	  let prove_trivial =  
-	    let nb_intro = List.length context in 
+	  let real_type_of_hyp =
+	    it_mkProd_or_LetIn ~init:popped_t' context
+	  in
+	  let prove_trivial =
+	    let nb_intro = List.length context in
 	    tclTHENLIST [
 	      tclDO nb_intro intro;
-	      (fun g -> 
-		 let context_hyps = 
+	      (fun g ->
+		 let context_hyps =
 		   fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
 		 in
-		 let to_refine = 
+		 let to_refine =
 		   applist (mkVar hyp_id,
 			    List.rev (coq_I::List.map mkVar context_hyps)
 			   )
@@ -482,19 +482,19 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	    ]
 	  in
 	  tclTHENLIST[
-	    change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp 
+	    change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp
 	      ((* observe_tac "prove_trivial" *) prove_trivial);
 	    scan_type context popped_t'
 	  ]
-	else if is_trivial_eq t_x 
-	then (*  t_x :=  t = t   => we remove this precond *) 
+	else if is_trivial_eq t_x
+	then (*  t_x :=  t = t   => we remove this precond *)
 	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn ~init:popped_t' context
 	  in
 	  let hd,args = destApp t_x in
-	  let get_args hd args = 
-	    if eq_constr hd (Lazy.force eq) 
+	  let get_args hd args =
+	    if eq_constr hd (Lazy.force eq)
 	    then (Lazy.force refl_equal,args.(0),args.(1))
 	    else (jmeq_refl (),args.(0),args.(1))
 	  in
@@ -504,77 +504,77 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		"prove_trivial_eq"
 		hyp_id
 		real_type_of_hyp
-		((* observe_tac "prove_trivial_eq" *) 
+		((* observe_tac "prove_trivial_eq" *)
 		  (prove_trivial_eq hyp_id context (get_args hd args)));
 	      scan_type context popped_t'
-	    ] 
-	else 
+	    ]
+	else
 	  begin
-	    try 
-	      let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in 
+	    try
+	      let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in
 	      tclTHEN
-		tac 
+		tac
 		(scan_type new_context new_t')
-	    with Failure "NoChange" -> 
-	      (* Last thing todo : push the rel in the context and continue *) 
+	    with Failure "NoChange" ->
+	      (* Last thing todo : push the rel in the context and continue *)
 	      scan_type ((x,None,t_x)::context) t'
 	  end
       end
     else
       tclIDTAC
-  in 
-  try 
+  in
+  try
     scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
-  with TOREMOVE -> 
+  with TOREMOVE ->
     thin [hyp_id],[]
 
 
-let clean_goal_with_heq ptes_infos continue_tac dyn_infos  = 
-  fun g -> 
-    let env = pf_env g 
-    and sigma = project g 
+let clean_goal_with_heq ptes_infos continue_tac dyn_infos  =
+  fun g ->
+    let env = pf_env g
+    and sigma = project g
     in
-    let tac,new_hyps = 
-      List.fold_left ( 
+    let tac,new_hyps =
+      List.fold_left (
 	fun (hyps_tac,new_hyps) hyp_id ->
-	  let hyp_tac,new_hyp = 
-	    clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma 
+	  let hyp_tac,new_hyp =
+	    clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma
 	  in
 	  (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
       )
 	(tclIDTAC,[])
 	dyn_infos.rec_hyps
     in
-    let new_infos = 
-      { dyn_infos with 
-	  rec_hyps = new_hyps; 
+    let new_infos =
+      { dyn_infos with
+	  rec_hyps = new_hyps;
 	  nb_rec_hyps  = List.length new_hyps
       }
     in
-    tclTHENLIST 
+    tclTHENLIST
       [
 	tac ;
 	(* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos)
       ]
-      g    
+      g
 
 let heq_id = id_of_string "Heq"
 
-let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = 
-  fun g -> 
-    let heq_id = pf_get_new_id heq_id g in 
+let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
+  fun g ->
+    let heq_id = pf_get_new_id heq_id g in
     let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
     tclTHENLIST
-      [ 
-	(* We first introduce the variables *) 
+      [
+	(* We first introduce the variables *)
 	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
 	(* Then the equation itself *)
 	introduction_no_check heq_id;
-	(* Then the new hypothesis *) 
+	(* Then the new hypothesis *)
 	tclMAP introduction_no_check dyn_infos.rec_hyps;
-	(* observe_tac "after_introduction"  *)(fun g' -> 
+	(* observe_tac "after_introduction"  *)(fun g' ->
 	   (* We get infos on the equations introduced*)
-	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in 
+	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
 	   (* compute the new value of the body *)
 	   let new_term_value =
 	     match kind_of_term new_term_value_eq with
@@ -592,31 +592,31 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   )
 	 in
 	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
-	 let new_infos = 
-	   {dyn_infos with 
+	 let new_infos =
+	   {dyn_infos with
 	      info = new_body;
 	      eq_hyps = heq_id::dyn_infos.eq_hyps
 	   }
-	 in 
+	 in
 	 clean_goal_with_heq ptes_infos continue_tac new_infos  g'
       )
     ]
       g
 
 
-let my_orelse tac1 tac2 g = 
-  try 
-    tac1 g 
-  with e -> 
+let my_orelse tac1 tac2 g =
+  try
+    tac1 g
+  with e ->
 (*     observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *)
-    tac2 g 
+    tac2 g
 
-let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = 
-  let args = Array.of_list (List.map mkVar  args_id) in 
-  let instanciate_one_hyp hid = 
+let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
+  let args = Array.of_list (List.map mkVar  args_id) in
+  let instanciate_one_hyp hid =
     my_orelse
       ( (* we instanciate the hyp if possible  *)
-	fun g -> 
+	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
 	    pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
@@ -625,21 +625,21 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	  ] g
       )
       ( (*
-	  if not then we are in a mutual function block 
+	  if not then we are in a mutual function block
 	  and this hyp is a recursive hyp on an other function.
-	  
-	  We are not supposed to use it while proving this 
-	  principle so that we can trash it 
-	  
+
+	  We are not supposed to use it while proving this
+	  principle so that we can trash it
+
 	*)
-	(fun g -> 
+	(fun g ->
 (* 	   observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
 	   thin [hid] g
 	)
       )
   in
-  if args_id = []  
-  then 
+  if args_id = []
+  then
     tclTHENLIST [
       tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
       do_prove hyps
@@ -649,32 +649,32 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
       [
 	tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
 	tclMAP instanciate_one_hyp hyps;
-	(fun g ->  
-	   let all_g_hyps_id = 
+	(fun g ->
+	   let all_g_hyps_id =
 	     List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
-	   in 
-	   let remaining_hyps = 
+	   in
+	   let remaining_hyps =
 	     List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
 	   in
 	   do_prove remaining_hyps g
 	  )
       ]
 
-let build_proof 
+let build_proof
     (interactive_proof:bool)
     (fnames:constant list)
     ptes_infos
     dyn_infos
     : tactic =
-  let rec build_proof_aux do_finalize dyn_infos : tactic = 
-    fun g -> 
+  let rec build_proof_aux do_finalize dyn_infos : tactic =
+    fun g ->
 (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
-	match kind_of_term dyn_infos.info with 
-	  | Case(ci,ct,t,cb) -> 
-	      let do_finalize_t dyn_info' = 
+	match kind_of_term dyn_infos.info with
+	  | Case(ci,ct,t,cb) ->
+	      let do_finalize_t dyn_info' =
 		fun g ->
-		  let t = dyn_info'.info in 
-		  let dyn_infos = {dyn_info' with info = 
+		  let t = dyn_info'.info in
+		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
 		  let g_nb_prod = nb_prod (pf_concl g) in
 		  let type_of_term = pf_type_of g t in
@@ -686,21 +686,21 @@ let build_proof
 		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		      thin dyn_infos.rec_hyps;
 		      pattern_option [(false,[1]),t] None;
-		      (fun g -> observe_tac "toto" (    
+		      (fun g -> observe_tac "toto" (
 			 tclTHENSEQ [h_simplest_case t;
-				     (fun g' -> 
-					let g'_nb_prod = nb_prod (pf_concl g') in 
-					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+				     (fun g' ->
+					let g'_nb_prod = nb_prod (pf_concl g') in
+					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
 			 		observe_tac "treat_new_case"
-					  (treat_new_case  
+					  (treat_new_case
 					     ptes_infos
-					     nb_instanciate_partial 
-					     (build_proof do_finalize) 
-					     t 
+					     nb_instanciate_partial
+					     (build_proof do_finalize)
+					     t
 					     dyn_infos)
 					  g'
 				     )
-			
+
 				    ]) g
 		      )
 		    ]
@@ -715,25 +715,25 @@ let build_proof
 			intro
 			(fun g' ->
 			   let (id,_,_) = pf_last_hyp g' in
-			   let new_term = 
-			     pf_nf_betaiota g' 
-			       (mkApp(dyn_infos.info,[|mkVar id|])) 
+			   let new_term =
+			     pf_nf_betaiota g'
+			       (mkApp(dyn_infos.info,[|mkVar id|]))
 			   in
 			   let new_infos = {dyn_infos with info = new_term} in
-			   let do_prove new_hyps = 
-			     build_proof do_finalize 
+			   let do_prove new_hyps =
+			     build_proof do_finalize
 			       {new_infos with
-			       	  rec_hyps = new_hyps; 
+			       	  rec_hyps = new_hyps;
 				  nb_rec_hyps  = List.length new_hyps
 			       }
-			   in 
+			   in
 (* 			   observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
 			     (* 			   build_proof do_finalize new_infos g' *)
 			) g
 		  | _ ->
-		      do_finalize dyn_infos g 
+		      do_finalize dyn_infos g
 	      end
-	  | Cast(t,_,_) -> 
+	  | Cast(t,_,_) ->
 	      build_proof do_finalize {dyn_infos with info = t} g
 	  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
 	      do_finalize dyn_infos g
@@ -743,15 +743,15 @@ let build_proof
 		match kind_of_term f with
 		  | App _ -> assert false (* we have collected all the app in decompose_app *)
 		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
-		      let new_infos = 
-			{ dyn_infos with 
+		      let new_infos =
+			{ dyn_infos with
 			    info = (f,args)
 			}
 		      in
 		      build_proof_args do_finalize new_infos  g
 		  | Const c when not (List.mem c fnames) ->
-		      let new_infos = 
-			{ dyn_infos with 
+		      let new_infos =
+			{ dyn_infos with
 			    info = (f,args)
 			}
 		      in
@@ -759,93 +759,93 @@ let build_proof
 		      build_proof_args do_finalize new_infos g
 		  | Const _ ->
 		      do_finalize dyn_infos  g
-		  | Lambda _ -> 
+		  | Lambda _ ->
 		      let new_term =
-                        Reductionops.nf_beta Evd.empty dyn_infos.info in 
-		      build_proof do_finalize {dyn_infos with info = new_term} 
+                        Reductionops.nf_beta Evd.empty dyn_infos.info in
+		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
-		  | LetIn _ -> 
-		      let new_infos = 
-			{ dyn_infos with info = nf_betaiotazeta dyn_infos.info } 
-		      in 
-
-		      tclTHENLIST 
-			[tclMAP 
-			   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
+		  | LetIn _ ->
+		      let new_infos =
+			{ dyn_infos with info = nf_betaiotazeta dyn_infos.info }
+		      in
+
+		      tclTHENLIST
+			[tclMAP
+			   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
 			   dyn_infos.rec_hyps;
 			 h_reduce_with_zeta Tacticals.onConcl;
 			 build_proof do_finalize new_infos
-			] 
+			]
 			g
-		  | Cast(b,_,_) -> 
+		  | Cast(b,_,_) ->
 		      build_proof do_finalize {dyn_infos with info = b } g
 		  | Case _ | Fix _ | CoFix _ ->
-		      let new_finalize dyn_infos = 
-			let new_infos = 
-			  { dyn_infos with 
+		      let new_finalize dyn_infos =
+			let new_infos =
+			  { dyn_infos with
 			      info = dyn_infos.info,args
 			  }
-			in 
-			build_proof_args do_finalize new_infos 
-		      in 
+			in
+			build_proof_args do_finalize new_infos
+		      in
 		      build_proof new_finalize {dyn_infos  with info = f } g
 	      end
 	  | Fix _ | CoFix _ ->
 	      error ( "Anonymous local (co)fixpoints are not handled yet")
 
-	  | Prod _ -> error "Prod" 
-	  | LetIn _ -> 
-	      let new_infos = 
-		{ dyn_infos with 
-		    info = nf_betaiotazeta dyn_infos.info 
+	  | Prod _ -> error "Prod"
+	  | LetIn _ ->
+	      let new_infos =
+		{ dyn_infos with
+		    info = nf_betaiotazeta dyn_infos.info
 		}
-	      in 
+	      in
 
-	      tclTHENLIST 
-		[tclMAP 
-		   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
+	      tclTHENLIST
+		[tclMAP
+		   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
 		   dyn_infos.rec_hyps;
 		 h_reduce_with_zeta Tacticals.onConcl;
 		 build_proof do_finalize new_infos
 		] g
-	  | Rel _ -> anomaly "Free var in goal conclusion !" 
+	  | Rel _ -> anomaly "Free var in goal conclusion !"
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
     observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
-      let (f_args',args) = dyn_infos.info in 
+      let (f_args',args) = dyn_infos.info in
       let tac : tactic =
-	fun g -> 
+	fun g ->
 	match args with
 	  | []  ->
-	      do_finalize {dyn_infos with info = f_args'} g 
+	      do_finalize {dyn_infos with info = f_args'} g
 	  | arg::args ->
 (* 		observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
 (* 			fnl () ++  *)
 (* 			pr_goal (Tacmach.sig_it g) *)
 (* 			); *)
 	      let do_finalize dyn_infos =
-		let new_arg = dyn_infos.info in 
+		let new_arg = dyn_infos.info in
 		(* 		tclTRYD *)
 		(build_proof_args
 		   do_finalize
 		   {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
 		)
 	      in
-	      build_proof do_finalize 
+	      build_proof do_finalize
 		{dyn_infos with info = arg }
 		g
       in
       (* observe_tac "build_proof_args" *) (tac ) g
    in
-   let do_finish_proof dyn_infos = 
-     (* tclTRYD *) (clean_goal_with_heq 
+   let do_finish_proof dyn_infos =
+     (* tclTRYD *) (clean_goal_with_heq
       ptes_infos
       finish_proof dyn_infos)
   in
   (* observe_tac "build_proof" *)
-    (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) 
+    (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
 
 
 
@@ -858,16 +858,16 @@ let build_proof
 
 
 
-(* Proof of principles from structural functions *) 
+(* Proof of principles from structural functions *)
 let is_pte_type t =
   isSort ((strip_prod t))
-    
+
 let is_pte (_,_,t) = is_pte_type t
 
 
 
 
-type static_fix_info = 
+type static_fix_info =
     {
       idx : int;
       name : identifier;
@@ -875,18 +875,18 @@ type static_fix_info =
       offset : int;
       nb_realargs : int;
       body_with_param : constr;
-      num_in_block : int 
+      num_in_block : int
     }
 
 
 
-let prove_rec_hyp_for_struct fix_info = 
-      (fun  eq_hyps -> tclTHEN 
+let prove_rec_hyp_for_struct fix_info =
+      (fun  eq_hyps -> tclTHEN
 	(rewrite_until_var (fix_info.idx) eq_hyps)
-	(fun g -> 
-	   let _,pte_args = destApp (pf_concl g) in 
-	   let rec_hyp_proof = 
-	     mkApp(mkVar fix_info.name,array_get_start pte_args) 
+	(fun g ->
+	   let _,pte_args = destApp (pf_concl g) in
+	   let rec_hyp_proof =
+	     mkApp(mkVar fix_info.name,array_get_start pte_args)
 	   in
 	   refine rec_hyp_proof g
 	))
@@ -894,38 +894,38 @@ let prove_rec_hyp_for_struct fix_info =
 let prove_rec_hyp fix_info  =
   { proving_tac = prove_rec_hyp_for_struct fix_info
   ;
-    is_valid = fun _ -> true 
+    is_valid = fun _ -> true
   }
 
 
 exception Not_Rec
-    
-let generalize_non_dep hyp g = 
+
+let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
-  let hyps = [hyp] in 
-  let env = Global.env () in 
-  let hyp_typ = pf_type_of g (mkVar hyp) in 
-  let to_revert,_ = 
+  let hyps = [hyp] in
+  let env = Global.env () in
+  let hyp_typ = pf_type_of g (mkVar hyp) in
+  let to_revert,_ =
     Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if List.mem hyp hyps
 	or List.exists (occur_var_in_decl env hyp) keep
 	or occur_var env hyp hyp_typ
-	or Termops.is_section_variable hyp (* should be dangerous *) 
+	or Termops.is_section_variable hyp (* should be dangerous *)
       then (clear,decl::keep)
       else (hyp::clear,keep))
       ~init:([],[]) (pf_env g)
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
-  tclTHEN 
+  tclTHEN
     ((* observe_tac "h_generalize" *) (h_generalize  (List.map mkVar to_revert) ))
     ((* observe_tac "thin" *) (thin to_revert))
     g
-  
+
 let id_of_decl (na,_,_) =  (Nameops.out_name na)
 let var_of_decl decl = mkVar (id_of_decl decl)
-let revert idl = 
-  tclTHEN 
-    (generalize (List.map mkVar idl)) 
+let revert idl =
+  tclTHEN
+    (generalize (List.map mkVar idl))
     (thin idl)
 
 let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
@@ -950,7 +950,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "f_body_with_params_and_other_fun " ++  pr_lconstr f_body_with_params_and_other_fun); *)
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
 (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
-  let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) 
+  let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
     (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
@@ -971,7 +971,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   Command.start_proof
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
-      i*) 
+      i*)
     (mk_equation_id f_id)
     (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
@@ -981,72 +981,72 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 
 
 
-  
+
 let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
-  let equation_lemma = 
-    try 
-      let finfos = find_Function_infos (destConst f) in 
+  let equation_lemma =
+    try
+      let finfos = find_Function_infos (destConst f) in
       mkConst (Option.get finfos.equation_lemma)
-    with (Not_found | Option.IsNone as e) -> 
-      let f_id = id_of_label (con_label (destConst f)) in 
+    with (Not_found | Option.IsNone as e) ->
+      let f_id = id_of_label (con_label (destConst f)) in
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
-	i*) 
-      let equation_lemma_id = (mk_equation_id f_id) in 
+	i*)
+      let equation_lemma_id = (mk_equation_id f_id) in
       generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
       let _ =
-	match e with 
-	  | Option.IsNone -> 
-	      let finfos = find_Function_infos (destConst f) in 
-	      update_Function 
+	match e with
+	  | Option.IsNone ->
+	      let finfos = find_Function_infos (destConst f) in
+	      update_Function
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> Util.anomaly "Not a constant" 
+					    | _ -> Util.anomaly "Not a constant"
 					 )
 		}
-	  | _ -> () 
+	  | _ -> ()
 
-      in 
+      in
       Tacinterp.constr_of_id (pf_env g) equation_lemma_id
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
       (tclDO nb_intro_to_do intro)
       (
-	fun g' -> 
-	  let just_introduced = nLastDecls nb_intro_to_do g' in 
-	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in 
+	fun g' ->
+	  let just_introduced = nLastDecls nb_intro_to_do g' in
+	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
 	  tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
       )
       g
 
 let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
-  fun g -> 
-    let princ_type = pf_concl g in 
-    let princ_info = compute_elim_sig princ_type in 
-    let fresh_id = 
-      let avoid = ref (pf_ids_of_hyps g) in 
-      (fun na -> 
-	 let new_id = 
-	   match na with 
-	       Name id -> fresh_id !avoid (string_of_id id) 
+  fun g ->
+    let princ_type = pf_concl g in
+    let princ_info = compute_elim_sig princ_type in
+    let fresh_id =
+      let avoid = ref (pf_ids_of_hyps g) in
+      (fun na ->
+	 let new_id =
+	   match na with
+	       Name id -> fresh_id !avoid (string_of_id id)
 	     | Anonymous -> fresh_id !avoid "H"
 	 in
-	 avoid := new_id :: !avoid; 
+	 avoid := new_id :: !avoid;
 	 (Name new_id)
       )
     in
-    let fresh_decl = 
-      (fun (na,b,t) -> 
+    let fresh_decl =
+      (fun (na,b,t) ->
 	 (fresh_id na,b,t)
       )
     in
-    let princ_info : elim_scheme = 
-      { princ_info with 
+    let princ_info : elim_scheme =
+      { princ_info with
 	  params = List.map fresh_decl princ_info.params;
-	  predicates = List.map fresh_decl princ_info.predicates; 
-	  branches = List.map fresh_decl princ_info.branches; 
+	  predicates = List.map fresh_decl princ_info.predicates;
+	  branches = List.map fresh_decl princ_info.branches;
 	  args = List.map fresh_decl princ_info.args
       }
     in
@@ -1062,15 +1062,15 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
     let fbody = get_body fnames.(fun_num) in
-    let f_ctxt,f_body = decompose_lam fbody in 
-    let f_ctxt_length = List.length f_ctxt in 
-    let diff_params = princ_info.nparams - f_ctxt_length in 
-    let full_params,princ_params,fbody_with_full_params = 
+    let f_ctxt,f_body = decompose_lam fbody in
+    let f_ctxt_length = List.length f_ctxt in
+    let diff_params = princ_info.nparams - f_ctxt_length in
+    let full_params,princ_params,fbody_with_full_params =
       if diff_params > 0
-      then 
-	let princ_params,full_params = 
-	  list_chop  diff_params princ_info.params 
-	in 
+      then
+	let princ_params,full_params =
+	  list_chop  diff_params princ_info.params
+	in
 	(full_params, (* real params *)
 	 princ_params, (* the params of the principle which are not params of the function *)
 	 substl (* function instanciated with real params *)
@@ -1078,9 +1078,9 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	   f_body
 	)
       else
-	let f_ctxt_other,f_ctxt_params = 
-	  list_chop (- diff_params) f_ctxt in 
-	let f_body = compose_lam f_ctxt_other f_body in 
+	let f_ctxt_other,f_ctxt_params =
+	  list_chop (- diff_params) f_ctxt in
+	let f_body = compose_lam f_ctxt_other f_body in
 	(princ_info.params, (* real params *)
 	 [],(* all params are full params *)
 	 substl (* function instanciated with real params *)
@@ -1099,32 +1099,32 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 (*     observe (str "fbody_with_full_params := " ++  *)
 (* 	       pr_lconstr fbody_with_full_params *)
 (* 	    );  *)
-    let all_funs_with_full_params = 
+    let all_funs_with_full_params =
       Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
     in
-    let fix_offset = List.length princ_params in 
-    let ptes_to_fix,infos = 
-      match kind_of_term fbody_with_full_params with 
-	| Fix((idxs,i),(names,typess,bodies)) -> 
-	    let bodies_with_all_params = 
-	      Array.map 
-		(fun body -> 
+    let fix_offset = List.length princ_params in
+    let ptes_to_fix,infos =
+      match kind_of_term fbody_with_full_params with
+	| Fix((idxs,i),(names,typess,bodies)) ->
+	    let bodies_with_all_params =
+	      Array.map
+		(fun body ->
 		   Reductionops.nf_betaiota Evd.empty
 		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
 			      List.rev_map var_of_decl princ_params))
 		)
 		bodies
 	    in
-	    let info_array = 
-	      Array.mapi 
-		(fun i types -> 
+	    let info_array =
+	      Array.mapi
+		(fun i types ->
 		   let types = prod_applist types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
 		     name = Nameops.out_name (fresh_id names.(i));
-		     types = types; 
+		     types = types;
 		     offset = fix_offset;
-		     nb_realargs = 
-		       List.length 
+		     nb_realargs =
+		       List.length
 			 (fst (decompose_lam bodies.(i))) - fix_offset;
 		     body_with_param = bodies_with_all_params.(i);
 		     num_in_block = i
@@ -1132,65 +1132,65 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		)
 		typess
 	    in
-	    let pte_to_fix,rev_info = 
-	      list_fold_left_i 
-		(fun i (acc_map,acc_info) (pte,_,_) -> 
-		   let infos = info_array.(i) in 
-		   let type_args,_ = decompose_prod infos.types in 
-		   let nargs = List.length type_args in 
+	    let pte_to_fix,rev_info =
+	      list_fold_left_i
+		(fun i (acc_map,acc_info) (pte,_,_) ->
+		   let infos = info_array.(i) in
+		   let type_args,_ = decompose_prod infos.types in
+		   let nargs = List.length type_args in
 		   let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in
 		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
 		   let app_f = mkApp(f,first_args) in
-		   let pte_args = (Array.to_list first_args)@[app_f] in 
-		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in 
-		   let body_with_param,num = 
-		     let body = get_body fnames.(i) in 
-		     let body_with_full_params = 
+		   let pte_args = (Array.to_list first_args)@[app_f] in
+		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
+		   let body_with_param,num =
+		     let body = get_body fnames.(i) in
+		     let body_with_full_params =
 		       Reductionops.nf_betaiota Evd.empty (
 			 applist(body,List.rev_map var_of_decl full_params))
 		     in
-		     match kind_of_term body_with_full_params with 
-		       | Fix((_,num),(_,_,bs)) -> 
+		     match kind_of_term body_with_full_params with
+		       | Fix((_,num),(_,_,bs)) ->
 			       Reductionops.nf_betaiota Evd.empty
 				 (
 				   (applist
-				      (substl 
-					 (List.rev 
-					    (Array.to_list all_funs_with_full_params)) 
+				      (substl
+					 (List.rev
+					    (Array.to_list all_funs_with_full_params))
 					 bs.(num),
 				       List.rev_map var_of_decl princ_params))
 				 ),num
 			 | _ -> error "Not a mutual block"
 		   in
-		   let info = 
-		     {infos with 
+		   let info =
+		     {infos with
 			types = compose_prod type_args app_pte;
 			 body_with_param = body_with_param;
 			 num_in_block = num
 		     }
-		   in 
+		   in
 (* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
 (* 			      str " to " ++ Ppconstr.pr_id info.name); *)
 		   (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
 		   )
-		0 
-		(Idmap.empty,[]) 
+		0
+		(Idmap.empty,[])
 		(List.rev princ_info.predicates)
 	    in
 	    pte_to_fix,List.rev rev_info
 	| _ -> Idmap.empty,[]
     in
-    let mk_fixes : tactic = 
-      let pre_info,infos = list_chop fun_num infos in 
-      match pre_info,infos with 
+    let mk_fixes : tactic =
+      let pre_info,infos = list_chop fun_num infos in
+      match pre_info,infos with
 	| [],[] -> tclIDTAC
-	| _, this_fix_info::others_infos -> 
+	| _, this_fix_info::others_infos ->
 	    let other_fix_infos =
 	      List.map
-		(fun fi -> fi.name,fi.idx + 1 ,fi.types) 
+		(fun fi -> fi.name,fi.idx + 1 ,fi.types)
 		(pre_info@others_infos)
-	    in 
-	    if other_fix_infos = [] 
+	    in
+	    if other_fix_infos = []
 	    then
 	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
@@ -1199,34 +1199,34 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	| _ -> anomaly "Not a valid information"
     in
     let first_tac : tactic = (* every operations until fix creations *)
-      tclTHENSEQ 
-	[ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params)); 
-	  (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates)); 
-	  (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches)); 
+      tclTHENSEQ
+	[ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params));
+	  (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates));
+	  (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches));
 	  (* observe_tac "building fixes" *) mk_fixes;
 	]
     in
-    let intros_after_fixes : tactic = 
-      fun gl -> 
+    let intros_after_fixes : tactic =
+      fun gl ->
 	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
-	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in 
+	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in
 	  let fix_info = Idmap.find  pte ptes_to_fix in
-	  let nb_args = fix_info.nb_realargs in 
+	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
 	    [
 	      (* observe_tac ("introducing args") *) (tclDO nb_args intro);
 	      (fun g -> (* replacement of the function by its body *)
-		 let args = nLastDecls nb_args g in 
+		 let args = nLastDecls nb_args g in
 		 let fix_body = fix_info.body_with_param in
 (* 		 observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
 		 let args_id = List.map (fun (id,_,_) -> id) args in
-		 let dyn_infos = 
+		 let dyn_infos =
 		   {
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
-		     info = 
+		     info =
 		       Reductionops.nf_betaiota Evd.empty
 			 (applist(fix_body,List.rev_map mkVar args_id));
 		     eq_hyps = []
@@ -1235,42 +1235,42 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 tclTHENSEQ
 		   [
 (* 		     observe_tac "do_replace"  *)
-		       (do_replace 
-			  full_params 
-			  (fix_info.idx + List.length princ_params) 
+		       (do_replace
+			  full_params
+			  (fix_info.idx + List.length princ_params)
 			  (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
-			  (all_funs.(fix_info.num_in_block)) 
-			  fix_info.num_in_block 
+			  (all_funs.(fix_info.num_in_block))
+			  fix_info.num_in_block
 			  all_funs
 		       );
 (* 		     observe_tac "do_replace"  *)
 (* 		       (do_replace princ_info.params fix_info.idx args_id *)
 (* 			  (List.hd (List.rev pte_args)) fix_body); *)
-		     let do_prove = 
-		       build_proof 
+		     let do_prove =
+		       build_proof
 			 interactive_proof
-			 (Array.to_list fnames) 
+			 (Array.to_list fnames)
 			 (Idmap.map prove_rec_hyp ptes_to_fix)
 		     in
-		     let prove_tac branches  = 
-		       let dyn_infos = 
-			 {dyn_infos with 
+		     let prove_tac branches  =
+		       let dyn_infos =
+			 {dyn_infos with
 			    rec_hyps = branches;
 			    nb_rec_hyps = List.length branches
 			 }
 		       in
 		       observe_tac "cleaning" (clean_goal_with_heq
-			 (Idmap.map prove_rec_hyp ptes_to_fix) 
-			 do_prove 
+			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 do_prove
 			 dyn_infos)
 		     in
 (* 		     observe (str "branches := " ++ *)
 (* 				prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++  fnl () ++ *)
 (* 			   str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
-			   
+
 (* 			   ); *)
-		     (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac 
-		       (List.rev_map id_of_decl princ_info.branches) 
+		     (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac
+		       (List.rev_map id_of_decl princ_info.branches)
 		       (List.rev args_id))
 		   ]
 		   g
@@ -1282,14 +1282,14 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    [
 	      tclDO nb_args intro;
 	      (fun g -> (* replacement of the function by its body *)
-		 let args = nLastDecls nb_args g in 
+		 let args = nLastDecls nb_args g in
 		 let args_id = List.map (fun (id,_,_) -> id) args in
-		 let dyn_infos = 
+		 let dyn_infos =
 		   {
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
-		     info = 
-		       Reductionops.nf_betaiota Evd.empty 
+		     info =
+		       Reductionops.nf_betaiota Evd.empty
 			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
@@ -1300,44 +1300,44 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
 		   [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)];
-		    let do_prove = 
-		      build_proof 
+		    let do_prove =
+		      build_proof
 			interactive_proof
-			(Array.to_list fnames) 
+			(Array.to_list fnames)
 			 (Idmap.map prove_rec_hyp ptes_to_fix)
 		    in
-		    let prove_tac branches  = 
-		      let dyn_infos = 
-			 {dyn_infos with 
+		    let prove_tac branches  =
+		      let dyn_infos =
+			 {dyn_infos with
 			    rec_hyps = branches;
 			    nb_rec_hyps = List.length branches
 			 }
 		      in
 		       clean_goal_with_heq
-			 (Idmap.map prove_rec_hyp ptes_to_fix) 
-			 do_prove 
+			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 do_prove
 			 dyn_infos
 		    in
-		    instanciate_hyps_with_args prove_tac 
-		       (List.rev_map id_of_decl princ_info.branches) 
+		    instanciate_hyps_with_args prove_tac
+		       (List.rev_map id_of_decl princ_info.branches)
 		      (List.rev args_id)
 		   ]
 		   g
 	      )
-	    ] 
+	    ]
 	  gl
     in
-    tclTHEN 
+    tclTHEN
       first_tac
       intros_after_fixes
       g
-	    
 
 
 
 
 
-(* Proof of principles of general functions *) 
+
+(* Proof of principles of general functions *)
 let h_id = Recdef.h_id
 and hrec_id = Recdef.hrec_id
 and acc_inv_id = Recdef.acc_inv_id
@@ -1376,73 +1376,73 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 	    gls
 
 
-let backtrack_eqs_until_hrec hrec eqs : tactic = 
-  fun gls -> 
-    let eqs = List.map mkVar eqs in 
-    let rewrite = 
+let backtrack_eqs_until_hrec hrec eqs : tactic =
+  fun gls ->
+    let eqs = List.map mkVar eqs in
+    let rewrite =
       tclFIRST (List.map Equality.rewriteRL eqs )
-    in 
-    let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in 
-    let f_app = array_last (snd (destApp hrec_concl)) in 
-    let f =  (fst (destApp f_app)) in 
-    let rec backtrack : tactic = 
-      fun g -> 
-	let f_app = array_last (snd (destApp (pf_concl g))) in 
-	match kind_of_term f_app with 
+    in
+    let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in
+    let f_app = array_last (snd (destApp hrec_concl)) in
+    let f =  (fst (destApp f_app)) in
+    let rec backtrack : tactic =
+      fun g ->
+	let f_app = array_last (snd (destApp (pf_concl g))) in
+	match kind_of_term f_app with
 	  | App(f',_) when eq_constr f' f -> tclIDTAC g
 	  | _ -> tclTHEN rewrite backtrack g
     in
     backtrack gls
 
-    
-    
-let build_clause eqs = 
+
+
+let build_clause eqs =
   {
-    Tacexpr.onhyps = 
-      Some (List.map 
+    Tacexpr.onhyps =
+      Some (List.map
 	      (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
 	      eqs
 	   );
-    Tacexpr.concl_occs = Rawterm.no_occurrences_expr 
+    Tacexpr.concl_occs = Rawterm.no_occurrences_expr
   }
 
-let rec rewrite_eqs_in_eqs eqs = 
-  match eqs with 
+let rec rewrite_eqs_in_eqs eqs =
+  match eqs with
     | [] -> tclIDTAC
-    | eq::eqs -> 
-	
-	  tclTHEN 
-	    (tclMAP 
-	       (fun id gl -> 
-		  observe_tac 
-		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) 
+    | eq::eqs ->
+
+	  tclTHEN
+	    (tclMAP
+	       (fun id gl ->
+		  observe_tac
+		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
 		    (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false))
 		    gl
-	       ) 
+	       )
 	       eqs
 	    )
-	    (rewrite_eqs_in_eqs eqs) 
+	    (rewrite_eqs_in_eqs eqs)
 
-let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = 
+let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
   fun gls ->
-    (tclTHENSEQ 
+    (tclTHENSEQ
        [
 	 backtrack_eqs_until_hrec hrec eqs;
 	 (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
 	    (apply (mkVar hrec))
-	    [ tclTHENSEQ 
+	    [ tclTHENSEQ
 		[
 		  keep (tcc_hyps@eqs);
 		  apply (Lazy.force acc_inv);
-		  (fun g -> 
-		     if is_mes 
-		     then 
-		       unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g 
+		  (fun g ->
+		     if is_mes
+		     then
+		       unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
 		     else tclIDTAC g
 		  );
 		  observe_tac "rew_and_finish"
-		    (tclTHENLIST 
+		    (tclTHENLIST
 		       [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs));
 			observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs);
 			 (observe_tac "finishing using"
@@ -1462,7 +1462,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 	    ])
        ])
       gls
-      
+
 
 let is_valid_hypothesis predicates_name =
   let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
@@ -1477,78 +1477,78 @@ let is_valid_hypothesis predicates_name =
   in
   let rec is_valid_hypothesis typ =
     is_pte typ ||
-      match kind_of_term typ with 
+      match kind_of_term typ with
 	| Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
-	| _ -> false 
+	| _ -> false
   in
-  is_valid_hypothesis 
+  is_valid_hypothesis
 
 let prove_principle_for_gen
     (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
-    rec_arg_num rec_arg_type relation gl = 
-  let princ_type = pf_concl gl in 
-  let princ_info = compute_elim_sig princ_type in 
-  let fresh_id = 
-    let avoid = ref (pf_ids_of_hyps gl) in 
-    fun na -> 
-      let new_id = 
-	  match na with 
-	    | Name id -> fresh_id !avoid (string_of_id id) 
-	    | Anonymous -> fresh_id !avoid "H" 
+    rec_arg_num rec_arg_type relation gl =
+  let princ_type = pf_concl gl in
+  let princ_info = compute_elim_sig princ_type in
+  let fresh_id =
+    let avoid = ref (pf_ids_of_hyps gl) in
+    fun na ->
+      let new_id =
+	  match na with
+	    | Name id -> fresh_id !avoid (string_of_id id)
+	    | Anonymous -> fresh_id !avoid "H"
       in
       avoid := new_id :: !avoid;
       Name new_id
   in
   let fresh_decl (na,b,t) = (fresh_id na,b,t) in
-  let princ_info : elim_scheme = 
-    { princ_info with 
+  let princ_info : elim_scheme =
+    { princ_info with
 	params = List.map fresh_decl princ_info.params;
-	predicates = List.map fresh_decl princ_info.predicates; 
-	branches = List.map fresh_decl princ_info.branches; 
+	predicates = List.map fresh_decl princ_info.predicates;
+	branches = List.map fresh_decl princ_info.branches;
 	args = List.map fresh_decl princ_info.args
     }
   in
-  let wf_tac = 
-    if is_mes 
-    then 
+  let wf_tac =
+    if is_mes
+    then
       (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None)
     else fun _ -> prove_with_tcc tcc_lemma_ref []
   in
-  let real_rec_arg_num = rec_arg_num - princ_info.nparams in 
-  let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in 
+  let real_rec_arg_num = rec_arg_num - princ_info.nparams in
+  let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
 (*   observe ( *)
 (*     str "princ_type := " ++ pr_lconstr  princ_type ++ fnl () ++ *)
 (*     str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++  *)
-      
+
 (*       str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++  *)
 (*     str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++  *)
 (* 	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
 (* 	     str "npost_rec_arg := " ++ int npost_rec_arg ); *)
-  let (post_rec_arg,pre_rec_arg) = 
+  let (post_rec_arg,pre_rec_arg) =
     Util.list_chop npost_rec_arg princ_info.args
   in
-  let rec_arg_id = 
-    match List.rev post_rec_arg with 
-      | (Name id,_,_)::_ -> id 
-      | _ -> assert false 
+  let rec_arg_id =
+    match List.rev post_rec_arg with
+      | (Name id,_,_)::_ -> id
+      | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in 
-  let relation = substl subst_constrs relation in 
-  let input_type = substl subst_constrs rec_arg_type in 
-  let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in 
-  let acc_rec_arg_id = 
+  let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
+  let relation = substl subst_constrs relation in
+  let input_type = substl subst_constrs rec_arg_type in
+  let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in
+  let acc_rec_arg_id =
     Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
-  in 
-  let revert l = 
-    tclTHEN (h_generalize (List.map mkVar l)) (clear l) 
   in
-  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in 
-  let prove_rec_arg_acc g = 
+  let revert l =
+    tclTHEN (h_generalize (List.map mkVar l)) (clear l)
+  in
+  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+  let prove_rec_arg_acc g =
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
 	    (tclTHEN
-	       (assert_by (Name wf_thm_id)  
+	       (assert_by (Name wf_thm_id)
 		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
 		  (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
 	       (
@@ -1562,8 +1562,8 @@ let prove_principle_for_gen
       g
   in
   let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
-  let lemma = 
-    match !tcc_lemma_ref with 
+  let lemma =
+    match !tcc_lemma_ref with
      | None -> anomaly ( "No tcc proof !!")
      | Some lemma -> lemma
   in
@@ -1578,11 +1578,11 @@ let prove_principle_for_gen
 (*                f::(list_diff r check_list) *)
 (*   in *)
   let tcc_list = ref [] in
-  let start_tac gls = 
-    let hyps = pf_ids_of_hyps gls in 
-      let hid = 
-	next_global_ident_away true 
-	  (id_of_string "prov") 
+  let start_tac gls =
+    let hyps = pf_ids_of_hyps gls in
+      let hid =
+	next_global_ident_away true
+	  (id_of_string "prov")
 	  hyps
       in
       tclTHENSEQ
@@ -1590,12 +1590,12 @@ let prove_principle_for_gen
 	  generalize [lemma];
 	  h_intro hid;
 	  Elim.h_decompose_and (mkVar hid);
-	  (fun g -> 
-	     let new_hyps = pf_ids_of_hyps g in 
+	  (fun g ->
+	     let new_hyps = pf_ids_of_hyps g in
 	     tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
 	     if !tcc_list = []
-	     then 
-	       begin 
+	     then
+	       begin
 		 tcc_list := [hid];
 		 tclIDTAC g
 	       end
@@ -1605,10 +1605,10 @@ let prove_principle_for_gen
 	  gls
   in
   tclTHENSEQ
-    [ 	      
+    [
       observe_tac "start_tac" start_tac;
-      h_intros 
-	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
+      h_intros
+	(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) (assert_by
@@ -1619,24 +1619,24 @@ let prove_principle_for_gen
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
 (* 			   str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
-      (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1)); 
+      (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Equality.rewriteLR (mkConst eq_ref);
-      (* observe_tac "finish" *) (fun gl' -> 
-	 let body = 
-	   let _,args = destApp (pf_concl gl') in 
+      (* observe_tac "finish" *) (fun gl' ->
+	 let body =
+	   let _,args = destApp (pf_concl gl') in
 	   array_last args
 	 in
-	 let body_info rec_hyps = 
+	 let body_info rec_hyps =
 	   {
 	     nb_rec_hyps = List.length rec_hyps;
 	     rec_hyps = rec_hyps;
 	     eq_hyps = [];
 	     info = body
 	   }
-	 in 
-	 let acc_inv = 
+	 in
+	 let acc_inv =
 	   lazy (
 	     mkApp (
 	       delayed_force acc_inv_id,
@@ -1645,12 +1645,12 @@ let prove_principle_for_gen
 	   )
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
-	 let predicates_names = 
+	 let predicates_names =
 	   List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
 	 in
-	 let pte_info = 
+	 let pte_info =
 	   { proving_tac =
-	       (fun eqs -> 
+	       (fun eqs ->
 (* 		  msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id  !tcc_list); *)
 (* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
 (* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
@@ -1658,47 +1658,47 @@ let prove_principle_for_gen
 (* 		  msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id  eqs); *)
 
 		  (* observe_tac "new_prove_with_tcc"  *)
-		    (new_prove_with_tcc  
-		       is_mes acc_inv fix_id  
-		         
-		       (!tcc_list@(List.map 
-			   (fun (na,_,_) -> (Nameops.out_name na)) 
+		    (new_prove_with_tcc
+		       is_mes acc_inv fix_id
+
+		       (!tcc_list@(List.map
+			   (fun (na,_,_) -> (Nameops.out_name na))
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
-	       
+
 	       );
 	     is_valid = is_valid_hypothesis predicates_names
 	   }
 	 in
-	 let ptes_info : pte_info Idmap.t = 
+	 let ptes_info : pte_info Idmap.t =
 	   List.fold_left
-	     (fun map pte_id -> 
-		Idmap.add pte_id 
-		  pte_info			       
+	     (fun map pte_id ->
+		Idmap.add pte_id
+		  pte_info
 		  map
 	     )
 	     Idmap.empty
 	     predicates_names
 	 in
-	 let make_proof rec_hyps = 
-	   build_proof 
-	     false 
+	 let make_proof rec_hyps =
+	   build_proof
+	     false
 	     [f_ref]
 	     ptes_info
 	     (body_info rec_hyps)
 	 in
 	 (* observe_tac "instanciate_hyps_with_args"  *)
-	   (instanciate_hyps_with_args 
+	   (instanciate_hyps_with_args
 	      make_proof
 	      (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'
       )
-			   
+
     ]
-    gl    
+    gl