[coq] Untabify the whole ML codebase.

We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```

5 files changed, 996 insertions, 996 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 2b990400e3..a02cb24bee 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -99,9 +99,9 @@ TACTIC EXTEND newfunind
 | ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
      {
        let c = match cl with
-	 | [] -> assert false
-	 | [c] -> c
-	 | c::cl -> EConstr.applist(c,cl)
+         | [] -> assert false
+         | [c] -> c
+         | c::cl -> EConstr.applist(c,cl)
        in
        Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl }
 END
@@ -110,9 +110,9 @@ TACTIC EXTEND snewfunind
 | ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
      {
        let c = match cl with
-	 | [] -> assert false
-	 | [c] -> c
-	 | c::cl -> EConstr.applist(c,cl)
+         | [] -> assert false
+         | [c] -> c
+         | c::cl -> EConstr.applist(c,cl)
        in
        Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl }
 END
@@ -260,7 +260,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
                   let names = List.map (fun (_,na,_) -> na) fas in
                   warning_error names e
               end
-	      | _ -> assert false (* we can only have non empty  list *)
+              | _ -> assert false (* we can only have non empty  list *)
           end
         | e when CErrors.noncritical e ->
           let names = List.map (fun (_,na,_) -> na) fas in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 895b6a37ee..e41b92d4dc 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -38,7 +38,7 @@ let rec solve_trivial_holes pat_as_term e =
   | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
        DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
   | _,_ -> pat_as_term
-                                              
+
 (*
    compose_glob_context [(bt_1,n_1,t_1);......] rt returns
    b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
@@ -90,11 +90,11 @@ let combine_results
     =
   let pre_result =     List.map
     ( fun res1 ->  (* for each result in arg_res *)
-	  List.map (* we add it in each args_res *)
-	    (fun res2 ->
-	       combine_fun res1 res2
-	    )
-	    res2.result
+          List.map (* we add it in each args_res *)
+            (fun res2 ->
+               combine_fun res1 res2
+            )
+            res2.result
       )
       res1.result
   in (* and then we flatten the map *)
@@ -127,18 +127,18 @@ let rec change_vars_in_binder mapping = function
   | (bt,t)::l ->
       let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
       (bt,change_vars mapping t)::
-	(if Id.Map.is_empty new_mapping
-	 then l
-	 else change_vars_in_binder new_mapping l
-	)
+        (if Id.Map.is_empty new_mapping
+         then l
+         else change_vars_in_binder new_mapping l
+        )
 
 let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
   | (bt,t)::l ->
       (bt,replace_var_by_term x_id term t)::
-	if Id.Set.mem x_id (ids_of_binder bt)
-	then l
-	else replace_var_by_term_in_binder x_id term l
+        if Id.Set.mem x_id (ids_of_binder bt)
+        then l
+        else replace_var_by_term_in_binder x_id term l
 
 let add_bt_names bt = Id.Set.union (ids_of_binder bt)
 
@@ -152,66 +152,66 @@ let apply_args ctxt body args =
   let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) =
     match na with
        | Name id when Id.Set.mem id avoid ->
-	   let new_id = Namegen.next_ident_away id avoid in
-	   Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
+           let new_id = Namegen.next_ident_away id avoid in
+           Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
        | _ -> na,mapping,avoid
   in
   let next_bt_away bt (avoid:Id.Set.t) =
     match bt with
       | LetIn na ->
-	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
-	  LetIn new_na,mapping,new_avoid
+          let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
+          LetIn new_na,mapping,new_avoid
       | Prod na ->
-	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
-	  Prod new_na,mapping,new_avoid
+          let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
+          Prod new_na,mapping,new_avoid
       | Lambda na ->
-	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
-	  Lambda new_na,mapping,new_avoid
+          let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
+          Lambda new_na,mapping,new_avoid
   in
   let rec do_apply avoid ctxt body args =
     match ctxt,args with
       | _,[] -> (* No more args *)
-	  (ctxt,body)
+          (ctxt,body)
       | [],_ -> (* no more fun *)
-	  let f,args' = glob_decompose_app body in
-	  (ctxt,mkGApp(f,args'@args))
+          let f,args' = glob_decompose_app body in
+          (ctxt,mkGApp(f,args'@args))
       | (Lambda Anonymous,t)::ctxt',arg::args' ->
-	  do_apply avoid ctxt' body args'
+          do_apply avoid ctxt' body args'
       | (Lambda (Name id),t)::ctxt',arg::args' ->
-	  let new_avoid,new_ctxt',new_body,new_id =
-	    if need_convert_id avoid id
-	    then
-	      let new_avoid =  Id.Set.add id avoid in
-	      let new_id = Namegen.next_ident_away id new_avoid in
-	      let new_avoid' = Id.Set.add new_id new_avoid in
-	      let mapping = Id.Map.add id new_id Id.Map.empty in
-	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
-	      let new_body = change_vars mapping body in
-	      new_avoid',new_ctxt',new_body,new_id
-	    else
-	      Id.Set.add id avoid,ctxt',body,id
-	  in
-	  let new_body = replace_var_by_term new_id arg new_body in
-	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
-	  do_apply avoid new_ctxt' new_body args'
+          let new_avoid,new_ctxt',new_body,new_id =
+            if need_convert_id avoid id
+            then
+              let new_avoid =  Id.Set.add id avoid in
+              let new_id = Namegen.next_ident_away id new_avoid in
+              let new_avoid' = Id.Set.add new_id new_avoid in
+              let mapping = Id.Map.add id new_id Id.Map.empty in
+              let new_ctxt' = change_vars_in_binder mapping ctxt' in
+              let new_body = change_vars mapping body in
+              new_avoid',new_ctxt',new_body,new_id
+            else
+              Id.Set.add id avoid,ctxt',body,id
+          in
+          let new_body = replace_var_by_term new_id arg new_body in
+          let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
+          do_apply avoid new_ctxt' new_body args'
       | (bt,t)::ctxt',_ ->
-	  let new_avoid,new_ctxt',new_body,new_bt =
-	    let new_avoid = add_bt_names bt avoid in
-	    if need_convert avoid bt
-	    then
-	      let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in
-	      (
-		new_avoid,
-		change_vars_in_binder mapping ctxt',
-		change_vars mapping body,
-		new_bt
-	     )
-	    else new_avoid,ctxt',body,bt
-	  in
-	  let new_ctxt',new_body =
-	    do_apply new_avoid new_ctxt' new_body args
-	  in
-	  (new_bt,t)::new_ctxt',new_body
+          let new_avoid,new_ctxt',new_body,new_bt =
+            let new_avoid = add_bt_names bt avoid in
+            if need_convert avoid bt
+            then
+              let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in
+              (
+                new_avoid,
+                change_vars_in_binder mapping ctxt',
+                change_vars mapping body,
+                new_bt
+             )
+            else new_avoid,ctxt',body,bt
+          in
+          let new_ctxt',new_body =
+            do_apply new_avoid new_ctxt' new_body args
+          in
+          (new_bt,t)::new_ctxt',new_body
   in
   do_apply Id.Set.empty ctxt body args
 
@@ -230,14 +230,14 @@ let combine_lam n t b =
   {
     context = [];
     value = mkGLambda(n, compose_glob_context t.context t.value,
-		      compose_glob_context b.context b.value )
+                      compose_glob_context b.context b.value )
   }
 
 let combine_prod2 n t b =
   {
     context = [];
     value = mkGProd(n, compose_glob_context t.context t.value,
-		      compose_glob_context b.context b.value )
+                      compose_glob_context b.context b.value )
   }
 
 let combine_prod n t b =
@@ -251,8 +251,8 @@ let mk_result ctxt value avoid =
   {
     result =
       [{context = ctxt;
-	value = value}]
-	;
+        value = value}]
+        ;
     to_avoid = avoid
   }
 (*************************************************
@@ -298,8 +298,8 @@ let make_discr_match_brl i =
 let make_discr_match brl =
   fun el i ->
   mkGCases(None,
-	   make_discr_match_el el,
-	   make_discr_match_brl i brl)
+           make_discr_match_el el,
+           make_discr_match_brl i brl)
 
 (**********************************************************************)
 (*  functions used to build case expression from lettuple and if ones *)
@@ -310,27 +310,27 @@ let build_constructors_of_type ind' argl =
   let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
   let npar = mib.Declarations.mind_nparams in
   Array.mapi (fun i _ ->
-		let construct = ind',i+1 in
+                let construct = ind',i+1 in
                 let constructref = GlobRef.ConstructRef(construct) in
-		let _implicit_positions_of_cst =
-		  Impargs.implicits_of_global constructref
-		in
-		let cst_narg =
+                let _implicit_positions_of_cst =
+                  Impargs.implicits_of_global constructref
+                in
+                let cst_narg =
                   Inductiveops.constructor_nallargs
-		    (Global.env ())
-		    construct
-		in
-		let argl =
+                    (Global.env ())
+                    construct
+                in
+                let argl =
                   if List.is_empty argl then
                     List.make cst_narg (mkGHole ())
                   else
                     List.make npar (mkGHole ()) @ argl
-		in
-		let pat_as_term =
+                in
+                let pat_as_term =
                   mkGApp(mkGRef (GlobRef.ConstructRef(ind',i+1)),argl)
-		in
+                in
                 cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
-	     )
+             )
     ind.Declarations.mind_consnames
 
 (******************)
@@ -359,20 +359,20 @@ let add_pat_variables sigma pat typ env : Environ.env =
     match DAst.get pat with
       | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env
       | PatCstr(c,patl,na) ->
-	  let Inductiveops.IndType(indf,indargs) =
-	    try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
-	    with Not_found -> assert false
-	  in
-	  let constructors = Inductiveops.get_constructors env indf in
-	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
-	  let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
-	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
+          let Inductiveops.IndType(indf,indargs) =
+            try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
+            with Not_found -> assert false
+          in
+          let constructors = Inductiveops.get_constructors env indf in
+          let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
+          let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
+          List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
   let new_env = add_pat_variables env pat typ in
   let res =
     fst (
       Context.Rel.fold_outside
-	(fun decl (env,ctxt) ->
+        (fun decl (env,ctxt) ->
            let open Context.Rel.Declaration in
            match decl with
            | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false
@@ -398,8 +398,8 @@ let add_pat_variables sigma pat typ env : Environ.env =
              let open Context.Named.Declaration in
              (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt)
         )
-	(Environ.rel_context new_env)
-	~init:(env,[])
+        (Environ.rel_context new_env)
+        ~init:(env,[])
     )
   in
   observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
@@ -411,16 +411,16 @@ let add_pat_variables sigma pat typ env : Environ.env =
 let rec pattern_to_term_and_type env typ  = DAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar (Name id) ->
-	mkGVar id
+        mkGVar id
   | PatCstr(constr,patternl,_) ->
       let cst_narg =
         Inductiveops.constructor_nallargs
-	  (Global.env ())
-	  constr
+          (Global.env ())
+          constr
       in
       let Inductiveops.IndType(indf,indargs) =
-	try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
-	with Not_found -> assert false
+        try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
+        with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
       let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
@@ -428,18 +428,18 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
       let _,cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
       let implicit_args =
-	Array.to_list
-	  (Array.init
-	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i)))
-	  )
+        Array.to_list
+          (Array.init
+             (cst_narg - List.length patternl)
+             (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i)))
+          )
       in
       let patl_as_term =
-	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
+        List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
       in
       mkGApp(mkGRef(GlobRef.ConstructRef constr),
-	     implicit_args@patl_as_term
-	    )
+             implicit_args@patl_as_term
+            )
   )
 
 (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
@@ -479,220 +479,220 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
   let open CAst in
   match DAst.get rt with
     | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ | GFloat _ ->
-	(* do nothing (except changing type of course) *)
-	mk_result [] rt avoid
+        (* do nothing (except changing type of course) *)
+        mk_result [] rt avoid
     | GApp(_,_) ->
-	let f,args = glob_decompose_app rt in
-	let args_res : (glob_constr list) build_entry_return =
-	  List.fold_right (* create the arguments lists of constructors and combine them *)
-	    (fun arg ctxt_argsl ->
+        let f,args = glob_decompose_app rt in
+        let args_res : (glob_constr list) build_entry_return =
+          List.fold_right (* create the arguments lists of constructors and combine them *)
+            (fun arg ctxt_argsl ->
                let arg_res = build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg in
-	       combine_results combine_args arg_res ctxt_argsl
-	    )
-	    args
-	    (mk_result [] [] avoid)
-	in
-	begin
-	  match DAst.get f with
-	    | GLambda _  -> 
-		let rec aux t l = 
-		  match l with 
-		    | [] -> t
-		    | u::l -> DAst.make @@
-			match DAst.get t with 
-			  | GLambda(na,_,nat,b) -> 
-			      GLetIn(na,u,None,aux b l)
-			  | _ -> 
-			      GApp(t,l)
-		in
+               combine_results combine_args arg_res ctxt_argsl
+            )
+            args
+            (mk_result [] [] avoid)
+        in
+        begin
+          match DAst.get f with
+            | GLambda _  ->
+                let rec aux t l =
+                  match l with
+                    | [] -> t
+                    | u::l -> DAst.make @@
+                        match DAst.get t with
+                          | GLambda(na,_,nat,b) ->
+                              GLetIn(na,u,None,aux b l)
+                          | _ ->
+                              GApp(t,l)
+                in
                 build_entry_lc env sigma funnames avoid (aux f args)
-	    | GVar id when Id.Set.mem id funnames ->
-		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
-		   then we create a fresh variable [res],
-		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
-		   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
-		   a pseudo value "v1 ... vn".
-		   The "value" of this branch is then simply [res]
-		*)
-		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
+            | GVar id when Id.Set.mem id funnames ->
+                (* if we have [f t1 ... tn] with [f]$\in$[fnames]
+                   then we create a fresh variable [res],
+                   add [res] and its "value" (i.e. [res v1 ... vn]) to each
+                   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
+                   a pseudo value "v1 ... vn".
+                   The "value" of this branch is then simply [res]
+                *)
+                let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
                 let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
-		let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
-		let res = fresh_id args_res.to_avoid "_res" in
-		let new_avoid = res::args_res.to_avoid in
-		let res_rt = mkGVar res in
-		let new_result =
-		  List.map
-		    (fun arg_res ->
-		       let new_hyps =
-			 [Prod (Name res),res_raw_type;
-			  Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)]
-		       in
-		       {context =  arg_res.context@new_hyps; value = res_rt }
-		    )
-		    args_res.result
-		in
-		{ result = new_result; to_avoid = new_avoid }
-	    | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
-		(* if have [g t1 ... tn] with [g] not appearing in [funnames]
-		   then
-		   foreach [ctxt,v1 ... vn] in [args_res] we return
-		   [ctxt, g v1 .... vn]
-		*)
-		{
-		  args_res with
-		    result =
-		    List.map
-		      (fun args_res ->
-			 {args_res with value = mkGApp(f,args_res.value)})
-		      args_res.result
-		}
-	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
-	    | GLetIn(n,v,t,b) ->
-		(* if we have [(let x := v in b) t1 ... tn] ,
-		   we discard our work and compute the list of constructor for
-		   [let x = v in (b t1 ... tn)] up to alpha conversion
-		*)
-		let new_n,new_b,new_avoid =
-		  match n with
-		    | Name id when List.exists (is_free_in id) args ->
-			(* need to alpha-convert the name *)
-			let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
-			let new_avoid = id:: avoid in
-			let new_b =
-			  replace_var_by_term
-			    id
-			    (DAst.make @@ GVar id)
-			    b
-			in
-			(Name new_id,new_b,new_avoid)
-		    | _ -> n,b,avoid
-		in
-		build_entry_lc
-		  env
+                let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
+                let res = fresh_id args_res.to_avoid "_res" in
+                let new_avoid = res::args_res.to_avoid in
+                let res_rt = mkGVar res in
+                let new_result =
+                  List.map
+                    (fun arg_res ->
+                       let new_hyps =
+                         [Prod (Name res),res_raw_type;
+                          Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)]
+                       in
+                       {context =  arg_res.context@new_hyps; value = res_rt }
+                    )
+                    args_res.result
+                in
+                { result = new_result; to_avoid = new_avoid }
+            | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
+                (* if have [g t1 ... tn] with [g] not appearing in [funnames]
+                   then
+                   foreach [ctxt,v1 ... vn] in [args_res] we return
+                   [ctxt, g v1 .... vn]
+                *)
+                {
+                  args_res with
+                    result =
+                    List.map
+                      (fun args_res ->
+                         {args_res with value = mkGApp(f,args_res.value)})
+                      args_res.result
+                }
+            | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
+            | GLetIn(n,v,t,b) ->
+                (* if we have [(let x := v in b) t1 ... tn] ,
+                   we discard our work and compute the list of constructor for
+                   [let x = v in (b t1 ... tn)] up to alpha conversion
+                *)
+                let new_n,new_b,new_avoid =
+                  match n with
+                    | Name id when List.exists (is_free_in id) args ->
+                        (* need to alpha-convert the name *)
+                        let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
+                        let new_avoid = id:: avoid in
+                        let new_b =
+                          replace_var_by_term
+                            id
+                            (DAst.make @@ GVar id)
+                            b
+                        in
+                        (Name new_id,new_b,new_avoid)
+                    | _ -> n,b,avoid
+                in
+                build_entry_lc
+                  env
       sigma
       funnames
-		  avoid
-		  (mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
-	    | GCases _  | GIf _ | GLetTuple _ ->
-		(* we have [(match e1, ...., en with ..... end) t1 tn]
-		   we first compute the result from the case and
-		   then combine each of them with each of args one
-		*)
+                  avoid
+                  (mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
+            | GCases _  | GIf _ | GLetTuple _ ->
+                (* we have [(match e1, ...., en with ..... end) t1 tn]
+                   we first compute the result from the case and
+                   then combine each of them with each of args one
+                *)
                 let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
-		combine_results combine_app f_res  args_res
-	    | GCast(b,_) ->
-		(* for an applied cast we just trash the cast part
-		   and restart the work.
+                combine_results combine_app f_res  args_res
+            | GCast(b,_) ->
+                (* for an applied cast we just trash the cast part
+                   and restart the work.
 
-		   WARNING: We need to restart since [b] itself should be an application term
-		*)
+                   WARNING: We need to restart since [b] itself should be an application term
+                *)
                 build_entry_lc env sigma funnames avoid (mkGApp(b,args))
-	    | GRec _ -> user_err Pp.(str "Not handled GRec")
-	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
+            | GRec _ -> user_err Pp.(str "Not handled GRec")
+            | GProd _ -> user_err Pp.(str "Cannot apply a type")
             | GInt _ -> user_err Pp.(str "Cannot apply an integer")
       | GFloat _ -> user_err Pp.(str "Cannot apply a float")
-	end (* end of the application treatement *)
+        end (* end of the application treatement *)
 
     | GLambda(n,_,t,b) ->
-	(* we first compute the list of constructor
-	   corresponding to the body of the function,
-	   then the one corresponding to the type
-	   and combine the two result
-	*)
+        (* we first compute the list of constructor
+           corresponding to the body of the function,
+           then the one corresponding to the type
+           and combine the two result
+        *)
         let t_res = build_entry_lc env sigma funnames avoid t  in
-	let new_n =
-	  match n with
-	    | Name _ -> n
-	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
-	in
-	let new_env = raw_push_named (new_n,None,t) env in
+        let new_n =
+          match n with
+            | Name _ -> n
+            | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
+        in
+        let new_env = raw_push_named (new_n,None,t) env in
         let b_res = build_entry_lc new_env sigma funnames avoid b in
-	combine_results (combine_lam new_n) t_res b_res
+        combine_results (combine_lam new_n) t_res b_res
     | GProd(n,_,t,b) ->
-	(* we first compute the list of constructor
-	   corresponding to the body of the function,
-	   then the one corresponding to the type
-	   and combine the two result
-	*)
+        (* we first compute the list of constructor
+           corresponding to the body of the function,
+           then the one corresponding to the type
+           and combine the two result
+        *)
         let t_res = build_entry_lc env sigma funnames avoid t in
-	let new_env = raw_push_named (n,None,t) env in
+        let new_env = raw_push_named (n,None,t) env in
         let b_res = build_entry_lc new_env sigma funnames avoid b in
         if List.length t_res.result = 1 && List.length b_res.result = 1
         then combine_results (combine_prod2 n) t_res b_res
         else combine_results (combine_prod n) t_res b_res
     | GLetIn(n,v,typ,b) ->
-	(* we first compute the list of constructor
-	   corresponding to the body of the function,
-	   then the one corresponding to the value [t]
-	   and combine the two result
-	*)
+        (* we first compute the list of constructor
+           corresponding to the body of the function,
+           then the one corresponding to the value [t]
+           and combine the two result
+        *)
         let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
         let v_res = build_entry_lc env sigma funnames avoid v in
-	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
+        let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
         let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
         let v_r = Sorts.Relevant in (* TODO relevance *)
-	let new_env =
-	  match n with
-	      Anonymous -> env
+        let new_env =
+          match n with
+              Anonymous -> env
             | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env
         in
         let b_res = build_entry_lc new_env sigma funnames avoid b in
-	combine_results (combine_letin n) v_res b_res
+        combine_results (combine_letin n) v_res b_res
     | GCases(_,_,el,brl) ->
-	(* we create the discrimination function
-	   and treat the case itself
-	*)
-	let make_discr = make_discr_match brl in
+        (* we create the discrimination function
+           and treat the case itself
+        *)
+        let make_discr = make_discr_match brl in
         build_entry_lc_from_case env sigma funnames make_discr el brl avoid
     | GIf(b,(na,e_option),lhs,rhs) ->
-	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+        let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
         let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
-	let (ind,_) =
-	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
-	  with Not_found ->
-	    user_err  (str "Cannot find the inductive associated to " ++
+        let (ind,_) =
+          try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+          with Not_found ->
+            user_err  (str "Cannot find the inductive associated to " ++
                                Printer.pr_glob_constr_env env b ++ str " in " ++
                                Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
-	in
-	let case_pats = build_constructors_of_type (fst ind) [] in
-	assert (Int.equal (Array.length case_pats) 2);
-	let brl =
-	  List.map_i
+        in
+        let case_pats = build_constructors_of_type (fst ind) [] in
+        assert (Int.equal (Array.length case_pats) 2);
+        let brl =
+          List.map_i
             (fun i x -> CAst.make ([],[case_pats.(i)],x))
-	    0
-	    [lhs;rhs]
-	in
-	let match_expr =
-	  mkGCases(None,[(b,(Anonymous,None))],brl)
-	in
-	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
+            0
+            [lhs;rhs]
+        in
+        let match_expr =
+          mkGCases(None,[(b,(Anonymous,None))],brl)
+        in
+        (* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
         build_entry_lc env sigma funnames avoid match_expr
     | GLetTuple(nal,_,b,e) ->
-	begin
-	  let nal_as_glob_constr =
-	    List.map
-	      (function
-		   Name id -> mkGVar id
-		 | Anonymous -> mkGHole ()
-	      )
-	      nal
-	  in
-	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+        begin
+          let nal_as_glob_constr =
+            List.map
+              (function
+                   Name id -> mkGVar id
+                 | Anonymous -> mkGHole ()
+              )
+              nal
+          in
+          let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
           let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
-	  let (ind,_) =
-	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
-	    with Not_found ->
-	      user_err  (str "Cannot find the inductive associated to " ++
+          let (ind,_) =
+            try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+            with Not_found ->
+              user_err  (str "Cannot find the inductive associated to " ++
                                  Printer.pr_glob_constr_env env b ++ str " in " ++
                                  Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
-	  in
-	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
-	  assert (Int.equal (Array.length case_pats) 1);
+          in
+          let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
+          assert (Int.equal (Array.length case_pats) 1);
           let br = CAst.make ([],[case_pats.(0)],e) in
-	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
+          let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
           build_entry_lc env sigma funnames avoid match_expr
 
-	end
+        end
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GCast(b,_) ->
         build_entry_lc env sigma funnames  avoid b
@@ -703,177 +703,177 @@ and build_entry_lc_from_case env sigma funname make_discr
   match el with
     | [] -> assert false (* this case correspond to match <nothing> with .... !*)
     | el ->
-	(* this case correspond to
-	   match el with brl end
-	   we first compute the list of lists corresponding to [el] and
-	   combine them .
-	   Then for each element of the combinations,
-	   we compute the result we compute one list per branch in [brl] and
-	   finally we just concatenate those list
-	*)
-	let case_resl =
-	    List.fold_right
-	      (fun (case_arg,_) ctxt_argsl ->
+        (* this case correspond to
+           match el with brl end
+           we first compute the list of lists corresponding to [el] and
+           combine them .
+           Then for each element of the combinations,
+           we compute the result we compute one list per branch in [brl] and
+           finally we just concatenate those list
+        *)
+        let case_resl =
+            List.fold_right
+              (fun (case_arg,_) ctxt_argsl ->
                 let arg_res = build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg in
-		combine_results combine_args arg_res ctxt_argsl
-	      )
-	      el
-	      (mk_result [] [] avoid)
-	in
-	let types =
-	  List.map (fun (case_arg,_) ->
-		      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
+                combine_results combine_args arg_res ctxt_argsl
+              )
+              el
+              (mk_result [] [] avoid)
+        in
+        let types =
+          List.map (fun (case_arg,_) ->
+                      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
                       EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr)
-		   ) el
-	in
-	(****** The next works only if the match is not dependent ****)
-	let results =
-	  List.map
-	    (fun ca ->
-	       let res = build_entry_lc_from_case_term
+                   ) el
+        in
+        (****** The next works only if the match is not dependent ****)
+        let results =
+          List.map
+            (fun ca ->
+               let res = build_entry_lc_from_case_term
                env sigma types
-	       funname (make_discr)
-	       []  brl
-	       case_resl.to_avoid
-	       ca
-	       in
-	       res
-	    )
-	    case_resl.result
-	in
-	{
-	  result = List.concat (List.map (fun r -> r.result) results);
-	  to_avoid =
-	    List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid)
+               funname (make_discr)
+               []  brl
+               case_resl.to_avoid
+               ca
+               in
+               res
+            )
+            case_resl.result
+        in
+        {
+          result = List.concat (List.map (fun r -> r.result) results);
+          to_avoid =
+            List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid)
               [] results
-	}
+        }
 
 and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to_prevent brl avoid
     matched_expr =
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
-	(* alpha conversion to prevent name clashes *)
+        (* alpha conversion to prevent name clashes *)
         let {CAst.v=(idl,patl,return)} = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
-	(* building a list of precondition stating that we are not in this branch
-	   (will be used in the following recursive calls)
-	*)
+        let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
+        (* building a list of precondition stating that we are not in this branch
+           (will be used in the following recursive calls)
+        *)
         let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
-	let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
-	  List.map2
-	    (fun pat typ ->
-	       fun avoid pat'_as_term ->
-		 let renamed_pat,_,_ = alpha_pat avoid pat in
-		 let pat_ids = get_pattern_id renamed_pat  in
+        let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
+          List.map2
+            (fun pat typ ->
+               fun avoid pat'_as_term ->
+                 let renamed_pat,_,_ = alpha_pat avoid pat in
+                 let pat_ids = get_pattern_id renamed_pat  in
                  let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
-		   List.fold_right
-		     (fun id acc ->
-			let typ_of_id =
-			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
-			in
-			let raw_typ_of_id =
-			  Detyping.detype Detyping.Now false Id.Set.empty
-			    env_with_pat_ids (Evd.from_env env) typ_of_id
-			in
-			mkGProd (Name id,raw_typ_of_id,acc))
-		     pat_ids
-		     (glob_make_neq pat'_as_term (pattern_to_term renamed_pat))
-	    )
-	    patl
-	    types
-	in
-	(* Checking if we can be in this branch
-	   (will be used in the following recursive calls)
-	*)
-	let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
-	  List.map
-	    (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
-	    patl
-	in
-	(*
-	   we first compute the other branch result (in ordrer to keep the order of the matching
-	   as much as possible)
-	*)
-	let brl'_res =
-	  build_entry_lc_from_case_term
-	    env
+                   List.fold_right
+                     (fun id acc ->
+                        let typ_of_id =
+                          Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
+                        in
+                        let raw_typ_of_id =
+                          Detyping.detype Detyping.Now false Id.Set.empty
+                            env_with_pat_ids (Evd.from_env env) typ_of_id
+                        in
+                        mkGProd (Name id,raw_typ_of_id,acc))
+                     pat_ids
+                     (glob_make_neq pat'_as_term (pattern_to_term renamed_pat))
+            )
+            patl
+            types
+        in
+        (* Checking if we can be in this branch
+           (will be used in the following recursive calls)
+        *)
+        let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
+          List.map
+            (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
+            patl
+        in
+        (*
+           we first compute the other branch result (in ordrer to keep the order of the matching
+           as much as possible)
+        *)
+        let brl'_res =
+          build_entry_lc_from_case_term
+            env
       sigma
-	    types
-	    funname
-	    make_discr
-	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
-	    brl'
-	    avoid
-	    matched_expr
-	in
-	(* We now create the precondition of this branch i.e.
-	   1- the list of variable appearing in the different patterns of this branch and
-	      the list of equation stating than el = patl (List.flatten ...)
-	   2- If there exists a previous branch which pattern unify with the one of this branch
+            types
+            funname
+            make_discr
+            ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
+            brl'
+            avoid
+            matched_expr
+        in
+        (* We now create the precondition of this branch i.e.
+           1- the list of variable appearing in the different patterns of this branch and
+              the list of equation stating than el = patl (List.flatten ...)
+           2- If there exists a previous branch which pattern unify with the one of this branch
               then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
-	*)
-      	let those_pattern_preconds =
-	  (List.flatten
-	    (
-	      List.map3
-	      (fun pat e typ_as_constr ->
-		 let this_pat_ids = ids_of_pat pat in
-		 let typ_as_constr = EConstr.of_constr typ_as_constr in
-		 let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
-		 let pat_as_term = pattern_to_term pat in
-                 (* removing trivial holes *) 
-                 let pat_as_term = solve_trivial_holes pat_as_term e in 
+        *)
+        let those_pattern_preconds =
+          (List.flatten
+            (
+              List.map3
+              (fun pat e typ_as_constr ->
+                 let this_pat_ids = ids_of_pat pat in
+                 let typ_as_constr = EConstr.of_constr typ_as_constr in
+                 let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
+                 let pat_as_term = pattern_to_term pat in
+                 (* removing trivial holes *)
+                 let pat_as_term = solve_trivial_holes pat_as_term e in
                   (* observe (str "those_pattern_preconds" ++ spc () ++ *)
                   (*            str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
                   (*            str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
                   (*            str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
-		 List.fold_right
-		   (fun id  acc ->
-		      if Id.Set.mem id this_pat_ids
-		      then (Prod (Name id),
-		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
-		      let raw_typ_of_id =
-			Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
-		      in
-		      raw_typ_of_id
-			   )::acc
-		      else acc
-		   )
-		   idl
-		   [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)]
-	      )
-	      patl
-	      matched_expr.value
-	      types
-	  )
-	  )
-	  @
-	  (if List.exists (function (unifl,_) ->
-			     let (unif,_) =
-			       List.split (List.map2 (fun x y -> x y) unifl patl)
-			     in
-			     List.for_all (fun x -> x) unif) patterns_to_prevent
-	   then
-	     let i = List.length patterns_to_prevent in
-	     let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
-	     [(Prod Anonymous,make_discr pats_as_constr i  )]
-	   else
-	     []
-	  )
-	in
-	(* We compute the result of the value returned by the branch*)
+                 List.fold_right
+                   (fun id  acc ->
+                      if Id.Set.mem id this_pat_ids
+                      then (Prod (Name id),
+                      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
+                      let raw_typ_of_id =
+                        Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
+                      in
+                      raw_typ_of_id
+                           )::acc
+                      else acc
+                   )
+                   idl
+                   [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)]
+              )
+              patl
+              matched_expr.value
+              types
+          )
+          )
+          @
+          (if List.exists (function (unifl,_) ->
+                             let (unif,_) =
+                               List.split (List.map2 (fun x y -> x y) unifl patl)
+                             in
+                             List.for_all (fun x -> x) unif) patterns_to_prevent
+           then
+             let i = List.length patterns_to_prevent in
+             let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
+             [(Prod Anonymous,make_discr pats_as_constr i  )]
+           else
+             []
+          )
+        in
+        (* We compute the result of the value returned by the branch*)
         let return_res = build_entry_lc new_env sigma funname new_avoid return in
-	(* and combine it with the preconds computed for this branch *)
-	let this_branch_res =
-	  List.map
-	    (fun res  ->
-	       { context = matched_expr.context@those_pattern_preconds@res.context ;
-		 value = res.value}
-	    )
-	    return_res.result
-	in
-	{ brl'_res with result = this_branch_res@brl'_res.result }
+        (* and combine it with the preconds computed for this branch *)
+        let this_branch_res =
+          List.map
+            (fun res  ->
+               { context = matched_expr.context@those_pattern_preconds@res.context ;
+                 value = res.value}
+            )
+            return_res.result
+        in
+        { brl'_res with result = this_branch_res@brl'_res.result }
 
 
 let is_res r = match DAst.get r with
@@ -891,8 +891,8 @@ let is_gvar c = match DAst.get c with
 | GVar id -> true
 | _ -> false
 
-let same_raw_term rt1 rt2 = 
-  match DAst.get rt1, DAst.get rt2 with 
+let same_raw_term rt1 rt2 =
+  match DAst.get rt1, DAst.get rt2 with
     | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
@@ -927,288 +927,288 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   let open CAst in
   match DAst.get rt with
     | GProd(n,k,t,b) ->
-	let not_free_in_t id = not (is_free_in id t) in
-	let new_crossed_types = t::crossed_types in
-	begin
-	  match DAst.get t with
-	    | GApp(res_rt ,args') when is_res res_rt ->
-		begin
+        let not_free_in_t id = not (is_free_in id t) in
+        let new_crossed_types = t::crossed_types in
+        begin
+          match DAst.get t with
+            | GApp(res_rt ,args') when is_res res_rt ->
+                begin
                   let arg = List.hd args' in
-		  match DAst.get arg with
-		    | GVar this_relname ->
-			(*i The next call to mk_rel_id is
-			  valid since we are constructing the graph
-			  Ensures by: obvious
-			  i*)
-
-			let new_t =
-			  mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
-			in
+                  match DAst.get arg with
+                    | GVar this_relname ->
+                        (*i The next call to mk_rel_id is
+                          valid since we are constructing the graph
+                          Ensures by: obvious
+                          i*)
+
+                        let new_t =
+                          mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
+                        in
                         let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
                         let r = Sorts.Relevant in (* TODO relevance *)
                         let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
                         let new_b,id_to_exclude =
-			  rebuild_cons new_env
-			    nb_args relname
-			    args new_crossed_types
-			    (depth + 1) b
-			in
-			mkGProd(n,new_t,new_b),
-			Id.Set.filter not_free_in_t id_to_exclude
-		    | _ -> (* the first args is the name of the function! *)
-			assert false
-		end
-	    | GApp(eq_as_ref,[ty; id ;rt])
+                          rebuild_cons new_env
+                            nb_args relname
+                            args new_crossed_types
+                            (depth + 1) b
+                        in
+                        mkGProd(n,new_t,new_b),
+                        Id.Set.filter not_free_in_t id_to_exclude
+                    | _ -> (* the first args is the name of the function! *)
+                        assert false
+                end
+            | GApp(eq_as_ref,[ty; id ;rt])
                 when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type")  && n == Anonymous
-		  ->
+                  ->
                 let loc1 = rt.CAst.loc in
                 let loc2 = eq_as_ref.CAst.loc in
                 let loc3 = id.CAst.loc in
                 let id = match DAst.get id with GVar id -> id | _ -> assert false in
-		begin
-		  try
+                begin
+                  try
                     observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
-		    let t' =
-		      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
+                    let t' =
+                      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
                       with e when CErrors.noncritical e -> raise Continue
-		    in
-		    let is_in_b = is_free_in id b in
-		    let _keep_eq =
-		      not (List.exists (is_free_in id) args) || is_in_b  ||
-			List.exists (is_free_in id) crossed_types
-		    in
-		    let new_args = List.map (replace_var_by_term id rt) args in
-		    let subst_b =
-		      if is_in_b then b else  replace_var_by_term id rt b
+                    in
+                    let is_in_b = is_free_in id b in
+                    let _keep_eq =
+                      not (List.exists (is_free_in id) args) || is_in_b  ||
+                        List.exists (is_free_in id) crossed_types
+                    in
+                    let new_args = List.map (replace_var_by_term id rt) args in
+                    let subst_b =
+                      if is_in_b then b else  replace_var_by_term id rt b
                     in
                     let r = Sorts.Relevant in (* TODO relevance *)
                     let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
                     let new_b,id_to_exclude =
-		      rebuild_cons
-			new_env
-			nb_args relname
-			new_args new_crossed_types
-			(depth + 1) subst_b
-		    in
-		    mkGProd(n,t,new_b),id_to_exclude
-		  with Continue ->
+                      rebuild_cons
+                        new_env
+                        nb_args relname
+                        new_args new_crossed_types
+                        (depth + 1) subst_b
+                    in
+                    mkGProd(n,t,new_b),id_to_exclude
+                  with Continue ->
                     let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
-		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
+                    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
                     let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
-		    let mib,_ = Global.lookup_inductive (fst ind) in
-		    let nparam = mib.Declarations.mind_nparams in
-		    let params,arg' =
-		      ((Util.List.chop nparam args'))
-		    in
-		    let rt_typ = DAst.make @@
+                    let mib,_ = Global.lookup_inductive (fst ind) in
+                    let nparam = mib.Declarations.mind_nparams in
+                    let params,arg' =
+                      ((Util.List.chop nparam args'))
+                    in
+                    let rt_typ = DAst.make @@
                        GApp(DAst.make @@ GRef (GlobRef.IndRef (fst ind),None),
-			    (List.map
-			      (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
-				 env (Evd.from_env env)
-				 (EConstr.of_constr p)) params)@(Array.to_list
-				      (Array.make
-					 (List.length args' - nparam)
-					 (mkGHole ()))))
-		    in
-		    let eq' =
-		      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
-		    in
+                            (List.map
+                              (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
+                                 env (Evd.from_env env)
+                                 (EConstr.of_constr p)) params)@(Array.to_list
+                                      (Array.make
+                                         (List.length args' - nparam)
+                                         (mkGHole ()))))
+                    in
+                    let eq' =
+                      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
+                    in
                     observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
-		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
-		    observe (str " computing new type for jmeq : done") ;
+                    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
+                    observe (str " computing new type for jmeq : done") ;
                     let sigma = Evd.(from_env env) in
-		    let new_args =
+                    let new_args =
                       match EConstr.kind sigma eq'_as_constr with
-			| App(_,[|_;_;ty;_|]) ->
+                        | App(_,[|_;_;ty;_|]) ->
                             let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in
-			    let ty' = snd (Util.List.chop nparam ty) in
-			    List.fold_left2
-			      (fun acc var_as_constr arg ->
-				 if isRel var_as_constr
-				 then
-				   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
-				   match na with
-				     | Anonymous -> acc
-				     | Name id' ->
-					 (id',Detyping.detype Detyping.Now false Id.Set.empty
-					    env
+                            let ty' = snd (Util.List.chop nparam ty) in
+                            List.fold_left2
+                              (fun acc var_as_constr arg ->
+                                 if isRel var_as_constr
+                                 then
+                                   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
+                                   match na with
+                                     | Anonymous -> acc
+                                     | Name id' ->
+                                         (id',Detyping.detype Detyping.Now false Id.Set.empty
+                                            env
                                             (Evd.from_env env)
-					    arg)::acc
-				 else if isVar var_as_constr
-				 then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
-					 env
+                                            arg)::acc
+                                 else if isVar var_as_constr
+                                 then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
+                                         env
                                          (Evd.from_env env)
-					 arg)::acc
-				 else acc
-			      )
-			      []
-			      arg'
-			      ty'
-			| _ -> assert false
-		    in
-		    let is_in_b = is_free_in id b in
-		    let _keep_eq =
-		      not (List.exists (is_free_in id) args) || is_in_b  ||
-			List.exists (is_free_in id) crossed_types
-		    in
-		    let new_args =
-		      List.fold_left
-			(fun args (id,rt) ->
-			   List.map (replace_var_by_term id rt) args
-			)
-			args
-			((id,rt)::new_args)
-		    in
-		    let subst_b =
-		     if is_in_b then b else  replace_var_by_term id rt b
-		    in
-		    let new_env =
-		      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
+                                         arg)::acc
+                                 else acc
+                              )
+                              []
+                              arg'
+                              ty'
+                        | _ -> assert false
+                    in
+                    let is_in_b = is_free_in id b in
+                    let _keep_eq =
+                      not (List.exists (is_free_in id) args) || is_in_b  ||
+                        List.exists (is_free_in id) crossed_types
+                    in
+                    let new_args =
+                      List.fold_left
+                        (fun args (id,rt) ->
+                           List.map (replace_var_by_term id rt) args
+                        )
+                        args
+                        ((id,rt)::new_args)
+                    in
+                    let subst_b =
+                     if is_in_b then b else  replace_var_by_term id rt b
+                    in
+                    let new_env =
+                      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
                       let r = Sorts.Relevant in (* TODO relevance *)
                       EConstr.push_rel (LocalAssum (make_annot n r,t')) env
                     in
-		    let new_b,id_to_exclude =
-		      rebuild_cons
-			new_env
-			nb_args relname
-			new_args new_crossed_types
-			(depth + 1) subst_b
-		    in
-		    mkGProd(n,eq',new_b),id_to_exclude
-		end
-		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
-		     if keep_eq then
-		     mkGProd(n,t,new_b),id_to_exclude
-		     else new_b, Id.Set.add id id_to_exclude
-		  *)
-	    | GApp(eq_as_ref,[ty;rt1;rt2])
+                    let new_b,id_to_exclude =
+                      rebuild_cons
+                        new_env
+                        nb_args relname
+                        new_args new_crossed_types
+                        (depth + 1) subst_b
+                    in
+                    mkGProd(n,eq',new_b),id_to_exclude
+                end
+                  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
+                     if keep_eq then
+                     mkGProd(n,t,new_b),id_to_exclude
+                     else new_b, Id.Set.add id id_to_exclude
+                  *)
+            | GApp(eq_as_ref,[ty;rt1;rt2])
                 when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
-		  ->
-	      begin
-		try 
+                  ->
+              begin
+                try
                   let l = decompose_raw_eq env rt1 rt2 in
-		  if List.length l > 1 
-		  then 
-		    let new_rt =
-		      List.fold_left 
-			(fun acc (lhs,rhs) -> 
-			  mkGProd(Anonymous,
+                  if List.length l > 1
+                  then
+                    let new_rt =
+                      List.fold_left
+                        (fun acc (lhs,rhs) ->
+                          mkGProd(Anonymous,
                                   mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc)
-			)
-			b
-			l
-		    in
-		    rebuild_cons env nb_args relname args crossed_types depth new_rt
-		  else raise Continue
-	      with Continue -> 
+                        )
+                        b
+                        l
+                    in
+                    rebuild_cons env nb_args relname args crossed_types depth new_rt
+                  else raise Continue
+              with Continue ->
                 observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
-		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
+                let t',ctx = Pretyping.understand env (Evd.from_env env) t in
                 let r = Sorts.Relevant in (* TODO relevance *)
                 let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
                 let new_b,id_to_exclude =
-		  rebuild_cons new_env
-		    nb_args relname
-		    args new_crossed_types
-		    (depth + 1) b
-		in
-		match n with
-		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Id.Set.remove id
-			(Id.Set.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-	      end
-	    | _ ->
+                  rebuild_cons new_env
+                    nb_args relname
+                    args new_crossed_types
+                    (depth + 1) b
+                in
+                match n with
+                  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+                      new_b,Id.Set.remove id
+                        (Id.Set.filter not_free_in_t id_to_exclude)
+                  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+              end
+            | _ ->
                 observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
-		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
+                let t',ctx = Pretyping.understand env (Evd.from_env env) t in
                 let r = Sorts.Relevant in (* TODO relevance *)
                 let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
                 let new_b,id_to_exclude =
-		  rebuild_cons new_env
-		    nb_args relname
-		    args new_crossed_types
-		    (depth + 1) b
-		in
-		match n with
-		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Id.Set.remove id
-			(Id.Set.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-	end
+                  rebuild_cons new_env
+                    nb_args relname
+                    args new_crossed_types
+                    (depth + 1) b
+                in
+                match n with
+                  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+                      new_b,Id.Set.remove id
+                        (Id.Set.filter not_free_in_t id_to_exclude)
+                  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+        end
     | GLambda(n,k,t,b) ->
-	begin
-	  let not_free_in_t id = not (is_free_in id t) in
-	  let new_crossed_types = t :: crossed_types in
+        begin
+          let not_free_in_t id = not (is_free_in id t) in
+          let new_crossed_types = t :: crossed_types in
           observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
-	  let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-	  match n with
-	    | Name id ->
+          let t',ctx = Pretyping.understand env (Evd.from_env env) t in
+          match n with
+            | Name id ->
               let r = Sorts.Relevant in (* TODO relevance *)
               let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
                 let new_b,id_to_exclude =
-		  rebuild_cons new_env
-		    nb_args relname
-		    (args@[mkGVar id])new_crossed_types
-		    (depth + 1 ) b
-		in
-		if Id.Set.mem id id_to_exclude && depth >= nb_args
-		then
-		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-		else
-		  DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-	    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
-		(* We have renamed all the anonymous functions during alpha_renaming phase *)
-
-	end
+                  rebuild_cons new_env
+                    nb_args relname
+                    (args@[mkGVar id])new_crossed_types
+                    (depth + 1 ) b
+                in
+                if Id.Set.mem id id_to_exclude && depth >= nb_args
+                then
+                  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
+                else
+                  DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+            | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
+                (* We have renamed all the anonymous functions during alpha_renaming phase *)
+
+        end
     | GLetIn(n,v,t,b) ->
-	begin
+        begin
           let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
-	  let not_free_in_t id = not (is_free_in id t) in
-	  let evd = (Evd.from_env env) in
-	  let t',ctx = Pretyping.understand env evd t in
-	  let evd = Evd.from_ctx ctx in
+          let not_free_in_t id = not (is_free_in id t) in
+          let evd = (Evd.from_env env) in
+          let t',ctx = Pretyping.understand env evd t in
+          let evd = Evd.from_ctx ctx in
           let type_t' = Typing.unsafe_type_of env evd t' in
           let t' = EConstr.Unsafe.to_constr t' in
-	  let type_t' = EConstr.Unsafe.to_constr type_t' in
+          let type_t' = EConstr.Unsafe.to_constr type_t' in
           let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
-	  let new_b,id_to_exclude =
-	    rebuild_cons new_env
-	      nb_args relname
-	      args (t::crossed_types)
-	      (depth + 1 ) b in
-	  match n with
-	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
-		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-	    | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
-		Id.Set.filter not_free_in_t id_to_exclude
-	end
+          let new_b,id_to_exclude =
+            rebuild_cons new_env
+              nb_args relname
+              args (t::crossed_types)
+              (depth + 1 ) b in
+          match n with
+            | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
+                new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
+            | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
+                Id.Set.filter not_free_in_t id_to_exclude
+        end
     | GLetTuple(nal,(na,rto),t,b) ->
-	assert (Option.is_empty rto);
-	begin
-	  let not_free_in_t id = not (is_free_in id t) in
-	  let new_t,id_to_exclude' =
-	    rebuild_cons env
-	      nb_args
-	      relname
-	      args (crossed_types)
-	      depth t
-	  in
-	  let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
+        assert (Option.is_empty rto);
+        begin
+          let not_free_in_t id = not (is_free_in id t) in
+          let new_t,id_to_exclude' =
+            rebuild_cons env
+              nb_args
+              relname
+              args (crossed_types)
+              depth t
+          in
+          let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
           let r = Sorts.Relevant in (* TODO relevance *)
           let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in
           let new_b,id_to_exclude =
-	    rebuild_cons new_env
-	      nb_args relname
-	      args (t::crossed_types)
-	      (depth + 1) b
-	  in
+            rebuild_cons new_env
+              nb_args relname
+              args (t::crossed_types)
+              (depth + 1) b
+          in
 (* 	  match n with  *)
 (* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
 (* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
-		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
+          DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
+                Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
-	end
+        end
 
     | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
@@ -1249,7 +1249,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
       compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
-		 discrimination ones *)
+                 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
@@ -1260,17 +1260,17 @@ and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
     | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c ->
-	compute_cst_params_from_app (param::acc) (params',rtl')
+        compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
 let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
-	 List.fold_left
-	   (fun params (_,cst) -> compute_cst_params relnames params cst)
-	   args
-	   csts.(i)
+         List.fold_left
+           (fun params (_,cst) -> compute_cst_params relnames params cst)
+           args
+           csts.(i)
       )
       args
   in
@@ -1278,16 +1278,16 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_
   let _ =
     try
       List.iteri
-	(fun i ((n,nt,typ) as param) ->
-	   if Array.for_all
-	     (fun l ->
-		let (n',nt',typ') = List.nth l i in
-		Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ')
-	     rels_params
-	   then
-	     l := param::!l
-	)
-	rels_params.(0)
+        (fun i ((n,nt,typ) as param) ->
+           if Array.for_all
+             (fun l ->
+                let (n',nt',typ') = List.nth l i in
+                Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ')
+             rels_params
+           then
+             l := param::!l
+        )
+        rels_params.(0)
     with e when CErrors.noncritical e ->
       ()
   in
@@ -1333,7 +1333,7 @@ let do_build_inductive
        let t = EConstr.Unsafe.to_constr t in
        evd,
        Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t))
-			 env
+                         env
       )
       funnames
       (Array.of_list funconstants)
@@ -1350,23 +1350,23 @@ let do_build_inductive
   let env_with_graphs =
     let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
       let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
-	funargs
+        funargs
       in
       List.fold_right
-	(fun (n,t,typ) acc ->
+        (fun (n,t,typ) acc ->
           match typ with
           | Some typ ->
              CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
-			      acc)
-	  | None ->
-	     CAst.make @@ Constrexpr.CProdN
+                              acc)
+          | None ->
+             CAst.make @@ Constrexpr.CProdN
                ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
-		acc
-	       )
-	)
-	rel_first_args
-	(rebuild_return_type returned_types.(i))
+                acc
+               )
+        )
+        rel_first_args
+        (rebuild_return_type returned_types.(i))
     in
     (* We need to lift back our work topconstr but only with all information
        We mimic a Set Printing All.
@@ -1383,15 +1383,15 @@ let do_build_inductive
   let constr i res =
     List.map
       (function result (* (args',concl') *) ->
-	 let rt = compose_glob_context result.context result.value in
-	 let nb_args = List.length funsargs.(i) in
-	 (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
-	 fst (
-	   rebuild_cons env_with_graphs nb_args relnames.(i)
-	     []
-	     []
-	     rt
-	 )
+         let rt = compose_glob_context result.context result.value in
+         let nb_args = List.length funsargs.(i) in
+         (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
+         fst (
+           rebuild_cons env_with_graphs nb_args relnames.(i)
+             []
+             []
+             rt
+         )
       )
       res.result
   in
@@ -1427,12 +1427,12 @@ let do_build_inductive
          | Some typ ->
            CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
-			    acc)
-	 | None ->
+                            acc)
+         | None ->
            CAst.make @@ Constrexpr.CProdN
            ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
-	    acc
-	   )
+            acc
+           )
       )
       rel_first_args
       (rebuild_return_type returned_types.(i))
@@ -1446,7 +1446,7 @@ let do_build_inductive
     List.fold_left
       (fun  acc (na,_,_) ->
        match na with
-	 Anonymous -> acc
+         Anonymous -> acc
        | Name id -> id::acc
       )
       []
@@ -1459,8 +1459,8 @@ let do_build_inductive
          | Some typ ->
            Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t,
                                   Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
-	 | None ->
-	 Constrexpr.CLocalAssum
+         | None ->
+         Constrexpr.CLocalAssum
            ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
@@ -1469,9 +1469,9 @@ let do_build_inductive
     Array.map (List.map
       (fun (id,t) ->
          false,((CAst.make id),
-		with_full_print
-		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
-	       )
+                with_full_print
+                  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
+               )
       ))
       (rel_constructors)
   in
@@ -1510,35 +1510,35 @@ let do_build_inductive
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
-	let _time3 = System.get_time () in
+        let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	let repacked_rel_inds =
+        let repacked_rel_inds =
           List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
-	                  rel_inds
-	in
-	let msg =
-	  str "while trying to define"++ spc () ++
+                          rel_inds
+        in
+        let msg =
+          str "while trying to define"++ spc () ++
             Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
-	    ++ fnl () ++
-	    msg
-	in
-	observe (msg);
-	raise e
+            ++ fnl () ++
+            msg
+        in
+        observe (msg);
+        raise e
     | reraise ->
-	let _time3 = System.get_time () in
+        let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	let repacked_rel_inds =
+        let repacked_rel_inds =
           List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
-	                  rel_inds
-	in
-	let msg =
-	  str "while trying to define"++ spc () ++
+                          rel_inds
+        in
+        let msg =
+          str "while trying to define"++ spc () ++
             Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
-	    ++ fnl () ++
-	    CErrors.print reraise
-	in
- 	observe msg;
-	raise reraise
+            ++ fnl () ++
+            CErrors.print reraise
+        in
+        observe msg;
+        raise reraise
 
 
 
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index ff0e98d00f..a29e5dff23 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -8,10 +8,10 @@ open Names
 
 val build_inductive :
 (*  (ModPath.t * DirPath.t) option ->
-  Id.t list -> (* The list of function name *) 
+  Id.t list -> (* The list of function name *)
  *)
   Evd.evar_map ->
-  Constr.pconstant list -> 
+  Constr.pconstant list ->
   (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5f54bad598..f2d98a13ab 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -36,7 +36,7 @@ let glob_decompose_app =
 (*     msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
     match DAst.get rt with
     | GApp(rt,rtl) ->
-	decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
+        decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
     | _ -> rt,List.rev acc
   in
   decompose_rapp []
@@ -62,62 +62,62 @@ let change_vars =
     DAst.map_with_loc (fun ?loc -> function
       | GRef _ as x -> x
       | GVar id ->
-	  let new_id =
-	    try
-	      Id.Map.find id mapping
-	    with Not_found -> id
-	  in
-	  GVar(new_id)
+          let new_id =
+            try
+              Id.Map.find id mapping
+            with Not_found -> id
+          in
+          GVar(new_id)
       | GEvar _ as x   -> x
       | GPatVar _ as x -> x
       | GApp(rt',rtl) ->
-	  GApp(change_vars mapping rt',
-	       List.map (change_vars mapping) rtl
-	      )
+          GApp(change_vars mapping rt',
+               List.map (change_vars mapping) rtl
+              )
       | GLambda(name,k,t,b) ->
-	  GLambda(name,
-		  k,
-		  change_vars mapping t,
-		  change_vars (remove_name_from_mapping mapping name) b
-		 )
+          GLambda(name,
+                  k,
+                  change_vars mapping t,
+                  change_vars (remove_name_from_mapping mapping name) b
+                 )
       | GProd(name,k,t,b) ->
-	  GProd(  name,
-	          k,
-		  change_vars mapping t,
-		  change_vars (remove_name_from_mapping mapping name) b
-		 )
+          GProd(  name,
+                  k,
+                  change_vars mapping t,
+                  change_vars (remove_name_from_mapping mapping name) b
+                 )
       | GLetIn(name,def,typ,b) ->
-	  GLetIn(name,
-		 change_vars mapping def,
-		 Option.map (change_vars mapping) typ,
-		 change_vars (remove_name_from_mapping mapping name) b
-		)
+          GLetIn(name,
+                 change_vars mapping def,
+                 Option.map (change_vars mapping) typ,
+                 change_vars (remove_name_from_mapping mapping name) b
+                )
       | GLetTuple(nal,(na,rto),b,e) ->
-	  let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
-	  GLetTuple(nal,
-		    (na, Option.map (change_vars mapping) rto),
-		    change_vars mapping b,
-		    change_vars new_mapping e
-		   )
+          let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
+          GLetTuple(nal,
+                    (na, Option.map (change_vars mapping) rto),
+                    change_vars mapping b,
+                    change_vars new_mapping e
+                   )
       | GCases(sty,infos,el,brl) ->
-	  GCases(sty,
-		 infos,
-		 List.map (fun (e,x) -> (change_vars mapping e,x)) el,
-		 List.map (change_vars_br mapping) brl
-		)
+          GCases(sty,
+                 infos,
+                 List.map (fun (e,x) -> (change_vars mapping e,x)) el,
+                 List.map (change_vars_br mapping) brl
+                )
       | GIf(b,(na,e_option),lhs,rhs) ->
-	  GIf(change_vars mapping b,
-	      (na,Option.map (change_vars mapping) e_option),
-	      change_vars mapping lhs,
-	      change_vars mapping rhs
-	     )
+          GIf(change_vars mapping b,
+              (na,Option.map (change_vars mapping) e_option),
+              change_vars mapping lhs,
+              change_vars mapping rhs
+             )
       | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported")
       | GSort _ as x -> x
       | GHole _ as x -> x
       | GInt _ as x -> x
       | GFloat _ as x -> x
       | GCast(b,c) ->
-	  GCast(change_vars mapping b,
+          GCast(change_vars mapping b,
                 Glob_ops.map_cast_type (change_vars mapping) c)
       ) rt
   and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
@@ -134,40 +134,40 @@ let rec alpha_pat excluded pat =
   let loc = pat.CAst.loc in
   match DAst.get pat with
     | PatVar Anonymous ->
-	let new_id = Indfun_common.fresh_id excluded "_x" in
-	(DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+        let new_id = Indfun_common.fresh_id excluded "_x" in
+        (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
     | PatVar(Name id) ->
-	if Id.List.mem id excluded
-	then
-	  let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
-	  (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
-	(Id.Map.add id new_id Id.Map.empty)
-	else pat, excluded,Id.Map.empty
+        if Id.List.mem id excluded
+        then
+          let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+          (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
+        (Id.Map.add id new_id Id.Map.empty)
+        else pat, excluded,Id.Map.empty
     | PatCstr(constr,patl,na) ->
-	let new_na,new_excluded,map =
-	  match na with
-	    | Name id when Id.List.mem id excluded ->
-		let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
-		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
-	    | _ -> na,excluded,Id.Map.empty
-	in
-	let new_patl,new_excluded,new_map =
-	  List.fold_left
-	    (fun (patl,excluded,map) pat ->
-	       let new_pat,new_excluded,new_map = alpha_pat excluded pat in
-	       (new_pat::patl,new_excluded,Id.Map.fold Id.Map.add new_map map)
-	    )
-	    ([],new_excluded,map)
-	    patl
-	in
+        let new_na,new_excluded,map =
+          match na with
+            | Name id when Id.List.mem id excluded ->
+                let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+                Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
+            | _ -> na,excluded,Id.Map.empty
+        in
+        let new_patl,new_excluded,new_map =
+          List.fold_left
+            (fun (patl,excluded,map) pat ->
+               let new_pat,new_excluded,new_map = alpha_pat excluded pat in
+               (new_pat::patl,new_excluded,Id.Map.fold Id.Map.add new_map map)
+            )
+            ([],new_excluded,map)
+            patl
+        in
         (DAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
 
 let alpha_patl excluded patl  =
   let patl,new_excluded,map =
     List.fold_left
       (fun (patl,excluded,map) pat ->
-	 let new_pat,new_excluded,new_map = alpha_pat excluded pat in
-	 new_pat::patl,new_excluded,(Id.Map.fold Id.Map.add new_map map)
+         let new_pat,new_excluded,new_map = alpha_pat excluded pat in
+         new_pat::patl,new_excluded,(Id.Map.fold Id.Map.add new_map map)
       )
       ([],excluded,Id.Map.empty)
       patl
@@ -182,15 +182,15 @@ let raw_get_pattern_id pat acc =
     match DAst.get pat with
       | PatVar(Anonymous) -> assert false
       | PatVar(Name id) ->
-	  [id]
+          [id]
       | PatCstr(constr,patternl,_) ->
-	  List.fold_right
-	  (fun pat idl ->
-	     let idl' = get_pattern_id pat in
-	     idl'@idl
-	  )
-	    patternl
-	    []
+          List.fold_right
+          (fun pat idl ->
+             let idl' = get_pattern_id pat in
+             idl'@idl
+          )
+            patternl
+            []
   in
   (get_pattern_id pat)@acc
 
@@ -202,109 +202,109 @@ let rec alpha_rt excluded rt =
     match DAst.get rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
       | GLambda(Anonymous,k,t,b) ->
-	  let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in
-	  let new_excluded = new_id :: excluded in
-	  let new_t = alpha_rt new_excluded t in
-	  let new_b = alpha_rt new_excluded b in
-	  GLambda(Name new_id,k,new_t,new_b)
+          let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in
+          let new_excluded = new_id :: excluded in
+          let new_t = alpha_rt new_excluded t in
+          let new_b = alpha_rt new_excluded b in
+          GLambda(Name new_id,k,new_t,new_b)
       | GProd(Anonymous,k,t,b) ->
-	let new_t = alpha_rt excluded t in
-	let new_b = alpha_rt excluded b in
-	GProd(Anonymous,k,new_t,new_b)
+        let new_t = alpha_rt excluded t in
+        let new_b = alpha_rt excluded b in
+        GProd(Anonymous,k,new_t,new_b)
     | GLetIn(Anonymous,b,t,c) ->
-	let new_b = alpha_rt excluded b in
-	let new_t = Option.map (alpha_rt excluded) t in
-	let new_c = alpha_rt excluded c in
-	GLetIn(Anonymous,new_b,new_t,new_c)
+        let new_b = alpha_rt excluded b in
+        let new_t = Option.map (alpha_rt excluded) t in
+        let new_c = alpha_rt excluded c in
+        GLetIn(Anonymous,new_b,new_t,new_c)
     | GLambda(Name id,k,t,b) ->
-	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
-	let t,b =
-	  if Id.equal new_id id
-	  then t, b
-	  else
-	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
-	    (t,replace b)
-	in
-	let new_excluded = new_id::excluded in
-	let new_t = alpha_rt new_excluded t in
-	let new_b = alpha_rt new_excluded b in
-	GLambda(Name new_id,k,new_t,new_b)
+        let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+        let t,b =
+          if Id.equal new_id id
+          then t, b
+          else
+            let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
+            (t,replace b)
+        in
+        let new_excluded = new_id::excluded in
+        let new_t = alpha_rt new_excluded t in
+        let new_b = alpha_rt new_excluded b in
+        GLambda(Name new_id,k,new_t,new_b)
     | GProd(Name id,k,t,b) ->
-	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
-	let new_excluded = new_id::excluded in
-	let t,b =
-	  if Id.equal new_id id
-	  then t,b
-	  else
-	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
-	    (t,replace b)
-	in
-	let new_t = alpha_rt new_excluded t in
-	let new_b = alpha_rt new_excluded b in
-	GProd(Name new_id,k,new_t,new_b)
+        let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+        let new_excluded = new_id::excluded in
+        let t,b =
+          if Id.equal new_id id
+          then t,b
+          else
+            let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
+            (t,replace b)
+        in
+        let new_t = alpha_rt new_excluded t in
+        let new_b = alpha_rt new_excluded b in
+        GProd(Name new_id,k,new_t,new_b)
     | GLetIn(Name id,b,t,c) ->
-	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
-	let c =
-	  if Id.equal new_id id then c
-	  else change_vars (Id.Map.add id new_id Id.Map.empty) c
-	in
-	let new_excluded = new_id::excluded in
-	let new_b = alpha_rt new_excluded b in
-	let new_t = Option.map (alpha_rt new_excluded) t in
-	let new_c = alpha_rt new_excluded c in
-	GLetIn(Name new_id,new_b,new_t,new_c)
+        let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+        let c =
+          if Id.equal new_id id then c
+          else change_vars (Id.Map.add id new_id Id.Map.empty) c
+        in
+        let new_excluded = new_id::excluded in
+        let new_b = alpha_rt new_excluded b in
+        let new_t = Option.map (alpha_rt new_excluded) t in
+        let new_c = alpha_rt new_excluded c in
+        GLetIn(Name new_id,new_b,new_t,new_c)
 
     | GLetTuple(nal,(na,rto),t,b) ->
-	let rev_new_nal,new_excluded,mapping =
-	  List.fold_left
-	    (fun (nal,excluded,mapping) na ->
-	       match na with
-		 | Anonymous -> (na::nal,excluded,mapping)
-		 | Name id ->
-		     let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
-		     if Id.equal new_id id
-		     then
-		       na::nal,id::excluded,mapping
-		     else
-		       (Name new_id)::nal,id::excluded,(Id.Map.add id new_id mapping)
-	    )
-	    ([],excluded,Id.Map.empty)
-	    nal
-	in
-	let new_nal = List.rev rev_new_nal in
-	let new_rto,new_t,new_b =
-	  if Id.Map.is_empty mapping
-	  then rto,t,b
-	  else let replace = change_vars mapping in
-	  (Option.map replace rto, t,replace b)
-	in
-	let new_t = alpha_rt new_excluded new_t in
-	let new_b = alpha_rt new_excluded new_b in
-	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
-	GLetTuple(new_nal,(na,new_rto),new_t,new_b)
+        let rev_new_nal,new_excluded,mapping =
+          List.fold_left
+            (fun (nal,excluded,mapping) na ->
+               match na with
+                 | Anonymous -> (na::nal,excluded,mapping)
+                 | Name id ->
+                     let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+                     if Id.equal new_id id
+                     then
+                       na::nal,id::excluded,mapping
+                     else
+                       (Name new_id)::nal,id::excluded,(Id.Map.add id new_id mapping)
+            )
+            ([],excluded,Id.Map.empty)
+            nal
+        in
+        let new_nal = List.rev rev_new_nal in
+        let new_rto,new_t,new_b =
+          if Id.Map.is_empty mapping
+          then rto,t,b
+          else let replace = change_vars mapping in
+          (Option.map replace rto, t,replace b)
+        in
+        let new_t = alpha_rt new_excluded new_t in
+        let new_b = alpha_rt new_excluded new_b in
+        let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
+        GLetTuple(new_nal,(na,new_rto),new_t,new_b)
     | GCases(sty,infos,el,brl) ->
-	let new_el =
-	  List.map (function (rt,i) -> alpha_rt excluded rt, i) el
-	in
-	GCases(sty,infos,new_el,List.map (alpha_br excluded) brl)
+        let new_el =
+          List.map (function (rt,i) -> alpha_rt excluded rt, i) el
+        in
+        GCases(sty,infos,new_el,List.map (alpha_br excluded) brl)
     | GIf(b,(na,e_o),lhs,rhs) ->
-	GIf(alpha_rt excluded b,
-	    (na,Option.map (alpha_rt excluded) e_o),
-	    alpha_rt excluded lhs,
-	    alpha_rt excluded rhs
-	   )
+        GIf(alpha_rt excluded b,
+            (na,Option.map (alpha_rt excluded) e_o),
+            alpha_rt excluded lhs,
+            alpha_rt excluded rhs
+           )
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GSort _
     | GInt _
     | GFloat _
     | GHole _ as rt -> rt
     | GCast (b,c) ->
-	GCast(alpha_rt excluded b,
+        GCast(alpha_rt excluded b,
               Glob_ops.map_cast_type (alpha_rt excluded) c)
     | GApp(f,args) ->
-	GApp(alpha_rt excluded f,
-	     List.map (alpha_rt excluded) args
-	    )
+        GApp(alpha_rt excluded f,
+             List.map (alpha_rt excluded) args
+            )
   in
   new_rt
 
@@ -327,30 +327,30 @@ let is_free_in id =
     | GPatVar _ -> false
     | GApp(rt,rtl) -> List.exists is_free_in (rt::rtl)
     | GLambda(n,_,t,b) | GProd(n,_,t,b) ->
-	let check_in_b =
-	  match n with
-	    | Name id' -> not (Id.equal id' id)
-	    | _ -> true
-	in
-	is_free_in t || (check_in_b && is_free_in b)
+        let check_in_b =
+          match n with
+            | Name id' -> not (Id.equal id' id)
+            | _ -> true
+        in
+        is_free_in t || (check_in_b && is_free_in b)
     | GLetIn(n,b,t,c) ->
-	let check_in_c =
-	  match n with
-	    | Name id' -> not (Id.equal id' id)
-	    | _ -> true
-	in
-	is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c)
+        let check_in_c =
+          match n with
+            | Name id' -> not (Id.equal id' id)
+            | _ -> true
+        in
+        is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c)
     | GCases(_,_,el,brl) ->
-	(List.exists (fun (e,_) -> is_free_in e) el) ||
-	  List.exists is_free_in_br brl
+        (List.exists (fun (e,_) -> is_free_in e) el) ||
+          List.exists is_free_in_br brl
     | GLetTuple(nal,_,b,t) ->
-	let check_in_nal =
-	  not (List.exists (function Name id' -> Id.equal id' id | _ -> false) nal)
-	in
-	is_free_in t  || (check_in_nal && is_free_in b)
+        let check_in_nal =
+          not (List.exists (function Name id' -> Id.equal id' id | _ -> false) nal)
+        in
+        is_free_in t  || (check_in_nal && is_free_in b)
 
     | GIf(cond,_,br1,br2) ->
-	is_free_in cond || is_free_in br1 || is_free_in br2
+        is_free_in cond || is_free_in br1 || is_free_in br2
     | GRec _  -> user_err Pp.(str "Not handled GRec")
     | GSort _ -> false
     | GHole _ -> false
@@ -368,26 +368,26 @@ let is_free_in id =
 let rec pattern_to_term pt = DAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar(Name id) ->
-	mkGVar id
+        mkGVar id
   | PatCstr(constr,patternl,_) ->
       let cst_narg =
         Inductiveops.constructor_nallargs
-	  (Global.env ())
-	  constr
+          (Global.env ())
+          constr
       in
       let implicit_args =
-	Array.to_list
-	  (Array.init
-	     (cst_narg - List.length patternl)
-	     (fun _ -> mkGHole ())
-	  )
+        Array.to_list
+          (Array.init
+             (cst_narg - List.length patternl)
+             (fun _ -> mkGHole ())
+          )
       in
       let patl_as_term =
-	List.map pattern_to_term patternl
+        List.map pattern_to_term patternl
       in
       mkGApp(mkGRef(GlobRef.ConstructRef constr),
-	     implicit_args@patl_as_term
-	    )
+             implicit_args@patl_as_term
+            )
   ) pt
 
 
@@ -399,51 +399,51 @@ let replace_var_by_term x_id term =
       | GEvar _
       | GPatVar _ as rt -> rt
       | GApp(rt',rtl) ->
-	  GApp(replace_var_by_pattern rt',
-	       List.map replace_var_by_pattern rtl
-	      )
+          GApp(replace_var_by_pattern rt',
+               List.map replace_var_by_pattern rtl
+              )
       | GLambda(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
       | GLambda(name,k,t,b) ->
-	  GLambda(name,
-		  k,
-		  replace_var_by_pattern t,
-		  replace_var_by_pattern b
-		 )
+          GLambda(name,
+                  k,
+                  replace_var_by_pattern t,
+                  replace_var_by_pattern b
+                 )
       | GProd(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
       | GProd(name,k,t,b) ->
-	  GProd(  name,
-	          k,
-		  replace_var_by_pattern t,
-		  replace_var_by_pattern b
-		 )
+          GProd(  name,
+                  k,
+                  replace_var_by_pattern t,
+                  replace_var_by_pattern b
+                 )
       | GLetIn(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
       | GLetIn(name,def,typ,b) ->
-	  GLetIn(name,
-		 replace_var_by_pattern def,
-		 Option.map (replace_var_by_pattern) typ,
-		 replace_var_by_pattern b
-		)
+          GLetIn(name,
+                 replace_var_by_pattern def,
+                 Option.map (replace_var_by_pattern) typ,
+                 replace_var_by_pattern b
+                )
       | GLetTuple(nal,_,_,_) as rt
-	  when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal  ->
-	  rt
+          when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal  ->
+          rt
       | GLetTuple(nal,(na,rto),def,b) ->
-	  GLetTuple(nal,
-		    (na,Option.map replace_var_by_pattern rto),
-		    replace_var_by_pattern def,
-		    replace_var_by_pattern b
-		   )
+          GLetTuple(nal,
+                    (na,Option.map replace_var_by_pattern rto),
+                    replace_var_by_pattern def,
+                    replace_var_by_pattern b
+                   )
       | GCases(sty,infos,el,brl) ->
-	  GCases(sty,
-		 infos,
-		 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
-		 List.map replace_var_by_pattern_br brl
-		)
+          GCases(sty,
+                 infos,
+                 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
+                 List.map replace_var_by_pattern_br brl
+                )
       | GIf(b,(na,e_option),lhs,rhs) ->
-	  GIf(replace_var_by_pattern b,
-	      (na,Option.map replace_var_by_pattern e_option),
-	      replace_var_by_pattern lhs,
-	      replace_var_by_pattern rhs
-	     )
+          GIf(replace_var_by_pattern b,
+              (na,Option.map replace_var_by_pattern e_option),
+              replace_var_by_pattern lhs,
+              replace_var_by_pattern rhs
+             )
       | GRec _ ->
         CErrors.user_err (Pp.str "Not handled GRec")
       | GSort _
@@ -451,7 +451,7 @@ let replace_var_by_term x_id term =
       | GInt _ as rt -> rt
       | GFloat _ as rt -> rt
       | GCast(b,c) ->
-	  GCast(replace_var_by_pattern b,
+          GCast(replace_var_by_pattern b,
                 Glob_ops.map_cast_type replace_var_by_pattern c)
     ) x
   and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) =
@@ -471,16 +471,16 @@ let rec are_unifiable_aux  = function
   | [] -> ()
   | (l, r) ::eqs ->
       match DAst.get l, DAst.get r with
-	 | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs
-	 | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
-	     if not (eq_constructor constructor2 constructor1)
-	     then raise NotUnifiable
-	     else
-	       let eqs' =
-		 try (List.combine cpl1 cpl2) @ eqs
-		 with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux.")
-	       in
-	       are_unifiable_aux eqs'
+         | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs
+         | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
+             if not (eq_constructor constructor2 constructor1)
+             then raise NotUnifiable
+             else
+               let eqs' =
+                 try (List.combine cpl1 cpl2) @ eqs
+                 with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux.")
+               in
+               are_unifiable_aux eqs'
 
 let are_unifiable pat1 pat2 =
   try
@@ -493,17 +493,17 @@ let rec eq_cases_pattern_aux  = function
   | [] -> ()
   | (l, r) ::eqs ->
       match DAst.get l, DAst.get r with
-	 | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
-	 | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
-	     if not (eq_constructor constructor2 constructor1)
-	     then raise NotUnifiable
-	     else
-	       let eqs' =
-		 try (List.combine cpl1 cpl2) @ eqs
-		 with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux.")
-	       in
-	       eq_cases_pattern_aux eqs'
-	 | _ -> raise NotUnifiable
+         | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
+         | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
+             if not (eq_constructor constructor2 constructor1)
+             then raise NotUnifiable
+             else
+               let eqs' =
+                 try (List.combine cpl1 cpl2) @ eqs
+                 with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux.")
+               in
+               eq_cases_pattern_aux eqs'
+         | _ -> raise NotUnifiable
 
 let eq_cases_pattern pat1 pat2 =
   try
@@ -528,50 +528,50 @@ let expand_as =
     match DAst.get rt with
       | PatVar _ -> map
       | PatCstr(_,patl,Name id) ->
-	  Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl)
+          Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl)
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map = DAst.map (function
       | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt
       | GVar id as rt ->
-	  begin
-	    try
-	      DAst.get (Id.Map.find id map)
-	    with Not_found -> rt
-	  end
+          begin
+            try
+              DAst.get (Id.Map.find id map)
+            with Not_found -> rt
+          end
       | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args)
       | GLambda(na,k,t,b) -> GLambda(na,k,expand_as map t, expand_as map b)
       | GProd(na,k,t,b) -> GProd(na,k,expand_as map t, expand_as map b)
       | GLetIn(na,v,typ,b) -> GLetIn(na, expand_as map v,Option.map (expand_as map) typ,expand_as map b)
       | GLetTuple(nal,(na,po),v,b) ->
-	  GLetTuple(nal,(na,Option.map (expand_as map) po),
-		    expand_as map v, expand_as map b)
+          GLetTuple(nal,(na,Option.map (expand_as map) po),
+                    expand_as map v, expand_as map b)
       | GIf(e,(na,po),br1,br2) ->
-	  GIf(expand_as map e,(na,Option.map (expand_as map) po),
-	      expand_as map br1, expand_as map br2)
+          GIf(expand_as map e,(na,Option.map (expand_as map) po),
+              expand_as map br1, expand_as map br2)
       | GRec _ ->  user_err Pp.(str "Not handled GRec")
       | GCast(b,c) ->
-	  GCast(expand_as map b,
+          GCast(expand_as map b,
                 Glob_ops.map_cast_type (expand_as map) c)
       | GCases(sty,po,el,brl) ->
-	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
-		List.map (expand_as_br map) brl)
+          GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+                List.map (expand_as_br map) brl)
     )
   and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} =
     CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
   expand_as Id.Map.empty
 
-(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution 
+(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
  *)
 
 exception Found of Evd.evar_info
 let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expected_type=Pretyping.WithoutTypeConstraint) env sigma rt =
   let open Evd in
-  let open Evar_kinds in 
+  let open Evar_kinds in
   (* we first (pseudo) understand [rt] and get back the computed evar_map *)
-  (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. 
-If someone knows how to prevent solved existantial removal in  understand, please do not hesitate to change the computation of [ctx] here *) 
+  (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed.
+If someone knows how to prevent solved existantial removal in  understand, please do not hesitate to change the computation of [ctx] here *)
   let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
   let ctx = Evd.minimize_universes ctx in
   let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in
@@ -603,7 +603,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
        )
     | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
        (
-         let res = 
+         let res =
            try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
              Evd.fold (* to simulate an iter *)
                (fun _ evi _ ->
@@ -622,9 +622,9 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
                    (* we just have to lift the solution in glob_term *)
                    Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c)
                 | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
-         in 
+         in
          res
        )
-    | _ -> Glob_ops.map_glob_constr change rt 
+    | _ -> Glob_ops.map_glob_constr change rt
   in
   change rt
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 70211a1860..bdde66bbd7 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -101,8 +101,8 @@ val   ids_of_pat : cases_pattern -> Id.Set.t
 
 val expand_as : glob_constr -> glob_constr
 
-(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution 
+(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
  *)
 val resolve_and_replace_implicits :
-      ?flags:Pretyping.inference_flags -> 
+      ?flags:Pretyping.inference_flags ->
       ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr