[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
```

1 files changed, 269 insertions, 269 deletions

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