1 files changed, 25 insertions, 25 deletions

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