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

9 files changed, 137 insertions, 137 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index dbb60e6712..de3c660938 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -270,7 +270,7 @@ let of_ftactic ftac gl =
   in
   (sigma, ans)
 
-let interp_wit wit ist gl x = 
+let interp_wit wit ist gl x =
   let globarg = in_gen (glbwit wit) x in
   let arg = Tacinterp.interp_genarg ist globarg in
   let (sigma, arg) = of_ftactic arg gl in
@@ -350,7 +350,7 @@ let same_prefix s t n =
   let rec loop i = i = n || s.[i] = t.[i] && loop (i + 1) in loop 0
 
 let skip_digits s =
-  let n = String.length s in 
+  let n = String.length s in
   let rec loop i = if i < n && is_digit s.[i] then loop (i + 1) else i in loop
 
 let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d_" t i)
@@ -368,7 +368,7 @@ let wildcard_tag = "_the_"
 let wildcard_post = "_wildcard_"
 let mk_wildcard_id i =
   Id.of_string (Printf.sprintf "%s%s%s" wildcard_tag (CString.ordinal i) wildcard_post)
-let has_wildcard_tag s = 
+let has_wildcard_tag s =
   let n = String.length s in let m = String.length wildcard_tag in
   let m' = String.length wildcard_post in
   n < m + m' + 2 && same_prefix s wildcard_tag m &&
@@ -440,7 +440,7 @@ let inc_safe n = if n = 0 then n else n + 1
 let rec safe_depth s c = match EConstr.kind s c with
 | LetIn ({binder_name=Name x}, _, _, c') when is_discharged_id x -> safe_depth s c' + 1
 | LetIn (_, _, _, c') | Prod (_, _, c') -> inc_safe (safe_depth s c')
-| _ -> 0 
+| _ -> 0
 
 let red_safe (r : Reductionops.reduction_function) e s c0 =
   let rec red_to e c n = match EConstr.kind s c with
@@ -518,7 +518,7 @@ let resolve_typeclasses ~where ~fail env sigma =
   sigma
 
 
-let nf_evar sigma t = 
+let nf_evar sigma t =
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
 
 let pf_abs_evars2 gl rigid (sigma, c0) =
@@ -535,7 +535,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
     let t = Context.Named.fold_inside abs_dc ~init:concl dc in
     nf_evar sigma t in
   let rec put evlist c = match Constr.kind c with
-  | Evar (k, a) ->  
+  | Evar (k, a) ->
     if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else
     let n = max 0 (Array.length a - nenv) in
     let t = abs_evar n k in (k, (n, t)) :: put evlist t
@@ -561,11 +561,11 @@ let pf_abs_evars gl t = pf_abs_evars2 gl [] t
 
 
 (* As before but if (?i : T(?j)) and (?j : P : Prop), then the lambda for i
- * looks like (fun evar_i : (forall pi : P. T(pi))) thanks to "loopP" and all 
+ * looks like (fun evar_i : (forall pi : P. T(pi))) thanks to "loopP" and all
  * occurrences of evar_i are replaced by (evar_i evar_j) thanks to "app".
  *
  * If P can be solved by ssrautoprop (that defaults to trivial), then
- * the corresponding lambda looks like (fun evar_i : T(c)) where c is 
+ * the corresponding lambda looks like (fun evar_i : T(c)) where c is
  * the solution found by ssrautoprop.
  *)
 let ssrautoprop_tac = ref (fun gl -> assert false)
@@ -596,11 +596,11 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
     let t = Context.Named.fold_inside abs_dc ~init:concl dc in
     nf_evar sigma0 (nf_evar sigma t) in
   let rec put evlist c = match Constr.kind c with
-  | Evar (k, a) ->  
+  | Evar (k, a) ->
     if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else
     let n = max 0 (Array.length a - nenv) in
-    let k_ty = 
-      Retyping.get_sort_family_of 
+    let k_ty =
+      Retyping.get_sort_family_of
         (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in
     let is_prop = k_ty = InProp in
     let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t
@@ -610,23 +610,23 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
     (fun (k,_) -> Evar.print k) evlist));
-  let evplist = 
-    let depev = List.fold_left (fun evs (_,(_,t,_)) -> 
+  let evplist =
+    let depev = List.fold_left (fun evs (_,(_,t,_)) ->
         let t = EConstr.of_constr t in
         Intset.union evs (Evarutil.undefined_evars_of_term sigma t)) Intset.empty evlist in
     List.filter (fun (i,(_,_,b)) -> b && Intset.mem i depev) evlist in
-  let evlist, evplist, sigma = 
+  let evlist, evplist, sigma =
     if evplist = [] then evlist, [], sigma else
     List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) ->
-      try 
+      try
         let ng, sigma = call_on_evar !ssrautoprop_tac i sigma in
         if (ng <> []) then errorstrm (str "Should we tell the user?");
         List.filter (fun (j,_) -> j <> i) ev, evp, sigma
       with _ -> ev, p::evp, sigma) (evlist, [], sigma) (List.rev evplist) in
   let c0 = nf_evar sigma c0 in
-  let evlist = 
+  let evlist =
     List.map (fun (x,(y,t,z)) -> x,(y,nf_evar sigma t,z)) evlist in
-  let evplist = 
+  let evplist =
     List.map (fun (x,(y,t,z)) -> x,(y,nf_evar sigma t,z)) evplist in
   pp(lazy(str"c0= " ++ pr_constr c0));
   let rec lookup k i = function
@@ -646,7 +646,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let rec loopP evlist c i = function
   | (_, (n, t, _)) :: evl ->
     let t = get evlist (i - 1) t in
-    let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in 
+    let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in
     loopP evlist (mkProd (make_annot n Sorts.Relevant, t, c)) (i - 1) evl
   | [] -> c in
   let rec loop c i = function
@@ -655,8 +655,8 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
     let t_evplist = List.filter (fun (k,_) -> Intset.mem k evs) evplist in
     let t = loopP t_evplist (get t_evplist 1 t) 1 t_evplist in
     let t = get evlist (i - 1) t in
-    let extra_args = 
-      List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) 
+    let extra_args =
+      List.map (fun (k,_) -> mkRel (fst (lookup k i evlist)))
         (List.rev t_evplist) in
     let c = if extra_args = [] then c else app extra_args 1 c in
     loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, t, c)) (i - 1) evl
@@ -755,7 +755,7 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project
 
 (** look up a name in the ssreflect internals module *)
 let ssrdirpath = DirPath.make [Id.of_string "ssreflect"]
-let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) 
+let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name)
 let mkSsrRef name =
   let qn = Format.sprintf "plugins.ssreflect.%s" name in
   if Coqlib.has_ref qn then Coqlib.lib_ref qn else
@@ -858,7 +858,7 @@ let top_id = mk_internal_id "top assumption"
 let ssr_n_tac seed n gl =
   let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in
   let fail msg = CErrors.user_err (Pp.str msg) in
-  let tacname = 
+  let tacname =
     try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
     with Not_found -> try Tacenv.locate_tactic (ssrqid name)
     with Not_found ->
@@ -927,13 +927,13 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
 
 (* TASSI: given (c : ty), generates (c ??? : ty[???/...]) with m evars *)
 exception NotEnoughProducts
-let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m 
+let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m
 =
-  let rec loop ty args sigma n = 
-  if n = 0 then 
+  let rec loop ty args sigma n =
+  if n = 0 then
     let args = List.rev args in
      (if beta then Reductionops.whd_beta sigma else fun x -> x)
-      (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma 
+      (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma
   else match EConstr.kind_of_type sigma ty with
   | ProdType (_, src, tgt) ->
       let sigma = create_evar_defs sigma in
@@ -941,7 +941,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
         Evarutil.new_evar env sigma
           (if bi_types then Reductionops.nf_betaiota env sigma src else src) in
       loop (EConstr.Vars.subst1 x tgt) ((m - n,x) :: args) sigma (n-1)
-  | CastType (t, _) -> loop t args sigma n 
+  | CastType (t, _) -> loop t args sigma n
   | LetInType (_, v, _, t) -> loop (EConstr.Vars.subst1 v t) args sigma n
   | SortType _ -> assert false
   | AtomicType _ ->
@@ -953,10 +953,10 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   in
    loop ty [] sigma m
 
-let pf_saturate ?beta ?bi_types gl c ?ty m = 
+let pf_saturate ?beta ?bi_types gl c ?ty m =
   let env, sigma, si = pf_env gl, project gl, sig_it gl in
   let t, ty, args, sigma = saturate ?beta ?bi_types env sigma c ?ty m in
-  t, ty, args, re_sig si sigma 
+  t, ty, args, re_sig si sigma
 
 let pf_partial_solution gl t evl =
   let sigma, g = project gl, sig_it gl in
@@ -973,7 +973,7 @@ let dependent_apply_error =
  * is just like apply, but with a user-provided number n of implicits.
  *
  * Refine.refine function that handles type classes and evars but fails to
- * handle "dependently typed higher order evars". 
+ * handle "dependently typed higher order evars".
  *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
@@ -998,7 +998,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g
     let t, gl = if n = 0 then t, gl else
       let sigma, si = project gl, sig_it gl in
       let rec loop sigma bo args = function (* saturate with metas *)
-        | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma 
+        | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma
         | n -> match EConstr.kind sigma bo with
           | Lambda (_, ty, bo) ->
               if not (EConstr.Vars.closed0 sigma ty) then
@@ -1041,7 +1041,7 @@ let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl ->
    let g, env = Tacmach.pf_concl gl, pf_env gl in
    let sigma = project gl in
    match EConstr.kind sigma g with
-   | App (hd, _) when EConstr.isLambda sigma hd -> 
+   | App (hd, _) when EConstr.isLambda sigma hd ->
       Proofview.V82.of_tactic (convert_concl_no_check (Reductionops.whd_beta sigma g)) gl
    | _ -> tclIDTAC gl)
   (Proofview.V82.of_tactic
@@ -1066,9 +1066,9 @@ let is_pf_var sigma c =
 let hyp_of_var sigma v = SsrHyp (Loc.tag @@ EConstr.destVar sigma v)
 
 let interp_clr sigma = function
-| Some clr, (k, c) 
+| Some clr, (k, c)
   when (k = xNoFlag  || k = xWithAt) && is_pf_var sigma c ->
-   hyp_of_var sigma c :: clr 
+   hyp_of_var sigma c :: clr
 | Some clr, _ -> clr
 | None, _ -> []
 
@@ -1091,7 +1091,7 @@ let tclDO n tac =
   let prefix i = str"At iteration " ++ int i ++ str": " in
   let tac_err_at i gl =
     try tac gl
-    with 
+    with
     | CErrors.UserError (l, s) as e ->
         let _, info = CErrors.push e in
         let e' = CErrors.UserError (l, prefix i ++ s) in
@@ -1123,7 +1123,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
   let pat = interp_cpattern gl t None in (* UGLY API *)
   let gl = pf_merge_uc_of (fst pat) gl in
   let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in
-  let (c, ucst), cl = 
+  let (c, ucst), cl =
     try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1
     with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in
   let gl = pf_merge_uc ucst gl in
@@ -1131,9 +1131,9 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
   let cl = EConstr.of_constr cl in
   let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in
   if not(occur_existential sigma c) then
-    if tag_of_cpattern t = xWithAt then 
+    if tag_of_cpattern t = xWithAt then
       if not (EConstr.isVar sigma c) then
-	errorstrm (str "@ can be used with variables only")
+        errorstrm (str "@ can be used with variables only")
       else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with
       | NamedDecl.LocalAssum _ -> errorstrm (str "@ can be used with let-ins only")
       | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl),c,clr,ucst,gl
@@ -1186,7 +1186,7 @@ let gen_tmp_ids
   push_ctxs ctx
     (tclTHENLIST
       (List.map (fun (id,orig_ref) ->
-        tclTHEN 
+        tclTHEN
         (gentac ((None,Some(false,[])),cpattern_of_id id))
         (rename_hd_prod orig_ref))
       ctx.tmp_ids) gl)
@@ -1210,7 +1210,7 @@ let pfLIFT f =
     Proofview.tclUNIT x
 ;;
 
-(* TASSI: This version of unprotects inlines the unfold tactic definition, 
+(* TASSI: This version of unprotects inlines the unfold tactic definition,
  * since we don't want to wipe out let-ins, and it seems there is no flag
  * to change that behaviour in the standard unfold code *)
 let unprotecttac gl =
@@ -1219,8 +1219,8 @@ let unprotecttac gl =
   Tacticals.onClause (fun idopt ->
     let hyploc = Option.map (fun id -> id, InHyp) idopt in
     Proofview.V82.of_tactic (Tactics.reduct_option ~check:false
-      (Reductionops.clos_norm_flags 
-        (CClosure.RedFlags.mkflags 
+      (Reductionops.clos_norm_flags
+        (CClosure.RedFlags.mkflags
           [CClosure.RedFlags.fBETA;
            CClosure.RedFlags.fCONST prot;
            CClosure.RedFlags.fMATCH;
@@ -1253,7 +1253,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
      let x' = make_annot (Name (f x)) (NamedDecl.get_relevance hyp) in
      let prod = EConstr.mkProd (x', NamedDecl.get_type hyp, EConstr.Vars.subst_var x c) in
      gl, EConstr.mkVar x :: args, prod
-  | _, Some ((x, "@"), Some p) -> 
+  | _, Some ((x, "@"), Some p) ->
      let x = hoi_id x in
      let cp = interp_cpattern gl p None in
      let gl = pf_merge_uc_of (fst cp) gl in
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index db1d2d456e..741db9a6c2 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -38,7 +38,7 @@ val hoi_id : ssrhyp_or_id -> Id.t
 
 (******************************* hints ***********************************)
 
-val mk_hint : 'a -> 'a ssrhint 
+val mk_hint : 'a -> 'a ssrhint
 val mk_orhint : 'a -> bool * 'a
 val nullhint : bool * 'a list
 val nohint : 'a ssrhint
@@ -122,7 +122,7 @@ val mkCLambda : ?loc:Loc.t -> Name.t -> constr_expr ->  constr_expr ->  constr_e
 val isCHoles : constr_expr list -> bool
 val isCxHoles : (constr_expr * 'a option) list -> bool
 
-val intern_term : 
+val intern_term :
   Tacinterp.interp_sign -> env ->
     ssrterm -> Glob_term.glob_constr
 
@@ -152,7 +152,7 @@ val pf_e_type_of :
   Goal.goal Evd.sigma ->
   EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
 
-val splay_open_constr : 
+val splay_open_constr :
            Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
            (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
@@ -181,7 +181,7 @@ val mk_evar_name : int -> Name.t
 val ssr_anon_hyp : string
 val pf_type_id :  Goal.goal Evd.sigma -> EConstr.types -> Id.t
 
-val pf_abs_evars : 
+val pf_abs_evars :
            Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
            int * EConstr.t * Evar.t list *
@@ -235,7 +235,7 @@ val is_discharged_id : Id.t -> bool
 val mk_discharged_id : Id.t -> Id.t
 val is_tagged : string -> string -> bool
 val has_discharged_tag : string -> bool
-val ssrqid : string -> Libnames.qualid 
+val ssrqid : string -> Libnames.qualid
 val new_tmp_id :
   tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx
 val mk_anon_id : string -> Id.t list -> Id.t
@@ -244,7 +244,7 @@ val pf_abs_evars_pirrel :
            evar_map * Constr.constr -> int * Constr.constr
 val nbargs_open_constr : Goal.goal Evd.sigma -> Evd.evar_map * EConstr.t -> int
 val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int
-val gen_tmp_ids : 
+val gen_tmp_ids :
            ?ist:Geninterp.interp_sign ->
            (Goal.goal * tac_ctx) Evd.sigma ->
            (Goal.goal * tac_ctx) list Evd.sigma
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index d0426c86b9..26962ee87b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -36,7 +36,7 @@ module RelDecl = Context.Rel.Declaration
  * checks if the eliminator is recursive or not *)
 let analyze_eliminator elimty env sigma =
   let rec loop ctx t = match EConstr.kind_of_type sigma t with
-  | AtomicType (hd, args) when EConstr.isRel sigma hd -> 
+  | AtomicType (hd, args) when EConstr.isRel sigma hd ->
     ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t
   | CastType (t, _) -> loop ctx t
   | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t
@@ -50,7 +50,7 @@ let analyze_eliminator elimty env sigma =
       str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
   let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in
   let n_elim_args = Context.Rel.nhyps ctx in
-  let is_rec_elim = 
+  let is_rec_elim =
      let count_occurn n term =
        let count = ref 0 in
        let rec occur_rec n c = match EConstr.kind sigma c with
@@ -59,7 +59,7 @@ let analyze_eliminator elimty env sigma =
        in
        occur_rec n term; !count in
      let occurr2 n t = count_occurn n t > 1 in
-     not (List.for_all_i 
+     not (List.for_all_i
        (fun i (_,rd) -> pred_id <= i || not (occurr2 (pred_id - i) rd))
        1 (assums_of_rel_context ctx))
   in
@@ -68,7 +68,7 @@ let analyze_eliminator elimty env sigma =
 
 let subgoals_tys sigma (relctx, concl) =
   let rec aux cur_depth acc = function
-    | hd :: rest -> 
+    | hd :: rest ->
         let ty = Context.Rel.Declaration.get_type hd in
         if EConstr.Vars.noccurn sigma cur_depth concl &&
            List.for_all_i (fun i -> function
@@ -94,7 +94,7 @@ let subgoals_tys sigma (relctx, concl) =
  * 1. find the eliminator if not given as ~elim and analyze it
  * 2. build the patterns to be matched against the conclusion, looking at
  *    (occ, c), deps and the pattern inferred from the type of the eliminator
- * 3. build the new predicate matching the patterns, and the tactic to 
+ * 3. build the new predicate matching the patterns, and the tactic to
  *    generalize the equality in case eqid is not None
  * 4. build the tactic handle instructions and clears as required in ipats and
  *    by eqid *)
@@ -131,7 +131,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   let is_undef_pat = function
   | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t)
   | _ -> false in
-  let match_pat env p occ h cl = 
+  let match_pat env p occ h cl =
     let sigma0 = project orig_gl in
     ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
     let (c,ucst), cl =
@@ -139,11 +139,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     ppdebug(lazy Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
     c, EConstr.of_constr cl, ucst in
   let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *)
-    let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in 
+    let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in
     let t, _, _, sigma = saturate ~beta:true env (project gl) t n in
     Evd.merge_universe_context sigma ucst, T (EConstr.Unsafe.to_constr t) in
   let unif_redex gl (sigma, r as p) t = (* t is a hint for the redex of p *)
-    let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in 
+    let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in
     let t, _, _, sigma = saturate ~beta:true env sigma t n in
     let sigma = Evd.merge_universe_context sigma ucst in
     match r with
@@ -317,11 +317,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           (* if we are the index for the equation we do not clear *)
           let clr_t = if deps = [] && eqid <> None then [] else clr_t in
           let p = if is_undef_pat p then mkTpat gl inf_t else p in
-          loop (patterns @ [i, p, inf_t, occ]) 
+          loop (patterns @ [i, p, inf_t, occ])
             (clr_t @ clr) (i+1) (deps, inf_deps)
-      | [], c :: inf_deps -> 
+      | [], c :: inf_deps ->
           ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c));
-          loop (patterns @ [i, mkTpat gl c, c, allocc]) 
+          loop (patterns @ [i, mkTpat gl c, c, allocc])
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
     let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with
@@ -332,7 +332,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
          let occ = if occ = None then allocc else occ in
          let inf_p, inf_deps_r = List.hd inf_deps_r, List.tl inf_deps_r in
          deps, [1, pc, inf_p, occ], inf_deps_r in
-    let patterns, clr, gl = 
+    let patterns, clr, gl =
       loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in
     head_p @ patterns, Util.List.uniquize clr, gl
   in
@@ -340,7 +340,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns)));
   (* Predicate generation, and (if necessary) tactic to generalize the
    * equation asked by the user *)
-  let elim_pred, gen_eq_tac, clr, gl = 
+  let elim_pred, gen_eq_tac, clr, gl =
     let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++
       spc()++pp_term gl t++spc()++str"while the inferred pattern"++
       spc()++pr_econstr_pat env (project gl) (fire_subst gl inf_t)++spc()++ str"doesn't") in
@@ -356,19 +356,19 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         let gl = try pf_unify_HO gl inf_t c
                  with exn when CErrors.noncritical exn -> error gl c inf_t in
         cl, gl, post
-      with 
+      with
       | NoMatch | NoProgress ->
           let e, ucst = redex_of_pattern env p in
           let gl = pf_merge_uc ucst gl in
           let e = EConstr.of_constr e in
           let n, e, _, _ucst =  pf_abs_evars gl (fst p, e) in
-          let e, _, _, gl = pf_saturate ~beta:true gl e n in 
+          let e, _, _, gl = pf_saturate ~beta:true gl e n in
           let gl = try pf_unify_HO gl inf_t e
                    with exn when CErrors.noncritical exn -> error gl e inf_t in
           cl, gl, post
-    in        
+    in
     let rec match_all concl gl patterns =
-      let concl, gl, postponed = 
+      let concl, gl, postponed =
         List.fold_left match_or_postpone (concl, gl, []) patterns in
       if postponed = [] then concl, gl
       else if List.length postponed = List.length patterns then
@@ -377,8 +377,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       else match_all concl gl postponed in
     let concl, gl = match_all concl gl patterns in
     let pred_rctx, _ = EConstr.decompose_prod_assum (project gl) (fire_subst gl predty) in
-    let concl, gen_eq_tac, clr, gl = match eqid with 
-    | Some (IPatId _) when not is_rec -> 
+    let concl, gen_eq_tac, clr, gl = match eqid with
+    | Some (IPatId _) when not is_rec ->
         let k = List.length deps in
         let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in
         let gl, t = pfe_type_of gl c in
@@ -405,7 +405,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     | _ -> concl, Tacticals.tclIDTAC, clr, gl in
     let mk_lam t r = EConstr.mkLambda_or_LetIn r t in
     let concl = List.fold_left mk_lam concl pred_rctx in
-    let gl, concl = 
+    let gl, concl =
       if eqid <> None && is_rec then
         let gl, concls = pfe_type_of gl concl in
         let concl, gl = mkProt concls concl gl in
@@ -421,10 +421,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in
   let gl, _ = pf_e_type_of gl elim in
   (* check that the patterns do not contain non instantiated dependent metas *)
-  let () = 
+  let () =
     let evars_of_term = Evarutil.undefined_evars_of_term (project gl) in
     let patterns = List.map (fun (_,_,t,_) -> fire_subst gl t) patterns in
-    let patterns_ev = List.map evars_of_term patterns in 
+    let patterns_ev = List.map evars_of_term patterns in
     let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in
     let ty_ev = Evar.Set.fold (fun i e ->
          let ex = i in
@@ -441,7 +441,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     end
   in
   (* the elim tactic, with the eliminator and the predicated we computed *)
-  let elim = project gl, elim in 
+  let elim = project gl, elim in
   let seed =
     Array.map (fun ty ->
     let ctx,_ = EConstr.decompose_prod_assum (project gl) ty in
@@ -517,7 +517,7 @@ let perform_injection c gl =
   let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in
   let id = injecteq_id in
   let id_with_ebind = (EConstr.mkVar id, NoBindings) in
-  let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in 
+  let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in
   Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl
 
 let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 742890637a..cdda84a18d 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -125,8 +125,8 @@ let newssrcongrtac arg ist gl =
     | Some gl_c ->
         tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true (fs gl_c c)))
           (t_ok (proj gl_c)) gl
-    | None -> t_fail () gl in 
-  let mk_evar gl ty = 
+    | None -> t_fail () gl in
+  let mk_evar gl ty =
     let env, sigma, si = pf_env gl, project gl, sig_it gl in
     let sigma = Evd.create_evar_defs sigma in
     let (sigma, x) = Evarutil.new_evar env sigma ty in
@@ -174,7 +174,7 @@ let nodocc = mkclr []
 
 let is_rw_cut = function RWred (Cut _) -> true | _ -> false
 
-let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg =   
+let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg =
  if rt <> RWeq then begin
    if rt = RWred Nop && not (m = nomult && occ = None && rx = None)
                      && (clr = None || clr = Some []) then
@@ -190,7 +190,7 @@ let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg =
 let norwmult = L2R, nomult
 let norwocc = noclr, None
 
-let simplintac occ rdx sim gl = 
+let simplintac occ rdx sim gl =
   let simptac m gl =
     if m <> ~-1 then begin
       if rdx <> None then
@@ -219,7 +219,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with
 
 (* Strip a pattern generated by a prenex implicit to its constant. *)
 let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
-  | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> 
+  | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f ->
     (sigma, f), true
   | Const _ | Var _ -> p, true
   | Proj _ -> p, true
@@ -235,7 +235,7 @@ let all_ok _ _ = true
 let fake_pmatcher_end () =
   mkProp, L2R, (Evd.empty, UState.empty, mkProp)
 
-let unfoldintac occ rdx t (kt,_) gl = 
+let unfoldintac occ rdx t (kt,_) gl =
   let fs sigma x = Reductionops.nf_evar sigma x in
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
@@ -250,18 +250,18 @@ let unfoldintac occ rdx t (kt,_) gl =
     let ise, u = mk_tpattern env0 sigma0 (ise,EConstr.Unsafe.to_constr t) all_ok L2R (EConstr.Unsafe.to_constr t) in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
-    (fun env c _ h -> 
+    (fun env c _ h ->
       try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c)))
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of "
         ++ pr_econstr_pat env sigma0 t ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
-    (fun () -> try end_T () with 
-      | NoMatch when easy -> fake_pmatcher_end () 
+    (fun () -> try end_T () with
+      | NoMatch when easy -> fake_pmatcher_end ()
       | NoMatch -> anomaly "unfoldintac")
-  | _ -> 
+  | _ ->
     (fun env (c as orig_c) _ h ->
       if const then
-        let rec aux c = 
+        let rec aux c =
           match EConstr.kind sigma0 c with
           | Const _ when EConstr.eq_constr sigma0 c t -> body env t t
           | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
@@ -282,15 +282,15 @@ let unfoldintac occ rdx t (kt,_) gl =
         with _ -> errorstrm Pp.(str "The term " ++
           pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_econstr_pat env sigma t)),
     fake_pmatcher_end in
-  let concl = 
+  let concl =
     let concl0 = EConstr.Unsafe.to_constr concl0 in
-    try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) 
+    try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold))
     with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in
   let _ = conclude () in
   Proofview.V82.of_tactic (convert_concl ~check:true concl) gl
 ;;
 
-let foldtac occ rdx ft gl = 
+let foldtac occ rdx ft gl =
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let sigma, t = ft in
   let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
@@ -303,7 +303,7 @@ let foldtac occ rdx ft gl =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in
     (fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c),
     (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ())
-  | _ -> 
+  | _ ->
     (fun env c _ h ->
        try
          let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in
@@ -371,12 +371,12 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   in
   ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
   ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
-  try refine_with 
+  try refine_with
     ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl
-  with _ -> 
+  with _ ->
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
-    | App (hd, args) -> 
+    | App (hd, args) ->
         let hd_ty = Retyping.get_type_of env sigma hd in
         let names = let rec aux t = function 0 -> [] | n ->
           let t = Reductionops.whd_all env sigma t in
@@ -409,7 +409,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
 (*         ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
         ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
   let cvtac, rwtac, gl =
-    if EConstr.Vars.closed0 (project gl) r' then 
+    if EConstr.Vars.closed0 (project gl) r' then
       let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
@@ -417,14 +417,14 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
       | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
-      | _ -> 
+      | _ ->
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
           let gl = pf_merge_uc_of sigma gl in
           Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl
     else
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
-      let r3, _, r3t  = 
+      let r3, _, r3t  =
         try EConstr.destCast (project gl) r2 with _ ->
         errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (snd sr)
                     ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
@@ -471,7 +471,7 @@ let ssr_is_setoid env =
   | None -> fun _ _ _ -> false
   | Some srel ->
   fun sigma r args ->
-    Rewrite.is_applied_rewrite_relation env 
+    Rewrite.is_applied_rewrite_relation env
       sigma [] (EConstr.mkApp (r, args)) <> None
 
 let closed0_check cl p gl =
@@ -585,7 +585,7 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
         sigma, pats @ [pat] in
       let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
       let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in
-      (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), 
+      (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i),
       fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx
   | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) ->
       let r = ref None in
@@ -633,7 +633,7 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt)
   let interp gc gl =
     try interp_term ist gl gc
     with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
-  let rwtac gl = 
+  let rwtac gl =
     let rx = Option.map (interp_rpattern gl) grx in
     let gl = match rx with
       | None -> gl
@@ -672,6 +672,6 @@ let unlocktac ist args gl =
   let locked, gl = pf_mkSsrConst "locked" gl in
   let key, gl = pf_mkSsrConst "master_key" gl in
   let ktacs = [
-    (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); 
+    (fun gl -> unfoldtac None None (project gl,locked) xInParens gl);
     Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in
   tclTHENLIST (List.map utac args @ ktacs) gl
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index b0f56c423f..f486d1e457 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -42,7 +42,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
     (mkRHole, Some body), ist) pty in
   let pat = interp_cpattern gl pat pty in
   let cl, sigma, env = pf_concl gl, project gl, pf_env gl in
-  let (c, ucst), cl = 
+  let (c, ucst), cl =
     let cl = EConstr.Unsafe.to_constr cl in
     try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
     with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in
@@ -77,8 +77,8 @@ let () =
     })
 
 
-open Constrexpr 
-open Glob_term 
+open Constrexpr
+open Glob_term
 
 let combineCG t1 t2 f g = match t1, t2 with
  | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
@@ -96,7 +96,7 @@ let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
 
 let havetac ist
   (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
-  suff namefst gl 
+  suff namefst gl
 =
  let concl = pf_concl gl in
  let pats = tclCompileIPats orig_pats in
@@ -195,7 +195,7 @@ let havetac ist
    | _,false,true ->
      let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
      gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c
-   | _, false, false -> 
+   | _, false, false ->
      let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
      gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac
    | _, true, false -> assert false in
@@ -260,7 +260,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
          | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
     c, args, pired c args, pf_merge_uc uc gl in
   let tacipat pats = introstac pats in
-  let tacigens = 
+  let tacigens =
     Tacticals.tclTHEN
       (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0])))
       (introstac (List.fold_right mkpats gens [])) in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index a1f707ffa8..22325f3fc3 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -167,7 +167,7 @@ let pr_name = function Name id -> pr_id id | Anonymous -> str "_"
 let pr_spc () = str " "
 let pr_list = prlist_with_sep
 
-(**************************** ssrhyp **************************************) 
+(**************************** ssrhyp **************************************)
 
 let pr_ssrhyp _ _ _ = pr_hyp
 
@@ -279,7 +279,7 @@ let negate_parser f tok x =
   let rc = try Some (f tok x) with Stream.Failure -> None in
   match rc with
   | None -> ()
-  | Some _ -> raise Stream.Failure 
+  | Some _ -> raise Stream.Failure
 
 let test_not_ssrslashnum =
   Pcoq.Entry.of_parser
@@ -612,10 +612,10 @@ let ipat_of_intro_pattern p = Tactypes.(
     | IntroAction IntroWildcard -> IPatAnon Drop
     | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
       IPatCase (Regular(
-       List.map (List.map ipat_of_intro_pattern) 
- 	 (List.map (List.map remove_loc) iorpat)))
+       List.map (List.map ipat_of_intro_pattern)
+         (List.map (List.map remove_loc) iorpat)))
     | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
-      IPatCase 
+      IPatCase
        (Regular [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)])
     | IntroNaming IntroAnonymous -> IPatAnon (One None)
     | IntroAction (IntroRewrite b) -> IPatRewrite (allocc, if b then L2R else R2L)
@@ -688,7 +688,7 @@ let rec add_intro_pattern_hyps ipat hyps =
   | IntroAction (IntroRewrite _) -> hyps
   | IntroAction (IntroInjection ips) -> List.fold_right add_intro_pattern_hyps ips hyps
   | IntroAction (IntroApplyOn (c,pat)) -> add_intro_pattern_hyps pat hyps
-  | IntroForthcoming _ -> 
+  | IntroForthcoming _ ->
     (* As in ipat_of_intro_pattern, was unable to determine which kind
       of ipat interp_introid could return [HH] *) assert false
 
@@ -890,12 +890,12 @@ let check_ssrhpats loc w_binders ipats =
   let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in
   let clr, ipats =
     let opt_app = function None -> fun l -> Some l
-      | Some l1 -> fun l2 -> Some (l1 @ l2) in 
+      | Some l1 -> fun l2 -> Some (l1 @ l2) in
     let rec aux clr = function
       | IPatClear cl :: tl -> aux (opt_app clr cl) tl
       | tl -> clr, tl
     in aux None ipats in
-  let simpl, ipats = 
+  let simpl, ipats =
     match List.rev ipats with
     | IPatSimpl _ as s :: tl -> [s], List.rev tl
     | _ -> [],  ipats in
@@ -906,7 +906,7 @@ let check_ssrhpats loc w_binders ipats =
       | [] -> ipat, []
       | ( IPatId _| IPatAnon _| IPatCase _ | IPatDispatch _ | IPatRewrite _ as i) :: tl ->
         if w_binders then
-          if simpl <> [] && tl <> [] then 
+          if simpl <> [] && tl <> [] then
             err_loc(str"binders XOR s-item allowed here: "++pr_ipats(tl@simpl))
           else if not (List.for_all (function IPatId _ -> true | _ -> false) tl)
           then err_loc (str "Only binders allowed here: " ++ pr_ipats tl)
@@ -939,7 +939,7 @@ ARGUMENT EXTEND ssrhpats_wtransp
   | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) }
 END
 
-ARGUMENT EXTEND ssrhpats_nobs 
+ARGUMENT EXTEND ssrhpats_nobs
 TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats }
   | [ ssripats(i) ] -> { check_ssrhpats loc false i }
 END
@@ -1019,7 +1019,7 @@ GRAMMAR EXTEND Gram
   ssrfwdid: [[ test_ssrfwdid; id = Prim.ident -> { id } ]];
   END
 
-  
+
 (* by *)
 (** Tactical arguments. *)
 
@@ -1109,7 +1109,7 @@ END
 open Ssrmatching_plugin.Ssrmatching
 open Ssrmatching_plugin.G_ssrmatching
 
-let pr_wgen = function 
+let pr_wgen = function
   | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id
   | (clr, Some((id,k),Some p)) ->
       spc() ++ pr_clear mt clr ++ str"(" ++ str k ++ pr_hoi id ++ str ":=" ++
@@ -1152,7 +1152,7 @@ let pr_ssrclausehyps _ _ _ = pr_clausehyps
 
 }
 
-ARGUMENT EXTEND ssrclausehyps 
+ARGUMENT EXTEND ssrclausehyps
 TYPED AS ssrwgen list PRINTED BY { pr_ssrclausehyps }
 | [ ssrwgen(hyp) "," ssrclausehyps(hyps) ] -> { hyp :: hyps }
 | [ ssrwgen(hyp) ssrclausehyps(hyps) ] -> { hyp :: hyps }
@@ -1163,7 +1163,7 @@ END
 
 (* type ssrclauses = ssrahyps * ssrclseq *)
 
-let pr_clauses (hyps, clseq) = 
+let pr_clauses (hyps, clseq) =
   if clseq = InGoal then mt ()
   else str "in " ++ pr_clausehyps hyps ++ pr_clseq clseq
 let pr_ssrclauses _ _ _ = pr_clauses
@@ -1215,7 +1215,7 @@ let rec format_local_binders h0 bl0 = match h0, bl0 with
   | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl ->
     Bdef (x, oty, v) :: format_local_binders h bl
   | _ -> []
-  
+
 let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } ->
     let bs, c' = format_constr_expr h c in
@@ -1228,11 +1228,11 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
     Bdef (x, oty, v) :: bs, c'
   | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
     [Bcast t], c
-  | BFrec (has_str, has_cast) :: h, 
+  | BFrec (has_str, has_cast) :: h,
     { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
     let bs = format_local_binders h bl in
     let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
-    bs @ bstr @ (if has_cast then [Bcast t] else []), c 
+    bs @ bstr @ (if has_cast then [Bcast t] else []), c
   | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } ->
     format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
   | _, c ->
@@ -1516,7 +1516,7 @@ END
 
 {
 
-let intro_id_to_binder = List.map (function 
+let intro_id_to_binder = List.map (function
   | IPatId id ->
       let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
@@ -1687,7 +1687,7 @@ let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
 
 }
 
-GRAMMAR EXTEND Gram 
+GRAMMAR EXTEND Gram
   GLOBAL: Prim.ident;
   Prim.ident: [[ s = IDENT; ssr_null_entry -> { ssr_id_of_string loc s } ]];
 END
@@ -1756,8 +1756,8 @@ END
 {
 
 let ssrautoprop gl =
-  try 
-    let tacname = 
+  try
+    let tacname =
       try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
       with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
     let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
@@ -2168,7 +2168,7 @@ let pr_ssraarg _ _ _ (view, (dgens, ipats)) =
 
 }
 
-ARGUMENT EXTEND ssrapplyarg 
+ARGUMENT EXTEND ssrapplyarg
 TYPED AS (ssrbwdview * (ssragens * ssrintros))
 PRINTED BY { pr_ssraarg }
 | [ ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] ->
@@ -2567,7 +2567,7 @@ ARGUMENT EXTEND ssrwlogfwd TYPED AS (ssrwgen list * ssrfwd)
 | [ ":" ssrwgen_list(gens) "/" ast_closure_lterm(t) ] -> { gens, mkFwdHint "/" t}
 END
 
-        
+
 TACTIC EXTEND ssrwlog
 | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
   { V82.tactic (wlogtac ist pats fwd hint false `NoGen) }
@@ -2589,13 +2589,13 @@ TACTIC EXTEND ssrwithoutloss
 END
 
 TACTIC EXTEND ssrwithoutlosss
-| [ "without" "loss" "suff" 
+| [ "without" "loss" "suff"
     ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
   { V82.tactic (wlogtac ist pats fwd hint true `NoGen) }
 END
 
 TACTIC EXTEND ssrwithoutlossss
-| [ "without" "loss" "suffices" 
+| [ "without" "loss" "suffices"
     ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]->
   { V82.tactic (wlogtac ist pats fwd hint true `NoGen) }
 END
@@ -2627,7 +2627,7 @@ let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma
 
 GRAMMAR EXTEND Gram
   GLOBAL: ssr_idcomma;
-  ssr_idcomma: [ [ test_idcomma; 
+  ssr_idcomma: [ [ test_idcomma;
     ip = [ id = IDENT -> { Some (Id.of_string id) } | "_" -> { None } ]; "," ->
     { Some ip }
   ] ];
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index e4df7399e1..240b1a5476 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -17,7 +17,7 @@ val pp_term :
 
 val pr_spc : unit -> Pp.t
 val pr_bar : unit -> Pp.t
-val pr_list : 
+val pr_list :
   (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
 
 val pp_concat :
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index cd2448d764..0fc05f58d3 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -109,7 +109,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
     EConstr.mkLetIn ({na with binder_name=Name (orig_id id)}, unmark v, unmark t, unmark c')
   | _ -> EConstr.map (project gl) unmark c in
   let utac hyp =
-    Proofview.V82.of_tactic 
+    Proofview.V82.of_tactic
      (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.map_constr unmark hyp)) in
   let utacs = List.map utac (pf_hyps gl) in
   let ugtac gl' =
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 064ea0a3e3..9f6fe0e651 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -104,7 +104,7 @@ GRAMMAR EXTEND Gram
     [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
       { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
     | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
-      { let b1, ct, rt = db1 in 
+      { let b1, ct, rt = db1 in
       let b1, b2 = let open CAst in
         let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
         (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
@@ -147,7 +147,7 @@ END
 
 let declare_one_prenex_implicit locality f =
   let fref =
-    try Smartlocate.global_with_alias f 
+    try Smartlocate.global_with_alias f
     with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
   let rec loop = function
   | a :: args' when Impargs.is_status_implicit a ->
@@ -340,7 +340,7 @@ END
 
 (* Main type conclusion pattern filter *)
 
-let rec splay_search_pattern na = function 
+let rec splay_search_pattern na = function
   | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp
   | Pattern.PLetIn (_, _, _, bp) -> splay_search_pattern na bp
   | Pattern.PRef hr -> hr, na
@@ -364,11 +364,11 @@ let coerce_search_pattern_to_sort hpat =
   if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
   let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
   let warn () =
-    Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ 
+    Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++
       pr_constr_pattern_env env sigma hpat') in
   if EConstr.isSort sigma ht then begin warn (); true, hpat' end else
   let filter_head, coe_path =
-    try 
+    try
       let _, cp =
         Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
       warn ();