[funind] Untabify; necessary to ease the review of subsequent work.

1 files changed, 595 insertions, 596 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 17d962f30f..2b5c0a01db 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -79,10 +79,10 @@ let def_of_const t =
     Const sp ->
       (try (match constant_opt_value_in (Global.env ()) sp with
              | Some c -> c
-	     | _ -> raise Not_found)
+             | _ -> raise Not_found)
        with Not_found ->
-	 anomaly (str "Cannot find definition of constant " ++
-		    (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".")
+         anomaly (str "Cannot find definition of constant " ++
+                    (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".")
       )
      |_ -> assert false
 
@@ -129,8 +129,8 @@ let lt = function () -> (coq_init_constant "lt")
 let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
 let ex = function () -> (coq_init_constant "ex")
 let nat = function () -> (coq_init_constant "nat")
-let iter_ref () =  
-  try find_reference ["Recdef"] "iter" 
+let iter_ref () =
+  try find_reference ["Recdef"] "iter"
   with Not_found -> user_err Pp.(str "module Recdef not loaded")
 let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
 let eq = function () -> (coq_init_constant "eq")
@@ -169,13 +169,13 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
   fun al fterm ->
     let rev_x_id_l =
       (
-	List.fold_left
-	  (fun x_id_l _ ->
-	     let x_id = next_ident_away_in_goal x_id x_id_l in
-	     x_id::x_id_l
-	  )
-	  []
-	  al
+        List.fold_left
+          (fun x_id_l _ ->
+             let x_id = next_ident_away_in_goal x_id x_id_l in
+             x_id::x_id_l
+          )
+          []
+          al
       )
     in
     let context = List.map
@@ -185,13 +185,13 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
     let glob_body =
       DAst.make @@
        GCases
-	(RegularStyle,None,
-	 [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l),
-	  (Anonymous,None)],
+        (RegularStyle,None,
+         [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l),
+          (Anonymous,None)],
          [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
-			   [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous],
+                           [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous],
                            Anonymous)],
-	    DAst.make @@ GVar v_id)])
+            DAst.make @@ GVar v_id)])
     in
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     let body = EConstr.Unsafe.to_constr body in
@@ -206,17 +206,17 @@ let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t
 (* Debugging mechanism *)
 let debug_queue = Stack.create ()
 
-let print_debug_queue b e = 
-  if  not (Stack.is_empty debug_queue) 
+let print_debug_queue b e =
+  if  not (Stack.is_empty debug_queue)
   then
     begin
-      let lmsg,goal = Stack.pop debug_queue in 
-      if b then 
-	Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
+      let lmsg,goal = Stack.pop debug_queue in
+      if b then
+        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
       else
-	begin
-	  Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
-	end;
+        begin
+          Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
+        end;
       (* print_debug_queue false e; *)
     end
 
@@ -226,14 +226,14 @@ let observe strm =
   else ()
 
 
-let do_observe_tac s tac g = 
+let do_observe_tac s tac g =
   let goal = Printer.pr_goal g in
   let s = s (pf_env g) (project g) in
-  let lmsg = (str "recdef : ") ++ s in 
+  let lmsg = (str "recdef : ") ++ s in
   observe (s++fnl());
   Stack.push (lmsg,goal) debug_queue;
-  try 
-    let v = tac g in 
+  try
+    let v = tac g in
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
@@ -258,7 +258,7 @@ let observe_tclTHENLIST s tacl =
     in
     aux 0 tacl
   else tclTHENLIST tacl
-	   
+
 (* Conclusion tactics *)
 
 (* The boolean value is_mes expresses that the termination is expressed
@@ -275,10 +275,10 @@ let tclUSER tac is_mes l g =
       if is_mes
       then observe_tclTHENLIST (fun _ _ -> str "tclUSER2")
         [
-	  Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
+          Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
             (delayed_force Indfun_common.ltof_ref))]);
          tac
-	 ]
+         ]
       else tac
     ]
     g
@@ -290,19 +290,19 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
 
 
 
-  
+
 
 (* Traveling term.
-   Both definitions of [f_terminate] and [f_equation] use the same generic 
+   Both definitions of [f_terminate] and [f_equation] use the same generic
    traveling mechanism.
 *)
 
-(* [check_not_nested forbidden e] checks that [e] does not contains any variable 
+(* [check_not_nested forbidden e] checks that [e] does not contains any variable
    of [forbidden]
 *)
 let check_not_nested env sigma forbidden e =
-  let rec check_not_nested e =  
-    match EConstr.kind sigma e with 
+  let rec check_not_nested e =
+    match EConstr.kind sigma e with
       | Rel _ -> ()
       | Int _ -> ()
       | Var x ->
@@ -319,18 +319,18 @@ let check_not_nested env sigma forbidden e =
       | Const _ -> ()
       | Ind _ -> ()
       | Construct _ -> ()
-      | Case(_,t,e,a) -> 
-	check_not_nested t;check_not_nested e;Array.iter check_not_nested a
+      | Case(_,t,e,a) ->
+        check_not_nested t;check_not_nested e;Array.iter check_not_nested a
       | Fix _ -> user_err Pp.(str "check_not_nested : Fix")
       | CoFix _ -> user_err Pp.(str "check_not_nested : Fix")
   in
-  try 
-    check_not_nested e 
-  with UserError(_,p) -> 
+  try
+    check_not_nested e
+  with UserError(_,p) ->
     user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
-type 'a infos = 
+type 'a infos =
     { nb_arg : int; (* function number of arguments *)
       concl_tac : tactic; (* final tactic to finish proofs *)
       rec_arg_id : Id.t; (*name of the declared recursive argument *)
@@ -343,8 +343,8 @@ type 'a infos =
       info : 'a;
       is_main_branch : bool; (* on the main branch or on a matched expression *)
       is_final : bool; (* final first order term or not *)
-      values_and_bounds : (Id.t*Id.t) list; 
-      eqs : Id.t list; 
+      values_and_bounds : (Id.t*Id.t) list;
+      eqs : Id.t list;
       forbidden_ids : Id.t list;
       acc_inv : constr lazy_t;
       acc_id : Id.t;
@@ -352,166 +352,166 @@ type 'a infos =
     }
 
 
-type ('a,'b) journey_info_tac = 
+type ('a,'b) journey_info_tac =
     'a -> (* the arguments of the constructor *)
     'b infos -> (* infos of the caller *)
     ('b infos -> tactic) -> (* the continuation tactic of the caller *)
     'b infos -> (* argument of the tactic *)
     tactic
-       
+
 (* journey_info : specifies the actions to do on the different term constructors during the traveling of the term
 *)
-type journey_info = 
+type journey_info =
     { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac;
       lambdA : ((Name.t*types*constr),constr) journey_info_tac;
-      casE : ((constr infos -> tactic) -> constr infos -> tactic) -> 
-	((case_info * constr * constr * constr array),constr) journey_info_tac;
+      casE : ((constr infos -> tactic) -> constr infos -> tactic) ->
+        ((case_info * constr * constr * constr array),constr) journey_info_tac;
       otherS : (unit,constr) journey_info_tac;
       apP : (constr*(constr list),constr) journey_info_tac;
       app_reC : (constr*(constr list),constr) journey_info_tac;
       message : string
     }
 
-	       
 
-let add_vars sigma forbidden e = 
+
+let add_vars sigma forbidden e =
   let rec aux forbidden e =
-  match EConstr.kind sigma e with 
-    | Var x -> x::forbidden 
+  match EConstr.kind sigma e with
+    | Var x -> x::forbidden
     | _ -> EConstr.fold sigma aux forbidden e
   in
   aux forbidden e
 
-let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = 
-  fun g -> 
+let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
+  fun g ->
     let rev_context,b = decompose_lam_n (project g) nb_lam e in
     let ids = List.fold_left (fun acc (na,_) ->
-      let pre_id = 
+      let pre_id =
         match na.binder_name with
-	  | Name x -> x 
-	  | Anonymous -> ano_id 
+          | Name x -> x
+          | Anonymous -> ano_id
       in
       pre_id::acc
-    ) [] rev_context in 
-    let rev_ids = pf_get_new_ids (List.rev ids) g in 
-    let new_b = substl (List.map mkVar rev_ids) b in 
+    ) [] rev_context in
+    let rev_ids = pf_get_new_ids (List.rev ids) g in
+    let new_b = substl (List.map mkVar rev_ids) b in
     observe_tclTHENLIST (fun _ _ -> str "treat_case1")
       [
-	h_intros (List.rev rev_ids);
-	Proofview.V82.of_tactic (intro_using teq_id);
-	onLastHypId (fun heq -> 
+        h_intros (List.rev rev_ids);
+        Proofview.V82.of_tactic (intro_using teq_id);
+        onLastHypId (fun heq ->
           observe_tclTHENLIST (fun _ _ -> str "treat_case2")[
-	    Proofview.V82.of_tactic (clear to_intros);
-	    h_intros to_intros;
-	    (fun g' -> 
-	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
-	      let teq_lhs,teq_rhs =
-		let _,args = try destApp (project g') ty_teq with DestKO -> assert false in
-		args.(1),args.(2)
-	      in
-	      let new_b' = Termops.replace_term (project g') teq_lhs teq_rhs new_b in 
-	      let new_infos = {
-		infos with 
-		  info = new_b';
-		  eqs = heq::infos.eqs;
-		  forbidden_ids = 
-		  if forbid_new_ids 
-		  then add_vars (project g') infos.forbidden_ids new_b'
-		  else infos.forbidden_ids
-	      } in 
-	      finalize_tac new_infos g' 
-	    )
-	  ]
-	)
+            Proofview.V82.of_tactic (clear to_intros);
+            h_intros to_intros;
+            (fun g' ->
+              let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+              let teq_lhs,teq_rhs =
+                let _,args = try destApp (project g') ty_teq with DestKO -> assert false in
+                args.(1),args.(2)
+              in
+              let new_b' = Termops.replace_term (project g') teq_lhs teq_rhs new_b in
+              let new_infos = {
+                infos with
+                  info = new_b';
+                  eqs = heq::infos.eqs;
+                  forbidden_ids =
+                  if forbid_new_ids
+                  then add_vars (project g') infos.forbidden_ids new_b'
+                  else infos.forbidden_ids
+              } in
+              finalize_tac new_infos g'
+            )
+          ]
+        )
       ] g
 
 let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
   let sigma = project g in
   let env = pf_env g in
-  match EConstr.kind sigma expr_info.info with 
+  match EConstr.kind sigma expr_info.info with
     | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
     | Proj _ -> user_err Pp.(str "Function cannot treat projections")
     | LetIn(na,b,t,e) ->
       begin
-	let new_continuation_tac = 
+        let new_continuation_tac =
           jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac
-	in
-	travel jinfo new_continuation_tac 
-	  {expr_info with info = b; is_final=false} g
+        in
+        travel jinfo new_continuation_tac
+          {expr_info with info = b; is_final=false} g
       end
     | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
-    | Prod _ -> 
+    | Prod _ ->
       begin
-	try
+        try
           check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
-	  jinfo.otherS () expr_info continuation_tac expr_info g
-	with e when CErrors.noncritical e ->
+          jinfo.otherS () expr_info continuation_tac expr_info g
+        with e when CErrors.noncritical e ->
           user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Lambda(n,t,b) ->
       begin
-	try
+        try
           check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
-	  jinfo.otherS () expr_info continuation_tac expr_info g
-	with e when CErrors.noncritical e ->
+          jinfo.otherS () expr_info continuation_tac expr_info g
+        with e when CErrors.noncritical e ->
           user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
-    | Case(ci,t,a,l) -> 
+    | Case(ci,t,a,l) ->
       begin
-	let continuation_tac_a = 
-	  jinfo.casE 
-	    (travel jinfo) (ci,t,a,l) 
-	    expr_info continuation_tac in 
-	travel 
-	  jinfo continuation_tac_a 
-	  {expr_info with info = a; is_main_branch = false; 
-	    is_final = false} g
+        let continuation_tac_a =
+          jinfo.casE
+            (travel jinfo) (ci,t,a,l)
+            expr_info continuation_tac in
+        travel
+          jinfo continuation_tac_a
+          {expr_info with info = a; is_main_branch = false;
+            is_final = false} g
       end
-    | App _ -> 
-      let f,args = decompose_app sigma expr_info.info in 
-      if EConstr.eq_constr sigma f (expr_info.f_constr) 
+    | App _ ->
+      let f,args = decompose_app sigma expr_info.info in
+      if EConstr.eq_constr sigma f (expr_info.f_constr)
       then jinfo.app_reC (f,args) expr_info continuation_tac expr_info g
       else
       begin
-	match EConstr.kind sigma f with 
-	  | App _ -> assert false (* f is coming from a decompose_app *)
-	  | Const _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ 
-	  | Sort _ | Prod _ | Var _ -> 
-	    let new_infos = {expr_info with info=(f,args)} in 
-	    let new_continuation_tac = 
-	      jinfo.apP (f,args) expr_info continuation_tac in 
-	    travel_args jinfo
-	      expr_info.is_main_branch new_continuation_tac new_infos g
+        match EConstr.kind sigma f with
+          | App _ -> assert false (* f is coming from a decompose_app *)
+          | Const _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _
+          | Sort _ | Prod _ | Var _ ->
+            let new_infos = {expr_info with info=(f,args)} in
+            let new_continuation_tac =
+              jinfo.apP (f,args) expr_info continuation_tac in
+            travel_args jinfo
+              expr_info.is_main_branch new_continuation_tac new_infos g
           | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
           | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
     | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
-      let new_continuation_tac = 
-	jinfo.otherS () expr_info continuation_tac in
+      let new_continuation_tac =
+        jinfo.otherS () expr_info continuation_tac in
       new_continuation_tac expr_info g
-and travel_args jinfo is_final continuation_tac infos = 
-  let (f_args',args) = infos.info in 
-  match args with 
-    | [] -> 
+and travel_args jinfo is_final continuation_tac infos =
+  let (f_args',args) = infos.info in
+  match args with
+    | [] ->
       continuation_tac {infos with info = f_args'; is_final = is_final}
-    | arg::args' -> 
-      let new_continuation_tac new_infos = 
-	let new_arg = new_infos.info in 
-	travel_args jinfo is_final
-	  continuation_tac
-	  {new_infos with info = (mkApp(f_args',[|new_arg|]),args')}
+    | arg::args' ->
+      let new_continuation_tac new_infos =
+        let new_arg = new_infos.info in
+        travel_args jinfo is_final
+          continuation_tac
+          {new_infos with info = (mkApp(f_args',[|new_arg|]),args')}
       in
-      travel jinfo new_continuation_tac 
-	{infos with info=arg;is_final=false} 
+      travel jinfo new_continuation_tac
+        {infos with info=arg;is_final=false}
 and travel jinfo continuation_tac expr_info =
   observe_tac
     (fun env sigma -> str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info)
     (travel_aux jinfo continuation_tac expr_info)
 
-(* Termination proof *) 
+(* Termination proof *)
 
-let rec prove_lt hyple g = 
+let rec prove_lt hyple g =
   let sigma = project g in
   begin
     try
@@ -520,125 +520,125 @@ let rec prove_lt hyple g =
         | _ -> assert false
       in
       let h =
-	List.find (fun id ->
+        List.find (fun id ->
           match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with
             | _, t::_ -> EConstr.eq_constr sigma t varx
             | _ -> false
-	) hyple
+        ) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in
+        List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in
       observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[
-	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
+        Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
         observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple)
       ]
-    with Not_found -> 
+    with Not_found ->
       (
-	(
+        (
           observe_tclTHENLIST (fun _ _ -> str "prove_lt2")[
-	    Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
+            Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
             (observe_tac (fun _ _ -> str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
-	  ])
+          ])
       )
   end
     g
 
-let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = 
-  match lbounds with 
-    | [] -> 
-      let ids = pf_ids_of_hyps g in 
-      let s_max = mkApp(delayed_force coq_S, [|bound|]) in 
+let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
+  match lbounds with
+    | [] ->
+      let ids = pf_ids_of_hyps g in
+      let s_max = mkApp(delayed_force coq_S, [|bound|]) in
       let k = next_ident_away_in_goal k_id ids in
       let ids = k::ids in
       let h' = next_ident_away_in_goal (h'_id) ids in
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
       observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux1")[
-	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
-	Proofview.V82.of_tactic (intro_then
-	  (fun id -> 
+        Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
+        Proofview.V82.of_tactic (intro_then
+          (fun id ->
             Proofview.V82.tactic begin
             observe_tac (fun _ _ -> str "destruct_bounds_aux")
-	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
-		 [
+              (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
+                 [
                    observe_tclTHENLIST (fun _ _ -> str "")[Proofview.V82.of_tactic (intro_using h_id);
-			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
-			       Proofview.V82.of_tactic default_full_auto];
+                               Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
+                               Proofview.V82.of_tactic default_full_auto];
                    observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux2")[
                      observe_tac (fun _ _ -> str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
-		     h_intros [k;h';def];
+                     h_intros [k;h';def];
                      observe_tac (fun _ _ -> str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
                      observe_tac (fun _ _ -> str "unfold functional")
-		       (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
-					 evaluable_of_global_reference infos.func)]));
-		     (
+                       (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+                                         evaluable_of_global_reference infos.func)]));
+                     (
                        observe_tclTHENLIST (fun _ _ -> str "test")[
-			 list_rewrite true
-			   (List.fold_right 
-			      (fun e acc -> (mkVar e,true)::acc)
-			      infos.eqs
-			      (List.map (fun e -> (e,true)) rechyps)
-			   );
-		      (* list_rewrite true *)
-		      (*   (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
-		      (*   ; *)
-			 
+                         list_rewrite true
+                           (List.fold_right
+                              (fun e acc -> (mkVar e,true)::acc)
+                              infos.eqs
+                              (List.map (fun e -> (e,true)) rechyps)
+                           );
+                      (* list_rewrite true *)
+                      (*   (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
+                      (*   ; *)
+
                          (observe_tac (fun _ _ -> str "finishing")
-			    (tclORELSE
-			       (Proofview.V82.of_tactic intros_reflexivity)
+                            (tclORELSE
+                               (Proofview.V82.of_tactic intros_reflexivity)
                                (observe_tac (fun _ _ -> str "calling prove_lt") (prove_lt hyple))))])
-		   ]
-	      ]
-	      )end))
-	  ] g
-      | (_,v_bound)::l -> 
+                   ]
+              ]
+              )end))
+          ] g
+      | (_,v_bound)::l ->
       observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux3")[
-	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
-	Proofview.V82.of_tactic (clear [v_bound]);
-	tclDO 2 (Proofview.V82.of_tactic intro);
-	onNthHypId 1 
-	  (fun p_hyp -> 
-	    (onNthHypId 2 
-	       (fun p ->  
+        Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
+        Proofview.V82.of_tactic (clear [v_bound]);
+        tclDO 2 (Proofview.V82.of_tactic intro);
+        onNthHypId 1
+          (fun p_hyp ->
+            (onNthHypId 2
+               (fun p ->
                  observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux4")[
-		   Proofview.V82.of_tactic (simplest_elim 
-		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
-		   tclDO 3 (Proofview.V82.of_tactic intro);
-		   onNLastHypsId 3 (fun lids -> 
-		     match lids with
-		       [hle2;hle1;pmax] -> 
-			 destruct_bounds_aux infos 
-			   ((mkVar pmax),
-			    hle1::hle2::hyple,(mkVar p_hyp)::rechyps) 
-			   l 
-		       | _ -> assert false) ;
-		 ]
-	       )
-	    )
-	  )
+                   Proofview.V82.of_tactic (simplest_elim
+                     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
+                   tclDO 3 (Proofview.V82.of_tactic intro);
+                   onNLastHypsId 3 (fun lids ->
+                     match lids with
+                       [hle2;hle1;pmax] ->
+                         destruct_bounds_aux infos
+                           ((mkVar pmax),
+                            hle1::hle2::hyple,(mkVar p_hyp)::rechyps)
+                           l
+                       | _ -> assert false) ;
+                 ]
+               )
+            )
+          )
       ] g
 
-let destruct_bounds infos = 
+let destruct_bounds infos =
   destruct_bounds_aux infos (delayed_force coq_O,[],[]) infos.values_and_bounds
 
-let terminate_app f_and_args expr_info continuation_tac infos = 
-    if expr_info.is_final && expr_info.is_main_branch 
-    then 
+let terminate_app f_and_args expr_info continuation_tac infos =
+    if expr_info.is_final && expr_info.is_main_branch
+    then
       observe_tclTHENLIST (fun _ _ -> str "terminate_app1")[
-	continuation_tac infos;
+        continuation_tac infos;
         observe_tac (fun _ _ -> str "first split")
-	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
+          (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
         observe_tac (fun _ _ -> str "destruct_bounds (1)") (destruct_bounds infos)
       ]
     else continuation_tac infos
 
-let terminate_others _ expr_info continuation_tac infos = 
-  if expr_info.is_final && expr_info.is_main_branch 
-  then 
+let terminate_others _ expr_info continuation_tac infos =
+  if expr_info.is_final && expr_info.is_main_branch
+  then
     observe_tclTHENLIST (fun _ _ -> str "terminate_others")[
-	    continuation_tac infos;
+            continuation_tac infos;
       observe_tac (fun _ _ -> str "first split")
-	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
+        (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
       observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos)
     ]
   else continuation_tac infos
@@ -646,24 +646,24 @@ let terminate_others _ expr_info continuation_tac infos =
 let terminate_letin (na,b,t,e) expr_info continuation_tac info g =
   let sigma = project g in
   let env = pf_env g in
-  let new_e = subst1 info.info e in 
-  let new_forbidden = 
-    let forbid = 
-      try 
+  let new_e = subst1 info.info e in
+  let new_forbidden =
+    let forbid =
+      try
         check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) b;
-	true
+        true
       with e when CErrors.noncritical e -> false
     in
-    if forbid 
-    then 
+    if forbid
+    then
       match na with
-	| Anonymous -> info.forbidden_ids
-	| Name id -> id::info.forbidden_ids
-    else info.forbidden_ids 
+        | Anonymous -> info.forbidden_ids
+        | Name id -> id::info.forbidden_ids
+    else info.forbidden_ids
   in
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
 
-let pf_type c tac gl = 
+let pf_type c tac gl =
   let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
     tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
@@ -704,7 +704,6 @@ let mkDestructEq :
         Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
-
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let sigma = project g in
   let env = pf_env g in
@@ -721,104 +720,104 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
       info = mkCase(ci,t,a',l);
       is_main_branch = expr_info.is_main_branch;
       is_final = expr_info.is_final} in
-  let destruct_tac,rev_to_thin_intro = 
-    mkDestructEq [expr_info.rec_arg_id] a' g in 
-  let to_thin_intro = List.rev rev_to_thin_intro in 
+  let destruct_tac,rev_to_thin_intro =
+    mkDestructEq [expr_info.rec_arg_id] a' g in
+  let to_thin_intro = List.rev rev_to_thin_intro in
   observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
     (try
       (tclTHENS
-	 destruct_tac
+         destruct_tac
          (List.map_i (fun i e -> observe_tac (fun _ _ -> str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
-	 ))
-    with 
-      | UserError(Some "Refiner.thensn_tac3",_) 
+         ))
+    with
+      | UserError(Some "Refiner.thensn_tac3",_)
       | UserError(Some "Refiner.tclFAIL_s",_) ->
         (observe_tac (fun _ _ -> str "is computable " ++ Printer.pr_leconstr_env env sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} )
-	))
+        ))
     g
-    
+
 let terminate_app_rec (f,args) expr_info continuation_tac _ g =
   let sigma = project g in
   let env = pf_env g in
   List.iter (check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids))
     args;
   begin
-    try 
+    try
       let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in
-      let new_infos = {expr_info with info = v} in 
+      let new_infos = {expr_info with info = v} in
       observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec")[
-	continuation_tac new_infos;
-	if expr_info.is_final && expr_info.is_main_branch 
-	then
+        continuation_tac new_infos;
+        if expr_info.is_final && expr_info.is_main_branch
+        then
           observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec1")[
             observe_tac (fun _ _ -> str "first split")
-	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
+              (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
             observe_tac (fun _ _ -> str "destruct_bounds (3)")
-	      (destruct_bounds new_infos)
-	  ]
-	else
-	  tclIDTAC			       
+              (destruct_bounds new_infos)
+          ]
+        else
+          tclIDTAC
       ] g
-    with Not_found -> 
+    with Not_found ->
       observe_tac (fun _ _ -> str "terminate_app_rec not found") (tclTHENS
-	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
-	[		
+        (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
+        [
           observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2")[
-	    Proofview.V82.of_tactic (intro_using rec_res_id);
-	    Proofview.V82.of_tactic intro;
-	    onNthHypId 1 
-	      (fun v_bound -> 
-		(onNthHypId 2 
-		   (fun v ->  
-		     let new_infos = { expr_info with 
-		       info = (mkVar v); 
-		       values_and_bounds = 
-			 (v,v_bound)::expr_info.values_and_bounds; 
-		       args_assoc=(args,mkVar v)::expr_info.args_assoc
-		     } in
+            Proofview.V82.of_tactic (intro_using rec_res_id);
+            Proofview.V82.of_tactic intro;
+            onNthHypId 1
+              (fun v_bound ->
+                (onNthHypId 2
+                   (fun v ->
+                     let new_infos = { expr_info with
+                       info = (mkVar v);
+                       values_and_bounds =
+                         (v,v_bound)::expr_info.values_and_bounds;
+                       args_assoc=(args,mkVar v)::expr_info.args_assoc
+                     } in
                      observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec3")[
-		       continuation_tac new_infos;
-		       if expr_info.is_final && expr_info.is_main_branch 
-		       then
+                       continuation_tac new_infos;
+                       if expr_info.is_final && expr_info.is_main_branch
+                       then
                          observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec4")[
                            observe_tac (fun _ _ -> str "first split")
-			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
+                             (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
                            observe_tac (fun _ _ -> str "destruct_bounds (2)")
-			     (destruct_bounds new_infos)
-			 ]
-		       else
-			 tclIDTAC			       
-		     ]    
-		   )
-		)
-	      )
-	  ];
+                             (destruct_bounds new_infos)
+                         ]
+                       else
+                         tclIDTAC
+                     ]
+                   )
+                )
+              )
+          ];
           observe_tac (fun _ _ -> str "proving decreasing") (
-	    tclTHENS (* proof of args < formal args *)
-	      (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
-	      [ 
+            tclTHENS (* proof of args < formal args *)
+              (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
+              [
                 observe_tac (fun _ _ -> str "assumption") (Proofview.V82.of_tactic assumption);
                 observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec5")
-		  [
-		    tclTRY(list_rewrite true 
-			     (List.map 
-				(fun e -> mkVar e,true) 
-				expr_info.eqs
-			     )
-		    );
-		    tclUSER expr_info.concl_tac true 
-		      (Some (
-		      expr_info.ih::expr_info.acc_id::
-			(fun (x,y) -> y) 
-			(List.split expr_info.values_and_bounds)
-		       )
-		      );
-		  ]
-	      ])
-	]) g
+                  [
+                    tclTRY(list_rewrite true
+                             (List.map
+                                (fun e -> mkVar e,true)
+                                expr_info.eqs
+                             )
+                    );
+                    tclUSER expr_info.concl_tac true
+                      (Some (
+                      expr_info.ih::expr_info.acc_id::
+                        (fun (x,y) -> y)
+                        (List.split expr_info.values_and_bounds)
+                       )
+                      );
+                  ]
+              ])
+        ]) g
   end
 
-let terminate_info = 
+let terminate_info =
   { message = "prove_terminate with term ";
     letiN = terminate_letin;
     lambdA = (fun _ _ _ _ -> assert false);
@@ -833,15 +832,15 @@ let prove_terminate = travel terminate_info
 
 (* Equation proof *)
 
-let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = 
+let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos =
   observe_tac (fun _ _ -> str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos)
 
-let rec prove_le g = 
+let rec prove_le g =
   let sigma = project g in
-  let x,z = 
-    let _,args = decompose_app sigma (pf_concl g) in 
+  let x,z =
+    let _,args = decompose_app sigma (pf_concl g) in
     (List.hd args,List.hd (List.tl args))
-  in 
+  in
   tclFIRST[
     Proofview.V82.of_tactic assumption;
     Proofview.V82.of_tactic (apply (delayed_force le_n));
@@ -856,151 +855,151 @@ let rec prove_le g =
         in
         let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in
         let h = h.binder_name in
-	let y = 
-	  let _,args = decompose_app sigma t in 
-	  List.hd (List.tl args)
-	in 
+        let y =
+          let _,args = decompose_app sigma t in
+          List.hd (List.tl args)
+        in
         observe_tclTHENLIST (fun _ _ -> str "prove_le")[
-	  Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
+          Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
           observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le)
-	] 
+        ]
       with Not_found -> tclFAIL 0 (mt())
     end;
   ]
     g
 
-let rec make_rewrite_list expr_info max = function 
+let rec make_rewrite_list expr_info max = function
   | [] -> tclIDTAC
-  | (_,p,hp)::l -> 
+  | (_,p,hp)::l ->
     observe_tac (fun _ _ -> str "make_rewrite_list") (tclTHENS
       (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) (
-	(fun g -> 
+        (fun g ->
           let sigma = project g in
-	  let t_eq = compute_renamed_type g (mkVar hp) in
-	  let k,def =
+          let t_eq = compute_renamed_type g (mkVar hp) in
+          let k,def =
             let k_na,_,t = destProd sigma t_eq in
             let _,_,t  = destProd sigma t in
             let def_na,_,_ = destProd sigma t in
             Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
-	  in
-	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
-	    true (* dep proofs also: *) true 
-	    (mkVar hp,
+          in
+          Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
+            true (* dep proofs also: *) true
+            (mkVar hp,
              ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
                               CAst.make @@ (NamedHyp k, f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        observe_tclTHENLIST (fun _ _ -> str "make_rewrite_list")[ (* x < S max proof *)
-	 Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
+         Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
          observe_tac (fun _ _ -> str "prove_le(2)") prove_le
        ]
       ] )
 
-let make_rewrite expr_info l hp max = 
+let make_rewrite expr_info l hp max =
   tclTHENFIRST
     (observe_tac (fun _ _ -> str "make_rewrite") (make_rewrite_list expr_info max l))
     (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS
-       (fun g -> 
+       (fun g ->
           let sigma = project g in
-	  let t_eq = compute_renamed_type g (mkVar hp) in
-	  let k,def =
+          let t_eq = compute_renamed_type g (mkVar hp) in
+          let k,def =
             let k_na,_,t = destProd sigma t_eq in
             let _,_,t  = destProd sigma t in
             let def_na,_,_ = destProd sigma t in
             Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
-	  in
+          in
          observe_tac (fun _ _ -> str "general_rewrite_bindings")
-	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
-	    true (* dep proofs also: *) true 
-	    (mkVar hp,
+           (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
+            true (* dep proofs also: *) true
+            (mkVar hp,
              ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
                               CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g)
        [observe_tac(fun _ _ -> str "make_rewrite finalize") (
-	 (* tclORELSE( h_reflexivity) *)
+         (* tclORELSE( h_reflexivity) *)
          (observe_tclTHENLIST (fun _ _ -> str "make_rewrite")[
-	   Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
+           Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
            observe_tac (fun _ _ -> str "unfold functional")
-	     (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
-			       evaluable_of_global_reference expr_info.func)]));
-	   
-	   (list_rewrite true 
-	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
+             (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+                               evaluable_of_global_reference expr_info.func)]));
+
+           (list_rewrite true
+              (List.map (fun e -> mkVar e,true) expr_info.eqs));
            (observe_tac (fun _ _ -> str "h_reflexivity")
-			(Proofview.V82.of_tactic intros_reflexivity)
-	   )
-	    ]))
+                        (Proofview.V82.of_tactic intros_reflexivity)
+           )
+            ]))
        ;
          observe_tclTHENLIST (fun _ _ -> str "make_rewrite1")[ (* x < S (S max) proof *)
-	 Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS)));
+         Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS)));
          observe_tac (fun _ _ -> str "prove_le (3)") prove_le
-	 ]
-       ])  
+         ]
+       ])
     )
 
-let rec compute_max rew_tac max l = 
-  match l with 
+let rec compute_max rew_tac max l =
+  match l with
     | [] -> rew_tac max
-    | (_,p,_)::l -> 
+    | (_,p,_)::l ->
       observe_tclTHENLIST (fun _ _ -> str "compute_max")[
-	Proofview.V82.of_tactic (simplest_elim 
-	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
-	tclDO 3 (Proofview.V82.of_tactic intro);
-	onNLastHypsId 3 (fun lids -> 
-	  match lids with
-	    | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l 
-	    | _ -> assert false
-	)]
-
-let rec destruct_hex expr_info acc l = 
-  match l with 
-    | [] -> 
+        Proofview.V82.of_tactic (simplest_elim
+          (mkApp(delayed_force max_constr, [| max; mkVar p|])));
+        tclDO 3 (Proofview.V82.of_tactic intro);
+        onNLastHypsId 3 (fun lids ->
+          match lids with
+            | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l
+            | _ -> assert false
+        )]
+
+let rec destruct_hex expr_info acc l =
+  match l with
+    | [] ->
       begin
-	match List.rev acc with 
-	  | [] -> tclIDTAC 
-	  | (_,p,hp)::tl  -> 
+        match List.rev acc with
+          | [] -> tclIDTAC
+          | (_,p,hp)::tl  ->
             observe_tac (fun _ _ -> str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl)
       end
-    | (v,hex)::l -> 
+    | (v,hex)::l ->
       observe_tclTHENLIST (fun _ _ -> str "destruct_hex")[
-	Proofview.V82.of_tactic (simplest_case (mkVar hex));
-	Proofview.V82.of_tactic (clear [hex]);
-	tclDO 2 (Proofview.V82.of_tactic intro);
-	onNthHypId 1 (fun hp -> 
-	  onNthHypId 2 (fun p -> 
-	    observe_tac 
+        Proofview.V82.of_tactic (simplest_case (mkVar hex));
+        Proofview.V82.of_tactic (clear [hex]);
+        tclDO 2 (Proofview.V82.of_tactic intro);
+        onNthHypId 1 (fun hp ->
+          onNthHypId 2 (fun p ->
+            observe_tac
               (fun _ _ -> str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p)
-	      (destruct_hex expr_info ((v,p,hp)::acc) l)
-	  )
-	)
+              (destruct_hex expr_info ((v,p,hp)::acc) l)
+          )
+        )
       ]
-	
-let rec intros_values_eq expr_info acc = 
+
+let rec intros_values_eq expr_info acc =
   tclORELSE(
     observe_tclTHENLIST (fun _ _ -> str "intros_values_eq")[
       tclDO 2 (Proofview.V82.of_tactic intro);
-      onNthHypId 1 (fun hex -> 
-	(onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
+      onNthHypId 1 (fun hex ->
+        (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
       )
     ])
     (tclCOMPLETE (
       destruct_hex expr_info [] acc
     ))
 
-let equation_others _ expr_info continuation_tac infos = 
-  if expr_info.is_final && expr_info.is_main_branch 
+let equation_others _ expr_info continuation_tac infos =
+  if expr_info.is_final && expr_info.is_main_branch
   then
     observe_tac (fun env sigma -> str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info)
-		(tclTHEN 
-      (continuation_tac infos) 
+                (tclTHEN
+      (continuation_tac infos)
       (observe_tac (fun env sigma -> str "intros_values_eq equation_others "  ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info [])))
   else observe_tac (fun env sigma -> str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos)
 
-let equation_app f_and_args expr_info continuation_tac infos = 
-    if expr_info.is_final && expr_info.is_main_branch 
+let equation_app f_and_args expr_info continuation_tac infos =
+    if expr_info.is_final && expr_info.is_main_branch
     then ((observe_tac (fun _ _ -> str "intros_values_eq equation_app") (intros_values_eq expr_info [])))
     else continuation_tac infos
-	    
-let equation_app_rec (f,args) expr_info continuation_tac info g = 
+
+let equation_app_rec (f,args) expr_info continuation_tac info g =
   let sigma = project g in
   begin
     try
@@ -1008,21 +1007,21 @@ let equation_app_rec (f,args) expr_info continuation_tac info g =
       let new_infos = {expr_info with info = v} in
       observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g
     with Not_found ->
-      if expr_info.is_final && expr_info.is_main_branch 
-      then 
+      if expr_info.is_final && expr_info.is_main_branch
+      then
         observe_tclTHENLIST (fun _ _ -> str "equation_app_rec")
-	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
-	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
+          [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
+            continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
             observe_tac (fun _ _ -> str "app_rec intros_values_eq") (intros_values_eq expr_info [])
-	  ] g
-      else 
+          ] g
+      else
         observe_tclTHENLIST (fun _ _ -> str "equation_app_rec1")[
-  	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
+          Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
           observe_tac (fun _ _ -> str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
-	] g
+        ] g
   end
 
-let equation_info = 
+let equation_info =
   {message = "prove_equation with term ";
    letiN = (fun _ -> assert false);
    lambdA = (fun _ _ _ _ -> assert false);
@@ -1031,7 +1030,7 @@ let equation_info =
    apP = equation_app;
    app_reC = equation_app_rec
 }
-    
+
 let prove_eq = travel equation_info
 
 (* wrappers *)
@@ -1045,12 +1044,12 @@ let compute_terminate_type nb_args func =
   let rev_args,b = decompose_prod_n nb_args a_arrow_b in
   let left =
     mkApp(delayed_force iter_rd,
-	  Array.of_list
-	    (lift 5 a_arrow_b:: mkRel 3::
+          Array.of_list
+            (lift 5 a_arrow_b:: mkRel 3::
                constr_of_monomorphic_global func::mkRel 1::
-	       List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
-	    )
-	 )
+               List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
+            )
+         )
   in
   let right = mkRel 5 in
   let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in
@@ -1059,14 +1058,14 @@ let compute_terminate_type nb_args func =
   let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in
   let nb_iter =
     mkApp(delayed_force ex,
-	  [|delayed_force nat;
-	    (mkLambda
+          [|delayed_force nat;
+            (mkLambda
                (make_annot (Name p_id) Sorts.Relevant,
-		  delayed_force nat,
+                  delayed_force nat,
                   (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat,
                            mkArrow cond Sorts.Relevant result))))|])in
   let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref),
-		    [|b;
+                    [|b;
                       (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in
   compose_prod rev_args value
 
@@ -1077,74 +1076,74 @@ let termination_proof_header is_mes input_type ids args_id relation
     fun g ->
       let nargs = List.length args_id in
       let pre_rec_args =
-	List.rev_map
-	  mkVar (fst (List.chop (rec_arg_num - 1) args_id))
+        List.rev_map
+          mkVar (fst (List.chop (rec_arg_num - 1) args_id))
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
       let wf_thm = next_ident_away_in_goal (Id.of_string ("wf_R")) ids in
       let wf_rec_arg =
-	next_ident_away_in_goal
-	  (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))
-	  (wf_thm::ids)
+        next_ident_away_in_goal
+          (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))
+          (wf_thm::ids)
       in
       let hrec = next_ident_away_in_goal hrec_id
-	(wf_rec_arg::wf_thm::ids) in
+        (wf_rec_arg::wf_thm::ids) in
       let acc_inv =
-	  lazy (
-	    mkApp (
-	      delayed_force acc_inv_id,
-	      [|input_type;relation;mkVar rec_arg_id|]
-	    )
-	  )
+          lazy (
+            mkApp (
+              delayed_force acc_inv_id,
+              [|input_type;relation;mkVar rec_arg_id|]
+            )
+          )
       in
       tclTHEN
-	(h_intros args_id)
-	(tclTHENS
-	   (observe_tac
+        (h_intros args_id)
+        (tclTHENS
+           (observe_tac
               (fun _ _ -> str "first assert")
-	      (Proofview.V82.of_tactic (assert_before
-		 (Name wf_rec_arg)
-		 (mkApp (delayed_force acc_rel,
-			 [|input_type;relation;mkVar rec_arg_id|])
-		 )
-	      ))
-	   )
-	   [
-	     (* accesibility proof *)
-	     tclTHENS
-	       (observe_tac
+              (Proofview.V82.of_tactic (assert_before
+                 (Name wf_rec_arg)
+                 (mkApp (delayed_force acc_rel,
+                         [|input_type;relation;mkVar rec_arg_id|])
+                 )
+              ))
+           )
+           [
+             (* accesibility proof *)
+             tclTHENS
+               (observe_tac
                   (fun _ _ -> str "second assert")
-		  (Proofview.V82.of_tactic (assert_before
-		     (Name wf_thm)
-		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
-		  ))
-	       )
-	       [
-		 (* interactive proof that the relation is well_founded *)
+                  (Proofview.V82.of_tactic (assert_before
+                     (Name wf_thm)
+                     (mkApp (delayed_force well_founded,[|input_type;relation|]))
+                  ))
+               )
+               [
+                 (* interactive proof that the relation is well_founded *)
                  observe_tac (fun _ _ -> str "wf_tac") (wf_tac is_mes (Some args_id));
-		 (* this gives the accessibility argument *)
-		 observe_tac
+                 (* this gives the accessibility argument *)
+                 observe_tac
                    (fun _ _ -> str "apply wf_thm")
-		   (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
-		   )
-	       ]
-	     ;
-	     (* rest of the proof *)
+                   (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
+                   )
+               ]
+             ;
+             (* rest of the proof *)
              observe_tclTHENLIST (fun _ _ -> str "rest of proof")
                [observe_tac (fun _ _ -> str "generalize")
-		  (onNLastHypsId (nargs+1)
-		     (tclMAP (fun id ->
-			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
-		     ))
-	       ;
+                  (onNLastHypsId (nargs+1)
+                     (tclMAP (fun id ->
+                        tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
+                     ))
+               ;
                 observe_tac (fun _ _ -> str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1)));
-		h_intros args_id;
-		Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
+                h_intros args_id;
+                Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
                 observe_tac (fun _ _ -> str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
-	       ]
-	   ]
-	) g
+               ]
+           ]
+        ) g
   end
 
 
@@ -1166,58 +1165,58 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let (f_name, _, body1) = destLambda sigma func_body in
       let f_id =
         match f_name.binder_name with
-	  | Name f_id -> next_ident_away_in_goal f_id ids
-	  | Anonymous -> anomaly (Pp.str "Anonymous function.")
+          | Name f_id -> next_ident_away_in_goal f_id ids
+          | Anonymous -> anomaly (Pp.str "Anonymous function.")
       in
       let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
       let n_ids,ids =
-	List.fold_left
+        List.fold_left
           (fun (n_ids,ids) (n_name,_) ->
              match n_name.binder_name with
-	       | Name id ->
-		   let n_id = next_ident_away_in_goal id ids in
-		   n_id::n_ids,n_id::ids
-	       | _ -> anomaly (Pp.str "anonymous argument.")
-	  )
-	  ([],(f_id::ids))
-	  n_names_types
+               | Name id ->
+                   let n_id = next_ident_away_in_goal id ids in
+                   n_id::n_ids,n_id::ids
+               | _ -> anomaly (Pp.str "anonymous argument.")
+          )
+          ([],(f_id::ids))
+          n_names_types
       in
       let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
       let expr = instantiate_lambda sigma func_body (mkVar f_id::(List.map mkVar n_ids)) in
       termination_proof_header
-	is_mes
-	input_type
-	ids
-	n_ids
-	relation
-	rec_arg_num
-	rec_arg_id
-	(fun rec_arg_id hrec acc_id acc_inv g -> 	      
-	  (prove_terminate (fun infos -> tclIDTAC) 
-	     { is_main_branch = true; (* we are on the main branche (i.e. still on a match ... with .... end *)
-	       is_final = true;      (* and on leaf (more or less) *)
-	       f_terminate = delayed_force coq_O;
-	       nb_arg = nb_args;
-	       concl_tac = concl_tac;
-	       rec_arg_id = rec_arg_id;
-	       is_mes = is_mes;
-	       ih = hrec;
-	       f_id = f_id;
-	       f_constr = mkVar f_id;
-	       func = func;
-	       info = expr;
-	       acc_inv = acc_inv;
-	       acc_id = acc_id;
-	       values_and_bounds = [];
-	       eqs = [];
-	       forbidden_ids = [];
-	       args_assoc = []
-	     }
-	  ) 
-	     g
-	)
-	(tclUSER_if_not_mes concl_tac)
-	g
+        is_mes
+        input_type
+        ids
+        n_ids
+        relation
+        rec_arg_num
+        rec_arg_id
+        (fun rec_arg_id hrec acc_id acc_inv g ->
+          (prove_terminate (fun infos -> tclIDTAC)
+             { is_main_branch = true; (* we are on the main branche (i.e. still on a match ... with .... end *)
+               is_final = true;      (* and on leaf (more or less) *)
+               f_terminate = delayed_force coq_O;
+               nb_arg = nb_args;
+               concl_tac = concl_tac;
+               rec_arg_id = rec_arg_id;
+               is_mes = is_mes;
+               ih = hrec;
+               f_id = f_id;
+               f_constr = mkVar f_id;
+               func = func;
+               info = expr;
+               acc_inv = acc_inv;
+               acc_id = acc_id;
+               values_and_bounds = [];
+               eqs = [];
+               forbidden_ids = [];
+               args_assoc = []
+             }
+          )
+             g
+        )
+        (tclUSER_if_not_mes concl_tac)
+        g
   end
 
 let get_current_subgoals_types pstate =
@@ -1231,32 +1230,32 @@ let build_and_l sigma l =
   let conj_constr = Coqlib.build_coq_conj () in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
-  let rec is_well_founded t = 
-    match EConstr.kind sigma t with 
+  let rec is_well_founded t =
+    match EConstr.kind sigma t with
       | Prod(_,_,t') -> is_well_founded t'
-      | App(_,_) -> 
-	let (f,_) = decompose_app sigma t in 
-	EConstr.eq_constr sigma f (well_founded ())
-      | _ -> 
-	false
+      | App(_,_) ->
+        let (f,_) = decompose_app sigma t in
+        EConstr.eq_constr sigma f (well_founded ())
+      | _ ->
+        false
   in
-  let compare t1 t2 = 
-    let b1,b2= is_well_founded t1,is_well_founded t2 in 
+  let compare t1 t2 =
+    let b1,b2= is_well_founded t1,is_well_founded t2 in
     if (b1&&b2) || not (b1 || b2) then 0
     else if b1 && not b2 then 1 else -1
   in
-  let l = List.sort compare l in 
+  let l = List.sort compare l in
   let rec f  = function
     | [] -> raise EmptySubgoals
     | [p] -> p,tclIDTAC,1
     | p1::pl ->
-	let c,tac,nb = f pl in
-	mk_and p1 c,
-	tclTHENS
+        let c,tac,nb = f pl in
+        mk_and p1 c,
+        tclTHENS
           (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr))))
-	  [tclIDTAC;
-	   tac
-	  ],nb+1
+          [tclIDTAC;
+           tac
+          ],nb+1
   in f l
 
 
@@ -1266,15 +1265,15 @@ let is_rec_res id =
   try
     String.equal (String.sub id_name 0 (String.length rec_res_name)) rec_res_name
   with Invalid_argument _ -> false
- 
+
 let clear_goals sigma =
   let rec clear_goal t =
     match EConstr.kind sigma t with
       | Prod({binder_name=Name id} as na,t',b) ->
-	  let b' = clear_goal b in
-	  if noccurn sigma 1 b' && (is_rec_res id)
-	  then Vars.lift (-1) b'
-	  else if b' == b then t
+          let b' = clear_goal b in
+          if noccurn sigma 1 b' && (is_rec_res id)
+          then Vars.lift (-1) b'
+          else if b' == b then t
           else mkProd(na,t',b')
       | _ -> EConstr.map sigma clear_goal t
   in
@@ -1303,8 +1302,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let name = match goal_name with
     | Some s -> s
     | None   ->
-	try add_suffix current_proof_name "_subproof"
-	with e when CErrors.noncritical e ->
+        try add_suffix current_proof_name "_subproof"
+        with e when CErrors.noncritical e ->
           anomaly (Pp.str "open_new_goal with an unnamed theorem.")
   in
   let na = next_global_ident_away name Id.Set.empty in
@@ -1315,8 +1314,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
       let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
-	  ConstRef c -> is_opaque_constant c
-	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
+          ConstRef c -> is_opaque_constant c
+        | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
     ref_ := Value (EConstr.Unsafe.to_constr lemma);
@@ -1325,47 +1324,47 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     let env = Global.env () in
     let lemma = build_proof env (Evd.from_env env)
       (  fun gls ->
-	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
+           let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
            observe_tclTHENLIST (fun _ _ -> str "")
-	     [
-	       Proofview.V82.of_tactic (generalize [lemma]);
-	       Proofview.V82.of_tactic (Simple.intro hid);
-	       (fun g ->
-		  let ids = pf_ids_of_hyps g in
-		  tclTHEN
-		    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
-		    (fun g ->
-		       let ids' = pf_ids_of_hyps g in
-		       lid := List.rev (List.subtract Id.equal ids' ids);
-		       if List.is_empty !lid then lid := [hid];
-		       tclIDTAC g
-		    )
-		    g
-	       );
-	     ] gls)
+             [
+               Proofview.V82.of_tactic (generalize [lemma]);
+               Proofview.V82.of_tactic (Simple.intro hid);
+               (fun g ->
+                  let ids = pf_ids_of_hyps g in
+                  tclTHEN
+                    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
+                    (fun g ->
+                       let ids' = pf_ids_of_hyps g in
+                       lid := List.rev (List.subtract Id.equal ids' ids);
+                       if List.is_empty !lid then lid := [hid];
+                       tclIDTAC g
+                    )
+                    g
+               );
+             ] gls)
       (fun g ->
         let sigma = project g in
-	 match EConstr.kind sigma (pf_concl g) with
-	   | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) ->
-	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
-	   | _ ->
-	       incr h_num;
+         match EConstr.kind sigma (pf_concl g) with
+           | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) ->
+               Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
+           | _ ->
+               incr h_num;
                (observe_tac (fun _ _ -> str "finishing using")
-		  (
-		    tclCOMPLETE(
-		      tclFIRST[
-			tclTHEN
-			  (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
-			  (Proofview.V82.of_tactic e_assumption);
-		      Eauto.eauto_with_bases
-			(true,5)
-			[(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
+                  (
+                    tclCOMPLETE(
+                      tclFIRST[
+                        tclTHEN
+                          (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
+                          (Proofview.V82.of_tactic e_assumption);
+                      Eauto.eauto_with_bases
+                        (true,5)
+                        [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
                         [Hints.Hint_db.empty TransparentState.empty false]
-		      ]
-		    )
-		  )
-	       )
-      		 g)
+                      ]
+                    )
+                  )
+               )
+                 g)
     in
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
@@ -1376,23 +1375,23 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
-  else 
+  else
     fst @@ Lemmas.by (Proofview.V82.tactic begin
-	fun g ->
-	  tclTHEN
-	    (decompose_and_tac)
-	    (tclORELSE
-	       (tclFIRST
-	 	  (List.map
-	 	     (fun c ->
-	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST 
-	 		  [intros;
+        fun g ->
+          tclTHEN
+            (decompose_and_tac)
+            (tclORELSE
+               (tclFIRST
+                  (List.map
+                     (fun c ->
+                        Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
+                          [intros;
                            Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
-	 		   Tacticals.New.tclCOMPLETE Auto.default_auto
-	 		  ])
-	 	     )
-	 	     using_lemmas)
-	       ) tclIDTAC)
+                           Tacticals.New.tclCOMPLETE Auto.default_auto
+                          ])
+                     )
+                     using_lemmas)
+               ) tclIDTAC)
             g end) lemma
   in
   if Lemmas.(pf_fold Proof_global.get_open_goals) lemma = 0 then (defined lemma; None) else Some lemma
@@ -1451,8 +1450,8 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let open CVars in
     let opacity =
       match terminate_ref with
-	| ConstRef c -> is_opaque_constant c
-	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
+        | ConstRef c -> is_opaque_constant c
+        | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
@@ -1461,31 +1460,31 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
-	  (fun  x ->
-	     prove_eq (fun _ -> tclIDTAC)
-	       {nb_arg=nb_arg;
+          (fun  x ->
+             prove_eq (fun _ -> tclIDTAC)
+               {nb_arg=nb_arg;
                 f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref);
-	        f_constr = EConstr.of_constr f_constr; 
-		concl_tac = tclIDTAC;
-		func=functional_ref;
-		info=(instantiate_lambda Evd.empty
+                f_constr = EConstr.of_constr f_constr;
+                concl_tac = tclIDTAC;
+                func=functional_ref;
+                info=(instantiate_lambda Evd.empty
                         (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref)))
-	       		(EConstr.of_constr f_constr::List.map mkVar x)
-		);
-		is_main_branch = true;
-		is_final = true;
-		values_and_bounds = [];
-		eqs = [];
-		forbidden_ids = [];
-		acc_inv = lazy (assert false);
-		acc_id = Id.of_string "____";
-		args_assoc = [];
-		f_id = Id.of_string "______";
-		rec_arg_id = Id.of_string "______";
-		is_mes = false;
-		ih = Id.of_string "______";
-	       }
-	  )
+                        (EConstr.of_constr f_constr::List.map mkVar x)
+                );
+                is_main_branch = true;
+                is_final = true;
+                values_and_bounds = [];
+                eqs = [];
+                forbidden_ids = [];
+                acc_inv = lazy (assert false);
+                acc_id = Id.of_string "____";
+                args_assoc = [];
+                f_id = Id.of_string "______";
+                rec_arg_id = Id.of_string "______";
+                is_mes = false;
+                ih = Id.of_string "______";
+               }
+          )
        )) lemma in
     let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in
     ()
@@ -1554,15 +1553,15 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
         com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
         false
       with e when CErrors.noncritical e ->
-	begin
-	  if do_observe ()
-	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
-	  else CErrors.user_err ~hdr:"Cannot create equation Lemma"
-               (str "Cannot create equation lemma." ++ spc () ++ 
+        begin
+          if do_observe ()
+          then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
+          else CErrors.user_err ~hdr:"Cannot create equation Lemma"
+               (str "Cannot create equation lemma." ++ spc () ++
                 str "This may be because the function is nested-recursive.")
-	  ;
-	  true
-	end
+          ;
+          true
+        end
     in
     if not stop
     then
@@ -1576,9 +1575,9 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
         (nb_prod evd (EConstr.of_constr res)) relation;
       Flags.if_verbose
         msgnl (h 1 (Ppconstr.pr_id function_name ++
-			 spc () ++ str"is defined" )++ fnl () ++
-		    h 1 (Ppconstr.pr_id equation_id ++
-			   spc () ++ str"is defined" )
+                         spc () ++ str"is defined" )++ fnl () ++
+                    h 1 (Ppconstr.pr_id equation_id ++
+                           spc () ++ str"is defined" )
       )
   in
   (* XXX STATE Why do we need this... why is the toplevel protection not enough *)