Merge PR #11010: [coq] Untabify the whole ML codebase.

Reviewed-by: SkySkimmer
Reviewed-by: herbelin

1 files changed, 166 insertions, 166 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0a1371413a..0c247e2660 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -303,8 +303,8 @@ let drop_implicits_in_patt cst nb_expl args =
   in let rec aux = function
     |[] -> None
     |(_,imps)::t -> match impls_fit [] (imps,args) with
-	|None -> aux t
-	|x -> x
+        |None -> aux t
+        |x -> x
      in
      if Int.equal nb_expl 0 then aux impl_data
      else
@@ -327,7 +327,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
         assert (bl=[]);
         mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
     | _ ->
-	match decompose_notation_key ntn, l with
+        match decompose_notation_key ntn, l with
         | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
            begin match NumTok.of_string x with
            | Some n -> mkprim (loc, Numeral (SMinus,n))
@@ -378,7 +378,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
     match availability_of_prim_token p sc scopes with
       | None -> raise No_match
       | Some key ->
-	let loc = cases_pattern_loc pat in
+        let loc = cases_pattern_loc pat in
         insert_pat_coercion ?loc coercion
           (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
   with No_match ->
@@ -398,40 +398,40 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       let pat = match pat with
         | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
         | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
-	| PatCstr(cstrsp,args,na) ->
+        | PatCstr(cstrsp,args,na) ->
           let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
-	  let p =
-	    try
+          let p =
+            try
               if !Flags.raw_print then raise Exit;
-	      let projs = Recordops.lookup_projections (fst cstrsp) in
-	      let rec ip projs args acc =
-		match projs, args with
-		  | [], [] -> acc
-		  | proj :: q, pat :: tail ->
+              let projs = Recordops.lookup_projections (fst cstrsp) in
+              let rec ip projs args acc =
+                match projs, args with
+                  | [], [] -> acc
+                  | proj :: q, pat :: tail ->
                      let acc =
                        match proj, pat with
-		       | _, { CAst.v = CPatAtom None } ->
-		          (* we don't want to have 'x := _' in our patterns *)
+                       | _, { CAst.v = CPatAtom None } ->
+                          (* we don't want to have 'x := _' in our patterns *)
                           acc
-		       | Some c, _ ->
+                       | Some c, _ ->
                           ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
                        | _ -> raise No_match in
                      ip q tail acc
-	          | _ -> assert false
-	      in
-	      CPatRecord(List.rev (ip projs args []))
-	    with
-		Not_found | No_match | Exit ->
+                  | _ -> assert false
+              in
+              CPatRecord(List.rev (ip projs args []))
+            with
+                Not_found | No_match | Exit ->
                   let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
-		    if pattern_printable_in_both_syntax cstrsp
-		    then CPatCstr (c, None, args)
-		    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
-		  else
-		    let full_args = add_patt_for_params (fst cstrsp) args in
+                    if pattern_printable_in_both_syntax cstrsp
+                    then CPatCstr (c, None, args)
+                    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
+                  else
+                    let full_args = add_patt_for_params (fst cstrsp) args in
                     match drop_implicits_in_patt (GlobRef.ConstructRef cstrsp) 0 full_args with
-		      | Some true_args -> CPatCstr (c, None, true_args)
-		      | None           -> CPatCstr (c, Some full_args, [])
+                      | Some true_args -> CPatCstr (c, None, true_args)
+                      | None           -> CPatCstr (c, Some full_args, [])
           in
           insert_pat_alias ?loc (CAst.make ?loc p) na
       in
@@ -450,23 +450,23 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
           | None -> raise No_match
           (* Uninterpretation is allowed in current context *)
           | Some (scopt,key) ->
-	    let scopes' = Option.List.cons scopt scopes in
-	    let l =
+            let scopes' = Option.List.cons scopt scopes in
+            let l =
               List.map (fun (c,(subentry,(scopt,scl))) ->
                 extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c)
-		subst in
-	    let ll =
+                subst in
+            let ll =
               List.map (fun (c,(subentry,(scopt,scl))) ->
                 let subscope = (subentry,(scopt,scl@scopes')) in
-		List.map (extern_cases_pattern_in_scope subscope vars) c)
-		substlist in
-	    let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+                List.map (extern_cases_pattern_in_scope subscope vars) c)
+                substlist in
+            let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
             let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
-	      else
-		match drop_implicits_in_patt gr nb_to_drop l2 with
-		  |Some true_args -> true_args
-		  |None -> raise No_match
-	    in
+              else
+                match drop_implicits_in_patt gr nb_to_drop l2 with
+                  |Some true_args -> true_args
+                  |None -> raise No_match
+            in
             insert_pat_coercion coercion
               (insert_pat_delimiters ?loc
                  (make_pat_notation ?loc ntn (l,ll) l2') key)
@@ -482,10 +482,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
           subst in
       let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
-	else
-	  match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
-	    |Some true_args -> true_args
-	    |None -> raise No_match
+        else
+          match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+            |Some true_args -> true_args
+            |None -> raise No_match
       in
       assert (List.is_empty substlist);
       insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
@@ -500,8 +500,8 @@ and extern_notation_pattern allscopes vars t = function
           let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
           let p = apply_notation_to_pattern ?loc (GlobRef.ConstructRef cstr)
             (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
-	  insert_pat_alias ?loc p na
-	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
+          insert_pat_alias ?loc p na
+        | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
         | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
     with
         No_match -> extern_notation_pattern allscopes vars t rules
@@ -532,8 +532,8 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
       let c = extern_reference vars (GlobRef.IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
       match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with
-	   |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
-	   |None           -> CAst.make @@ CPatCstr (c, Some args, [])
+           |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
+           |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (InConstrEntrySomeLevel,(None,[])) vars p
@@ -554,8 +554,8 @@ let is_projection nargs = function
   | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
     (try
        let n = Recordops.find_projection_nparams r + 1 in
-	 if n <= nargs then Some n
-	 else None
+         if n <= nargs then Some n
+         else None
      with Not_found -> None)
   | _ -> None
 
@@ -581,23 +581,23 @@ let explicitize inctx impl (cf,f) args =
           !Flags.raw_print ||
           (!print_implicits && !print_implicits_explicit_args) ||
           (is_needed_for_correct_partial_application tail imp) ||
-	  (!print_implicits_defensive &&
-	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
-	   is_significant_implicit (Lazy.force a))
-	in
+          (!print_implicits_defensive &&
+           (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
+           is_significant_implicit (Lazy.force a))
+        in
         if visible then
           (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail
-	else
-	  tail
+        else
+          tail
     | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
     | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*)
-    | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp -> 
+    | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
       (* The non-explicit application cannot be parsed back with the same type *)
       raise Expl
     | [], _ -> []
   in
   let ip = is_projection (List.length args) cf in
-  let expl () = 
+  let expl () =
     match ip with
     | Some i ->
       (* Careful: It is possible to have declared implicits ending
@@ -609,12 +609,12 @@ let explicitize inctx impl (cf,f) args =
       if is_impl
       then raise Expl
       else
-	let (args1,args2) = List.chop i args in
+        let (args1,args2) = List.chop i args in
         let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
-	let args1 = exprec 1 (args1,impl1) in
-	let args2 = exprec (i+1) (args2,impl2) in
-	let ip = Some (List.length args1) in
-	  CApp ((ip,f),args1@args2)
+        let args1 = exprec 1 (args1,impl1) in
+        let args2 = exprec (i+1) (args2,impl2) in
+        let ip = Some (List.length args1) in
+          CApp ((ip,f),args1@args2)
     | None ->
       let args = exprec 1 (args,impl) in
         if List.is_empty args then f.CAst.v else
@@ -625,10 +625,10 @@ let explicitize inctx impl (cf,f) args =
               CApp (g,args'@args)
           | _ -> CApp ((None, f), args) in
     try expl ()
-    with Expl -> 
+    with Expl ->
       let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
       let ip = if !print_projections then ip else None in
-	CAppExpl ((ip, f', us), List.map Lazy.force args)
+        CAppExpl ((ip, f', us), List.map Lazy.force args)
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -679,22 +679,22 @@ let rec remove_coercions inctx c =
   | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
       let nargs = List.length args in
       (try match Classops.hide_coercion r with
-	  | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
-	      (* We skip a coercion *)
-	      let l = List.skipn (n - pars) args in
-	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
+          | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
+              (* We skip a coercion *)
+              let l = List.skipn (n - pars) args in
+              let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
               (* Recursively remove the head coercions *)
-	      let a' = remove_coercions true a in
-	      (* Don't flatten App's in case of funclass so that
-		 (atomic) notations on [a] work; should be compatible
-		 since printer does not care whether App's are
-		 collapsed or not and notations with an implicit
-		 coercion using funclass either would have already
-		 been confused with ordinary application or would have need
+              let a' = remove_coercions true a in
+              (* Don't flatten App's in case of funclass so that
+                 (atomic) notations on [a] work; should be compatible
+                 since printer does not care whether App's are
+                 collapsed or not and notations with an implicit
+                 coercion using funclass either would have already
+                 been confused with ordinary application or would have need
                  a surrounding context and the coercion to funclass would
                  have been made explicit to match *)
-	      if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
-	  | _ -> c
+              if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
+          | _ -> c
       with Not_found -> c)
   | _ -> c
 
@@ -841,58 +841,58 @@ let rec extern inctx scopes vars r =
 
   | GApp (f,args) ->
       (match DAst.get f with
-	 | GRef (ref,us) ->
-	     let subscopes = find_arguments_scope ref in
+         | GRef (ref,us) ->
+             let subscopes = find_arguments_scope ref in
              let args = fill_arg_scopes args subscopes scopes in
-	     begin
-	       try
+             begin
+               try
                  if !Flags.raw_print then raise Exit;
                  let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
-		 let struc = Recordops.lookup_structure (fst cstrsp) in
+                 let struc = Recordops.lookup_structure (fst cstrsp) in
                  if PrintingRecord.active (fst cstrsp) then
                    ()
                  else if PrintingConstructor.active (fst cstrsp) then
                    raise Exit
                  else if not (get_record_print ()) then
                    raise Exit;
-		 let projs = struc.Recordops.s_PROJ in
-		 let locals = struc.Recordops.s_PROJKIND in
-		 let rec cut args n =
-		   if Int.equal n 0 then args
-		   else
-		     match args with
-		     | [] -> raise No_match
-		     | _ :: t -> cut t (n - 1) in
-		 let args = cut args struc.Recordops.s_EXPECTEDPARAM in
-		 let rec ip projs locs args acc =
-		   match projs with
-		     | [] -> acc
-		     | None :: q -> raise No_match
-		     | Some c :: q ->
-		         match locs with
-			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
+                 let projs = struc.Recordops.s_PROJ in
+                 let locals = struc.Recordops.s_PROJKIND in
+                 let rec cut args n =
+                   if Int.equal n 0 then args
+                   else
+                     match args with
+                     | [] -> raise No_match
+                     | _ :: t -> cut t (n - 1) in
+                 let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+                 let rec ip projs locs args acc =
+                   match projs with
+                     | [] -> acc
+                     | None :: q -> raise No_match
+                     | Some c :: q ->
+                         match locs with
+                           | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
                            | { Recordops.pk_true_proj = false } :: locs' ->
-			       (* we don't want to print locals *)
-			       ip q locs' args acc
+                               (* we don't want to print locals *)
+                               ip q locs' args acc
                            | { Recordops.pk_true_proj = true } :: locs' ->
-			       match args with
-				 | [] -> raise No_match
-				     (* we give up since the constructor is not complete *)
-				 | (arg, scopes) :: tail ->
+                               match args with
+                                 | [] -> raise No_match
+                                     (* we give up since the constructor is not complete *)
+                                 | (arg, scopes) :: tail ->
                                      let head = extern true scopes vars arg in
                                      ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
-		   in
-		 CRecord (List.rev (ip projs locals args []))
-	       with
-		 | Not_found | No_match | Exit ->
+                   in
+                 CRecord (List.rev (ip projs locals args []))
+               with
+                 | Not_found | No_match | Exit ->
                     let args = extern_args (extern true) vars args in
-		     extern_app inctx
-		       (select_stronger_impargs (implicits_of_global ref))
+                     extern_app inctx
+                       (select_stronger_impargs (implicits_of_global ref))
                        (Some ref,extern_reference ?loc vars ref) (extern_universes us) args
-	     end
+             end
 
-	 | _       ->
-	   explicitize inctx [] (None,sub_extern false scopes vars f)
+         | _       ->
+           explicitize inctx [] (None,sub_extern false scopes vars f)
              (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
 
   | GLetIn (na,b,t,c) ->
@@ -911,7 +911,7 @@ let rec extern inctx scopes vars r =
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
       List.fold_right (Name.fold_right Id.Set.add)
-	(cases_predicate_names tml) vars in
+        (cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
                  let na' = match na, DAst.get tm with
@@ -954,9 +954,9 @@ let rec extern inctx scopes vars r =
   | GRec (fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Id.Set.add idv vars in
       (match fk with
-	 | GFix (nv,n) ->
-	     let listdecl =
-	       Array.mapi (fun i fi ->
+         | GFix (nv,n) ->
+             let listdecl =
+               Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
@@ -969,10 +969,10 @@ let rec extern inctx scopes vars r =
                              in
                  ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
-	     in
+             in
              CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
-	 | GCoFix n ->
-	     let listdecl =
+         | GCoFix n ->
+             let listdecl =
                Array.mapi (fun i fi ->
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
@@ -980,7 +980,7 @@ let rec extern inctx scopes vars r =
                  let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
                  ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
-	     in
+             in
              CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
 
   | GSort s -> CSort (extern_glob_sort s)
@@ -1102,44 +1102,44 @@ and extern_notation (custom,scopes as allscopes) vars t = function
       let loc = Glob_ops.loc_of_glob_constr t in
       try
         if is_inactive_rule keyrule then raise No_match;
-	(* Adjusts to the number of arguments expected by the notation *)
-	let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
-	  | GApp (f,args), Some n
-	      when List.length args >= n ->
-	      let args1, args2 = List.chop n args in
+        (* Adjusts to the number of arguments expected by the notation *)
+        let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
+          | GApp (f,args), Some n
+              when List.length args >= n ->
+              let args1, args2 = List.chop n args in
               let subscopes, impls =
                 match DAst.get f with
                 | GRef (ref,us) ->
-	          let subscopes =
-		    try List.skipn n (find_arguments_scope ref)
+                  let subscopes =
+                    try List.skipn n (find_arguments_scope ref)
                     with Failure _ -> [] in
-	          let impls =
-		    let impls =
-		      select_impargs_size
-		        (List.length args) (implicits_of_global ref) in
-		    try List.skipn n impls with Failure _ -> [] in
+                  let impls =
+                    let impls =
+                      select_impargs_size
+                        (List.length args) (implicits_of_global ref) in
+                    try List.skipn n impls with Failure _ -> [] in
                   subscopes,impls
                 | _ ->
                   [], [] in
-	      (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
-	      args2, subscopes, impls
-	  | GApp (f, args), None ->
+              (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
+              args2, subscopes, impls
+          | GApp (f, args), None ->
             begin match DAst.get f with
             | GRef (ref,us) ->
-	      let subscopes = find_arguments_scope ref in
-	      let impls =
-		  select_impargs_size
-		    (List.length args) (implicits_of_global ref) in
-	      f, args, subscopes, impls
+              let subscopes = find_arguments_scope ref in
+              let impls =
+                  select_impargs_size
+                    (List.length args) (implicits_of_global ref) in
+              f, args, subscopes, impls
             | _ -> t, [], [], []
             end
-	  | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
+          | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
           | _, None -> t, [], [], []
           | _ -> raise No_match in
-	(* Try matching ... *)
+        (* Try matching ... *)
         let terms,termlists,binders,binderlists =
           match_notation_constr !print_universes t pat in
-	(* Try availability of interpretation ... *)
+        (* Try availability of interpretation ... *)
         let e =
           match keyrule with
           | NotationRule (sc,ntn) ->
@@ -1152,12 +1152,12 @@ and extern_notation (custom,scopes as allscopes) vars t = function
                   (* Uninterpretation is allowed in current context *)
               | Some (scopt,key) ->
                   let scopes' = Option.List.cons scopt (snd scopes) in
-	          let l =
+                  let l =
                     List.map (fun (c,(subentry,(scopt,scl))) ->
-		      extern (* assuming no overloading: *) true
+                      extern (* assuming no overloading: *) true
                         (subentry,(scopt,scl@scopes')) vars c)
                       terms in
-		  let ll =
+                  let ll =
                     List.map (fun (c,(subentry,(scopt,scl))) ->
                       List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
                       termlists in
@@ -1174,17 +1174,17 @@ and extern_notation (custom,scopes as allscopes) vars t = function
              match availability_of_entry_coercion custom InConstrEntrySomeLevel with
              | None -> raise No_match
              | Some coercion ->
-	      let l =
+              let l =
                 List.map (fun (c,(subentry,(scopt,scl))) ->
                   extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
-		  terms in
+                  terms in
               let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
               insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
- 	if List.is_empty args then e
-	else
+        if List.is_empty args then e
+        else
           let args = fill_arg_scopes args argsscopes allscopes in
-	  let args = extern_args (extern true) vars args in
-	  CAst.make ?loc @@ explicitize false argsimpls (None,e) args
+          let args = extern_args (extern true) vars args in
+          CAst.make ?loc @@ explicitize false argsimpls (None,e) args
       with
           No_match -> extern_notation allscopes vars t rules
 
@@ -1255,15 +1255,15 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
-	| Name id   -> id
-	| Anonymous ->
-	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
+        | Name id   -> id
+        | Anonymous ->
+            anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
   | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None),
-			 [glob_of_pat avoid env sigma c])
+                         [glob_of_pat avoid env sigma c])
   | PApp (f,args) ->
       GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args)
   | PSoApp (n,args) ->
@@ -1290,19 +1290,19 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
   | PCase (info,p,tm,bl) ->
       let mat = match bl, info.cip_ind with
-	| [], _ -> []
-	| _, Some ind ->
-	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
-	  simple_cases_matrix_of_branches ind bl'
-	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
+        | [], _ -> []
+        | _, Some ind ->
+          let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
+          simple_cases_matrix_of_branches ind bl'
+        | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
       let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
-	| PMeta None, _, _ -> (Anonymous,None),None
-	| _, Some ind, Some nargs ->
-	  return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
-	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
+        | PMeta None, _, _ -> (Anonymous,None),None
+        | _, Some ind, Some nargs ->
+          return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
+        | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
   | PFix ((ln,i),(lna,tl,bl)) ->