Merge branch 'master' of https://github.com/math-comp/math-comp

6 files changed, 390 insertions, 143 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 0e04221..e05526e 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -44,6 +44,7 @@ open Coqlib
 open Glob_term
 open Util
 open Evd
+open Sigma.Notations
 open Extend
 open Goptions
 open Tacexpr
@@ -563,7 +564,9 @@ let pf_partial_solution gl t evl =
 
 let pf_new_evar gl ty =
   let sigma, env, it = project gl, pf_env gl, sig_it gl in
-  let sigma, extra = Evarutil.new_evar env sigma ty in
+  let sigma = Sigma.Unsafe.of_evar_map sigma in
+  let Sigma (extra, sigma, _) = Evarutil.new_evar env sigma ty in
+  let sigma = Sigma.to_evar_map sigma in
   re_sig it sigma, extra
 
 (* Basic tactics *)
@@ -1040,10 +1043,7 @@ let ssrtac_expr = ssrtac_atom
 
 
 let ssrevaltac ist gtac =
-  let debug = match TacStore.get ist.extra f_debug with
-  | None -> Tactic_debug.DebugOff | Some level -> level
-  in
-  Proofview.V82.of_tactic (interp_tac_gen ist.lfun [] debug (globTacticIn (fun _ -> gtac)))
+  Proofview.V82.of_tactic (eval_tactic_ist ist gtac)
 
 (* fun gl -> let lfun = [tacarg_id, val_interp ist gl gtac] in
   interp_tac_gen lfun [] ist.debug tacarg_expr gl *)
@@ -2397,7 +2397,7 @@ let glob_view_hints lvh =
 
 let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
 
-VERNAC COMMAND EXTEND HintView CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
   |  [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] ->
      [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ]
 END
@@ -2873,23 +2873,33 @@ let mk_abstract_id () = incr ssr_abstract_id; nat_of_n !ssr_abstract_id
 
 let ssrmkabs id gl =
   let env, concl = pf_env gl, pf_concl gl in
-  let step sigma =
+  let step = { run = begin fun sigma ->
+    let sigma = Sigma.to_evar_map sigma in
     let sigma, abstract_proof, abstract_ty =
       let sigma, (ty, _) =
         Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
       let sigma, ablock = mkSsrConst "abstract_lock" env sigma in
-      let sigma, lock = Evarutil.new_evar env sigma ablock in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (lock, sigma, _) = Evarutil.new_evar env sigma ablock in
+      let sigma = Sigma.to_evar_map sigma in
       let sigma, abstract = mkSsrConst "abstract" env sigma in
       let abstract_ty = mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
-      let sigma, m = Evarutil.new_evar env sigma abstract_ty in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (m, sigma, _) = Evarutil.new_evar env sigma abstract_ty in
+      let sigma = Sigma.to_evar_map sigma in
       sigma, m, abstract_ty in
     let sigma, kont =
       let rd = Name id, None, abstract_ty in
-      Evarutil.new_evar (Environ.push_rel rd env) sigma concl in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (ev, sigma, _) = Evarutil.new_evar (Environ.push_rel rd env) sigma concl in
+      let sigma = Sigma.to_evar_map sigma in
+      (sigma, ev)
+    in
     pp(lazy(pr_constr concl));
     let term = mkApp (mkLambda(Name id,abstract_ty,kont) ,[|abstract_proof|]) in
     let sigma, _ = Typing.type_of env sigma term in
-    sigma, term in
+    Sigma.Unsafe.of_pair (term, sigma)
+  end } in
   Proofview.V82.of_tactic
     (Proofview.tclTHEN
       (Tactics.New.refine step)
@@ -3304,7 +3314,7 @@ let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t =
        let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
        sigma, Evarutil.nf_evar sigma ct in
   let n, c, abstracted_away, ucst = pf_abs_evars gl t in
-  List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst
+  List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst, n
 
 let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    let n_binders = ref 0 in
@@ -3368,9 +3378,12 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
       (mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma 
   else match kind_of_type ty with
   | ProdType (_, src, tgt) ->
-      let sigma, x =
-        Evarutil.new_evar env (create_evar_defs sigma)
-          (if bi_types then Reductionops.nf_betaiota sigma src else src) in
+      let sigma = create_evar_defs sigma in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (x, sigma, _) =
+        Evarutil.new_evar env sigma
+          (if bi_types then Reductionops.nf_betaiota (Sigma.to_evar_map sigma) src else src) in
+      let sigma = Sigma.to_evar_map sigma in
       loop (subst1 x tgt) ((m - n,x) :: args) sigma (n-1)
   | CastType (t, _) -> loop t args sigma n 
   | LetInType (_, v, _, t) -> loop (subst1 v t) args sigma n
@@ -3381,7 +3394,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
         (Reductionops.whd_betadeltaiota env sigma) ty in
       match kind_of_type ty with
       | ProdType _ -> loop ty args sigma n
-      | _ -> anomaly "saturate did not find enough products"
+      | _ -> raise NotEnoughProducts
   in
    loop ty [] sigma m
 
@@ -3904,7 +3917,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
   | _ -> false in
   let match_pat env p occ h cl = 
     let sigma0 = project orig_gl in
-    pp(lazy(str"matching: " ++ pp_pattern p));
+    pp(lazy(str"matching: " ++ pr_occ occ ++ pp_pattern p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in
     pp(lazy(str"     got: " ++ pr_constr c));
@@ -3924,6 +3937,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
        with e when Errors.noncritical e -> p in
   (* finds the eliminator applies it to evars and c saturated as needed  *)
   (* obtaining "elim ??? (c ???)". pred is the higher order evar         *)
+  (* cty is None when the user writes _ (hence we can't make a pattern *)
   let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl =
     match elim with
     | Some elim ->
@@ -3934,7 +3948,15 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in
-      None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
+      let cty, gl =
+        if Option.is_empty oc then None, gl
+        else
+          let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
+          let pc = match c_gen with
+            | Some p -> interp_cpattern (Option.get ist) orig_gl p None 
+            | _ -> mkTpat gl c in
+          Some(c, c_ty, pc), gl in
+      cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
     | None ->
       let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
       let ((kn, i) as ind, _ as indu), unfolded_c_ty =
@@ -3945,8 +3967,11 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           let t, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
           gl, t
         else
-          pf_eapply (fun env sigma ->
-            Indrec.build_case_analysis_scheme env sigma indu true) gl sort in
+          pf_eapply (fun env sigma () ->
+            let sigma = Sigma.Unsafe.of_evar_map sigma in
+            let Sigma (ind, sigma, _) = Indrec.build_case_analysis_scheme env sigma indu true sort in
+            let sigma = Sigma.to_evar_map sigma in
+            (sigma, ind)) gl () in
       let gl, elimty = pf_type_of gl elim in
       let pred_id,n_elim_args,is_rec,elim_is_dep,n_pred_args =
         analyze_eliminator elimty env (project gl) in
@@ -3964,7 +3989,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
   pp(lazy(str"elim= "++ pr_constr_pat elim));
-  pp(lazy(str"elimty= "++ pr_constr elimty));
+  pp(lazy(str"elimty= "++ pr_constr_pat elimty));
   let inf_deps_r = match kind_of_type elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -3973,11 +3998,17 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in
       let gl' = f c c_ty gl in
       Some (c, c_ty, gl, gl')
-    with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in
-  let elim_is_dep, gl = match cty with
-    | None -> true, gl
+    with
+    | NotEnoughProducts -> None
+    | e when Errors.noncritical e -> loop (n+1) in loop 0 in
+  (* Here we try to understand if the main pattern/term the user gave is
+   * the first pattern to be matched (i.e. if elimty ends in P t1 .. tn,
+   * weather tn is the t the user wrote in 'elim: t' *)
+  let c_is_head_p, gl = match cty with
+    | None -> true, gl  (* The user wrote elim: _ *)
     | Some (c, c_ty, _) ->
     let res = 
+      (* we try to see if c unifies with the last arg of elim *)
       if elim_is_dep then None else
       let arg = List.assoc (n_elim_args - 1) elim_args in
       let gl, arg_ty = pf_type_of gl arg in
@@ -3988,21 +4019,22 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
     match res with
     | Some x -> x
     | None ->
+      (* we try to see if c unifies with the last inferred pattern *)
       let inf_arg = List.hd inf_deps_r in
       let gl, inf_arg_ty = pf_type_of gl inf_arg in
       match saturate_until gl c c_ty (fun _ c_ty gl ->
               pf_unify_HO gl c_ty inf_arg_ty) with
       | Some (c, _, _,gl) -> true, gl
       | None ->
-	errorstrm (str"Unable to apply the eliminator to the term"++
-      spc()++pr_constr c++spc()++str"or to unify it's type with"++
-      pr_constr inf_arg_ty) in
-  pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep));
+        errorstrm (str"Unable to apply the eliminator to the term"++
+          spc()++pr_constr c++spc()++str"or to unify it's type with"++
+          pr_constr inf_arg_ty) in
+  pp(lazy(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pf_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
    * the type of the elimination principle *)
-  let pp_pat (_,p,_,_) = pp_pattern p in
+  let pp_pat (_,p,_,occ) = pr_occ occ ++ pp_pattern p in
   let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
@@ -4018,12 +4050,12 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           loop (patterns @ [i, p, inf_t, occ]) 
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps -> 
-          pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c));
+          pp(lazy(str"adding inf pattern " ++ pr_constr_pat c));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm (str "Too many dependent abstractions") in
-    let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with
-    | `EConstr _, _, None -> anomaly "Simple welim with no term"
+    let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with
+    | `EConstr _, _, None -> anomaly "Simple elim with no term"
     | _, false, _ -> deps, [], inf_deps_r
     | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r
     | _, true, Some (c, _, pc) ->
@@ -4083,7 +4115,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           let erefl, gl = mkRefl t c gl in
           let erefl = fire_subst gl erefl in
           apply_type new_concl [erefl], gl in
-        let rel = k + if elim_is_dep then 1 else 0 in
+        let rel = k + if c_is_head_p then 1 else 0 in
         let src, gl = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) gl in
         let concl = mkArrow src (lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
@@ -4461,7 +4493,10 @@ let newssrcongrtac arg ist gl =
     | 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, x = Evarutil.new_evar env (create_evar_defs sigma) ty in
+    let sigma = create_evar_defs sigma in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (x, sigma, _) = Evarutil.new_evar env sigma ty in
+    let sigma = Sigma.to_evar_map sigma in
     x, re_sig si sigma in
   let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
   let ssr_congr lr = mkApp (arr, lr) in
@@ -4649,7 +4684,7 @@ END
 let simplintac occ rdx sim gl = 
   let simptac gl = 
     let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
-    let simp env c _ = red_safe Tacred.simpl env sigma0 c in
+    let simp env c _ _ = red_safe Tacred.simpl env sigma0 c in
     Proofview.V82.of_tactic
       (convert_concl_no_check (eval_pattern env0 sigma0 concl0 rdx occ simp))
       gl in
@@ -4687,8 +4722,8 @@ let unfoldintac occ rdx t (kt,_) gl =
     let ise, u = mk_tpattern env0 sigma0 (ise,t) all_ok L2R t in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
-    (fun env c h -> 
-      try find_T env c h (fun env c _ -> body env t c)
+    (fun env c _ h -> 
+      try find_T env c h (fun env c _ _ -> body env t c)
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm (str"No occurrence of "
         ++ pr_constr_pat t ++ spc() ++ str "in " ++ pr_constr c)),
@@ -4696,7 +4731,7 @@ let unfoldintac occ rdx t (kt,_) gl =
       | NoMatch when easy -> fake_pmatcher_end () 
       | NoMatch -> anomaly "unfoldintac")
   | _ -> 
-    (fun env (c as orig_c) h ->
+    (fun env (c as orig_c) _ h ->
       if const then
           let rec aux c = 
             match kind_of_term c with
@@ -4734,10 +4769,10 @@ let foldtac occ rdx ft gl =
     let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in
-    (fun env c h -> try find_T env c h (fun env t _ -> t) with NoMatch -> c),
+    (fun env c _ h -> try find_T env c h (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 c t in fs sigma t
+    (fun env c _ h -> try let sigma = unify_HO env sigma c t in fs sigma t
     with _ -> errorstrm (str "fold pattern " ++ pr_constr_pat t ++ spc ()
       ++ str "does not match redex " ++ pr_constr_pat c)), 
     fake_pmatcher_end in
@@ -4773,7 +4808,11 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   let beta = Reductionops.clos_norm_flags Closure.beta env sigma in
   let sigma, p = 
     let sigma = create_evar_defs sigma in
-    Evarutil.new_evar env sigma (beta (subst1 new_rdx pred)) in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma (beta (subst1 new_rdx pred)) in
+    let sigma = Sigma.to_evar_map sigma in
+    (sigma, ev)
+  in
   let pred = mkNamedLambda pattern_id rdx_ty pred in
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
@@ -4902,7 +4941,7 @@ let closed0_check cl p gl =
   if closed0 cl then
     errorstrm (str"No occurrence of redex "++pf_pr_constr gl (project gl) p)
 
-let rwrxtac occ rdx_pat dir rule gl =
+let rwprocess_rule dir rule gl =
   let env = pf_env gl in
   let coq_prod = lz_coq_prod () in
   let is_setoid = ssr_is_setoid env in
@@ -4914,7 +4953,10 @@ let rwrxtac occ rdx_pat dir rule gl =
       pp(lazy(str"rewrule="++pr_constr t));
       match kind_of_term t with
       | Prod (_, xt, at) ->
-        let ise, x = Evarutil.new_evar env (create_evar_defs sigma) xt in
+        let sigma = create_evar_defs sigma in
+        let sigma = Sigma.Unsafe.of_evar_map sigma in
+        let Sigma (x, sigma, _) = Evarutil.new_evar env sigma xt in
+        let ise = Sigma.to_evar_map sigma in
         loop d ise (mkApp (r, [|x|])) (subst1 x at) rs 0
       | App (pr, a) when is_ind_ref pr coq_prod.Coqlib.typ ->
         let sr sigma = match kind_of_term (Tacred.hnf_constr env sigma r) with
@@ -4973,7 +5015,13 @@ let rwrxtac occ rdx_pat dir rule gl =
         in
     let sigma, r = rule in
     let t = Retyping.get_type_of env sigma r in
-    loop dir sigma r t [] 0 in
+    loop dir sigma r t [] 0
+  in
+    r_sigma, rules
+
+let rwrxtac occ rdx_pat dir rule gl =
+  let env = pf_env gl in
+  let r_sigma, rules = rwprocess_rule dir rule gl in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
@@ -4998,11 +5046,11 @@ let rwrxtac 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
-      find_R ~k:(fun _ _ h -> mkRel h), 
+      (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
-      (fun env c h -> do_once r (fun () -> find_rule c, c); mkRel h),
+      (fun env c _ h -> do_once r (fun () -> find_rule c, c); mkRel h),
       (fun concl -> closed0_check concl e gl; assert_done r) in
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
@@ -5015,6 +5063,32 @@ let rwrxtac occ rdx_pat dir rule gl =
   prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
 ;;
 
+let ssrinstancesofrule ist dir arg gl =
+  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
+  let rule = interp_term ist gl arg in
+  let r_sigma, rules = rwprocess_rule dir rule gl in
+  let find, conclude =
+    let upats_origin = dir, snd rule in
+    let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
+      let sigma, pat =
+        mk_tpattern env sigma0 (sigma,r) (rw_progress rhs) d lhs in
+      sigma, pats @ [pat] in
+    let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
+    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  ppnl (str"BEGIN INSTANCES");
+  try
+    while true do
+      ignore(find env0 concl0 1 ~k:print)
+    done; raise NoMatch
+  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+
+TACTIC EXTEND ssrinstofruleL2R
+| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist L2R arg) ]
+END
+TACTIC EXTEND ssrinstofruleR2L
+| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist R2L arg) ]
+END
 
 (* Resolve forward reference *)
 let _ = 
@@ -5496,7 +5570,7 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
 END
 
 let ssrposetac ist (id, (_, t)) gl =
-  let sigma, t, ucst = pf_abs_ssrterm ist gl t in
+  let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in
   posetac id t (pf_merge_uc ucst gl)
 
 
@@ -5654,7 +5728,7 @@ let unfold cl =
     (List.map (fun c -> F.fCONST (fst (destConst c))) cl @ [F.fBETA; F.fIOTA])))
 
 let havegentac ist t gl =
-  let sigma, c, ucst = pf_abs_ssrterm ist gl t in
+  let sigma, c, ucst, _ = pf_abs_ssrterm ist gl t in
   let gl = pf_merge_uc ucst gl in
   let gl, cty = pf_type_of gl c in
   apply_type (mkArrow cty (pf_concl gl)) [c] gl
@@ -5710,7 +5784,7 @@ let havetac ist
      errorstrm (str"Suff have does not accept a proof term")
    | FwdHave, false, true ->
      let cty = combineCG cty hole (mkCArrow loc) mkRArrow in
-     let _, t, uc = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
+     let _,t,uc,_ = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
      let gl = pf_merge_uc uc gl in
      let gl, ty = pf_type_of gl t in
      let ctx, _ = decompose_prod_n 1 ty in
@@ -5726,8 +5800,12 @@ let havetac ist
      let skols_args =
        List.map (fun id -> examine_abstract (mkVar id) gl) skols in
      let gl = List.fold_right unlock_abs skols_args gl in
-     let sigma, t, uc =
+     let sigma, t, uc, n_evars =
        interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
+     if skols <> [] && n_evars <> 0 then
+       Errors.error ("Automatic generalization of unresolved implicit "^
+                     "arguments together with abstract variables is "^
+                     "not supported");
      let gl = re_sig (sig_it gl) (Evd.merge_universe_context sigma uc) in
      let gs =
        List.map (fun (_,a) ->
@@ -5938,7 +6016,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       List.fold_left (fun (env, c) _ ->
         let rd, c = destProd_or_LetIn c in
         Environ.push_rel rd env, c) (pf_env gl, c) gens in
-    let sigma, ev = Evarutil.new_evar env (project gl) Term.mkProp in
+    let sigma = project gl in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma Term.mkProp in
+    let sigma = Sigma.to_evar_map sigma in
     let k, _ = Term.destEvar ev in
     let fake_gl = {Evd.it = k; Evd.sigma = sigma} in
     let _, ct, _, uc = pf_interp_ty ist fake_gl ct in
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index effd193..aa44fec 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
@@ -621,7 +621,7 @@ let match_upats_FO upats env sigma0 ise c =
 ;;
 
 
-let match_upats_HO upats env sigma0 ise c =
+let match_upats_HO ~on_instance upats env sigma0 ise c =
  let it_did_match = ref false in
  let rec aux upats env sigma0 ise c =
   let f, a = splay_app ise c in let i0 = ref (-1) in
@@ -650,7 +650,7 @@ let match_upats_HO upats env sigma0 ise c =
         let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in
         let lhs = mkSubApp f i a in
         let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in
-        raise (FoundUnif (ungen_upat lhs pt' u))
+        on_instance (ungen_upat lhs pt' u)
       with FoundUnif _ as sigma_u -> raise sigma_u 
       | NoProgress -> it_did_match := true
       | _ -> () in
@@ -663,8 +663,8 @@ let match_upats_HO upats env sigma0 ise c =
  if !it_did_match then raise NoProgress
 
 let prof_HO = mk_profiler "match_upats_HO";;
-let match_upats_HO upats env sigma0 ise c =
-  prof_HO.profile (match_upats_HO upats env sigma0) ise c
+let match_upats_HO ~on_instance upats env sigma0 ise c =
+  prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c
 ;;
 
 
@@ -677,7 +677,14 @@ let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
 let assert_done r = 
   match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called")
 
-type subst = Environ.env -> Term.constr -> int -> Term.constr
+let assert_done_multires r = 
+  match !r with
+  | None -> Errors.anomaly (str"do_once never called")
+  | Some (n, xs) ->
+      r := Some (n+1,xs);
+      try List.nth xs n with Failure _ -> raise NoMatch
+
+type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr
 type find_P = 
   Environ.env -> Term.constr -> int ->
   k:subst ->
@@ -686,7 +693,7 @@ type conclude = unit ->
   Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * Term.constr)
 
 (* upats_origin makes a better error message only            *)
-let mk_tpattern_matcher
+let mk_tpattern_matcher ?(all_instances=false)
   ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats)
 =
   let nocc = ref 0 and skip_occ = ref false in
@@ -729,13 +736,35 @@ let source () = match upats_origin, upats with
       pr_constr_pat rule ++ spc()
   | _, [] | None, _::_::_ ->
       Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
+let on_instance, instances =
+  let instances = ref [] in
+  (fun x ->
+    if all_instances then instances := !instances @ [x]
+    else raise (FoundUnif x)),
+  (fun () -> !instances) in
+let rec uniquize = function
+  | [] -> []
+  | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs ->
+    let t = Reductionops.nf_evar sigma t in
+    let f = Reductionops.nf_evar sigma f in
+    let a = Array.map (Reductionops.nf_evar sigma) a in
+    let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) =
+      let t1 = Reductionops.nf_evar sigma1 t1 in
+      let f1 = Reductionops.nf_evar sigma1 f1 in
+      let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in
+      not (Term.eq_constr t t1 &&
+           Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in
+    x :: uniquize (List.filter neq xs) in
+
 ((fun env c h ~k -> 
   do_once upat_that_matched (fun () -> 
     try
-      match_upats_FO upats env sigma0 ise c;
-      match_upats_HO upats env sigma0 ise c;
+      if not all_instances then match_upats_FO upats env sigma0 ise c;
+      match_upats_HO ~on_instance upats env sigma0 ise c;
       raise NoMatch
-    with FoundUnif sigma_u -> sigma_u
+    with FoundUnif sigma_u -> 0,[sigma_u]
+    | (NoMatch|NoProgress) when all_instances && instances () <> [] ->
+      0, uniquize (instances ())
     | NoMatch when (not raise_NoMatch) ->
       errorstrm (source () ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
@@ -744,9 +773,11 @@ let source () = match upats_origin, upats with
         errorstrm (str"all matches of "++source()++
           str"are equal to the " ++ pr_dir_side (inv_dir dir))
     | NoProgress -> raise NoMatch);
-  let sigma, _, ({up_f = pf; up_a = pa} as u) = assert_done upat_that_matched in
-  pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma));
-  if !skip_occ then (ignore(k env u.up_t 0); c) else
+  let sigma, _, ({up_f = pf; up_a = pa} as u) =
+    if all_instances then assert_done_multires upat_that_matched
+    else List.hd (snd(assert_done upat_that_matched)) in
+(*   pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *)
+  if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else
   let match_EQ = match_EQ env sigma u in
   let pn = Array.length pa in
   let rec subst_loop (env,h as acc) c' =
@@ -755,7 +786,7 @@ let source () = match upats_origin, upats with
     if Array.length a >= pn && match_EQ f && unif_EQ_args env sigma pa a then
       let a1, a2 = Array.chop (Array.length pa) a in
       let fa1 = mkApp (f, a1) in
-      let f' = if subst_occ () then k env u.up_t h else fa1 in
+      let f' = if subst_occ () then k env u.up_t fa1 h else fa1 in
       mkApp (f', Array.map_left (subst_loop acc) a2)
     else
       (* TASSI: clear letin values to avoid unfolding *)
@@ -766,7 +797,7 @@ let source () = match upats_origin, upats with
 ((fun () ->
   let sigma, uc, ({up_f = pf; up_a = pa} as u) =
     match !upat_that_matched with
-    | Some x -> x | None when raise_NoMatch -> raise NoMatch
+    | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch
     | None -> Errors.anomaly (str"companion function never called") in
   let p' = mkApp (pf, pa) in
   if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
@@ -815,7 +846,7 @@ let pr_pattern_aux pr_constr = function
   | E_As_X_In_T (e,x,t) ->
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
 let pp_pattern (sigma, p) =
-  pr_pattern_aux (fun t -> pr_constr (pi3 (nf_open_term sigma sigma t))) p
+  pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
@@ -1088,7 +1119,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in
     sigma, [pat] in
   match pattern with
-  | None -> do_subst env0 concl0 1
+  | None -> do_subst env0 concl0 concl0 1
   | Some (sigma, (T rp | In_T rp)) -> 
     let rp = fs sigma rp in
     let ise = create_evar_defs sigma in
@@ -1107,7 +1138,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     (* we start from sigma, so hole is considered a rigid head *)
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in
-    let concl = find_T env0 concl0 1 (fun env c h ->
+    let concl = find_T env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
       fs p_sigma (find_X env (fs sigma p) h 
@@ -1123,10 +1154,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_X, end_X = mk_tpattern_matcher sigma noindex holep in
     let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in
     let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in
-    let concl = find_T env0 concl0 1 (fun env c h ->
+    let concl = find_T env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c h ->
+      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
         find_E env e_body h do_subst))) in
     let _ = end_E () in let _ = end_X () in let _ = end_T () in
     concl
@@ -1140,13 +1171,13 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher sigma occ holep in
-    let concl = find_TE env0 concl0 1 (fun env c h ->
+    let concl = find_TE env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c h ->
+      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
         let e_sigma = unify_HO env sigma e_body e in
         let e_body = fs e_sigma e in
-        do_subst env e_body h))) in
+        do_subst env e_body e_body h))) in
     let _ = end_X () in let _ = end_TE () in
     concl
 ;;
@@ -1161,9 +1192,13 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
   Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma
 
 let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
-  let find_R, conclude = let r = ref None in
-    (fun env c h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context);
-                     mkRel (h'+h-1)),
+  let do_make_rel, occ =
+    if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in
+  let find_R, conclude =
+    let r = ref None in
+    (fun env c _ h' ->
+       do_once r (fun () -> c, Evd.empty_evar_universe_context);
+       if do_make_rel then mkRel (h'+h-1) else c),
     (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in
   let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in
   let e = conclude cl in
@@ -1180,7 +1215,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in
  let find_U, end_U =
    mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
- let concl = find_U env concl h (fun _ _ -> mkRel) in
+ let concl = find_U env concl h (fun _ _ _ -> mkRel) in
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, p, concl, rdx
 
@@ -1238,6 +1273,27 @@ TACTIC EXTEND ssrat
 | [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ]
 END
 
+let ssrinstancesof ist arg gl =
+  let ok rhs lhs ise = true in
+(*   not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *)
+  let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
+  let sigma0, cpat = interp_cpattern ist gl arg None in
+  let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in
+  let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in
+  let find, conclude =
+    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true
+      sigma None (etpat,[tpat]) in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  ppnl (str"BEGIN INSTANCES");
+  try
+    while true do
+      ignore(find env concl 1 ~k:print)
+    done; raise NoMatch
+  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+
+TACTIC EXTEND ssrinstoftpat
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ]
+END
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
index 0976be7..b7d8d18 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
@@ -77,9 +77,9 @@ val interp_cpattern :
  *  to signal the complement of this set (i.e. {-1 3}) *)
 type occ = (bool * int list) option
 
-(** Substitution function. The [int] argument is the number of binders
-    traversed so far *)
-type subst = env -> constr -> int -> constr
+(** [subst e p t i]. [i] is the number of binders
+    traversed so far, [p] the term from the pattern, [t] the matched one *)
+type subst = env -> constr -> constr -> int -> constr
 
 (** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every
     [occ] occurrence of [pat]. The [int] argument is the number of 
@@ -120,7 +120,7 @@ val pr_dir_side : ssrdir -> Pp.std_ppcmds
 (** a pattern for a term with wildcards *)
 type tpattern
 
-(** [mk_tpattern env sigma0 sigma_t ok p_origin dir p] compiles a term [t] 
+(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] 
     living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern].
     The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok]
     callback is used to filter occurrences.
@@ -161,6 +161,7 @@ type conclude =
     be passed to tune the [UserError] eventually raised (useful if the 
     pattern is coming from the LHS/RHS of an equation) *)
 val mk_tpattern_matcher :
+  ?all_instances:bool ->
   ?raise_NoMatch:bool ->
   ?upats_origin:ssrdir * constr ->
   evar_map -> occ -> evar_map * tpattern list ->
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index e6636cb..20fd720 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -2391,7 +2391,7 @@ let glob_view_hints lvh =
 
 let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
 
-VERNAC COMMAND EXTEND HintView CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
   |  [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] ->
      [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ]
 END
@@ -3298,7 +3298,7 @@ let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t =
        let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
        sigma, Evarutil.nf_evar sigma ct in
   let n, c, abstracted_away, ucst = pf_abs_evars gl t in
-  List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst
+  List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst, n
 
 let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    let n_binders = ref 0 in
@@ -3375,7 +3375,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
         (Reductionops.whd_betadeltaiota env sigma) ty in
       match kind_of_type ty with
       | ProdType _ -> loop ty args sigma n
-      | _ -> anomaly "saturate did not find enough products"
+      | _ -> raise NotEnoughProducts
   in
    loop ty [] sigma m
 
@@ -3898,7 +3898,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
   | _ -> false in
   let match_pat env p occ h cl = 
     let sigma0 = project orig_gl in
-    pp(lazy(str"matching: " ++ pp_pattern p));
+    pp(lazy(str"matching: " ++ pr_occ occ ++ pp_pattern p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in
     pp(lazy(str"     got: " ++ pr_constr c));
@@ -3918,6 +3918,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
        with e when Errors.noncritical e -> p in
   (* finds the eliminator applies it to evars and c saturated as needed  *)
   (* obtaining "elim ??? (c ???)". pred is the higher order evar         *)
+  (* cty is None when the user writes _ (hence we can't make a pattern *)
   let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl =
     match elim with
     | Some elim ->
@@ -3928,7 +3929,15 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in
-      None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
+      let cty, gl =
+        if Option.is_empty oc then None, gl
+        else
+          let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
+          let pc = match c_gen with
+            | Some p -> interp_cpattern (Option.get ist) orig_gl p None 
+            | _ -> mkTpat gl c in
+          Some(c, c_ty, pc), gl in
+      cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
     | None ->
       let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
       let ((kn, i) as ind, _ as indu), unfolded_c_ty =
@@ -3958,7 +3967,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
   pp(lazy(str"elim= "++ pr_constr_pat elim));
-  pp(lazy(str"elimty= "++ pr_constr elimty));
+  pp(lazy(str"elimty= "++ pr_constr_pat elimty));
   let inf_deps_r = match kind_of_type elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -3967,11 +3976,17 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in
       let gl' = f c c_ty gl in
       Some (c, c_ty, gl, gl')
-    with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in
-  let elim_is_dep, gl = match cty with
-    | None -> true, gl
+    with
+    | NotEnoughProducts -> None
+    | e when Errors.noncritical e -> loop (n+1) in loop 0 in
+  (* Here we try to understand if the main pattern/term the user gave is
+   * the first pattern to be matched (i.e. if elimty ends in P t1 .. tn,
+   * weather tn is the t the user wrote in 'elim: t' *)
+  let c_is_head_p, gl = match cty with
+    | None -> true, gl  (* The user wrote elim: _ *)
     | Some (c, c_ty, _) ->
     let res = 
+      (* we try to see if c unifies with the last arg of elim *)
       if elim_is_dep then None else
       let arg = List.assoc (n_elim_args - 1) elim_args in
       let gl, arg_ty = pf_type_of gl arg in
@@ -3982,21 +3997,22 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
     match res with
     | Some x -> x
     | None ->
+      (* we try to see if c unifies with the last inferred pattern *)
       let inf_arg = List.hd inf_deps_r in
       let gl, inf_arg_ty = pf_type_of gl inf_arg in
       match saturate_until gl c c_ty (fun _ c_ty gl ->
               pf_unify_HO gl c_ty inf_arg_ty) with
       | Some (c, _, _,gl) -> true, gl
       | None ->
-	errorstrm (str"Unable to apply the eliminator to the term"++
-      spc()++pr_constr c++spc()++str"or to unify it's type with"++
-      pr_constr inf_arg_ty) in
-  pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep));
+        errorstrm (str"Unable to apply the eliminator to the term"++
+          spc()++pr_constr c++spc()++str"or to unify it's type with"++
+          pr_constr inf_arg_ty) in
+  pp(lazy(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pf_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
    * the type of the elimination principle *)
-  let pp_pat (_,p,_,_) = pp_pattern p in
+  let pp_pat (_,p,_,occ) = pr_occ occ ++ pp_pattern p in
   let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
@@ -4012,12 +4028,12 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           loop (patterns @ [i, p, inf_t, occ]) 
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps -> 
-          pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c));
+          pp(lazy(str"adding inf pattern " ++ pr_constr_pat c));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm (str "Too many dependent abstractions") in
-    let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with
-    | `EConstr _, _, None -> anomaly "Simple welim with no term"
+    let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with
+    | `EConstr _, _, None -> anomaly "Simple elim with no term"
     | _, false, _ -> deps, [], inf_deps_r
     | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r
     | _, true, Some (c, _, pc) ->
@@ -4077,7 +4093,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           let erefl, gl = mkRefl t c gl in
           let erefl = fire_subst gl erefl in
           apply_type new_concl [erefl], gl in
-        let rel = k + if elim_is_dep then 1 else 0 in
+        let rel = k + if c_is_head_p then 1 else 0 in
         let src, gl = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) gl in
         let concl = mkArrow src (lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
@@ -4643,7 +4659,7 @@ END
 let simplintac occ rdx sim gl = 
   let simptac gl = 
     let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
-    let simp env c _ = red_safe Tacred.simpl env sigma0 c in
+    let simp env c _ _ = red_safe Tacred.simpl env sigma0 c in
     Proofview.V82.of_tactic
       (convert_concl_no_check (eval_pattern env0 sigma0 concl0 rdx occ simp))
       gl in
@@ -4681,8 +4697,8 @@ let unfoldintac occ rdx t (kt,_) gl =
     let ise, u = mk_tpattern env0 sigma0 (ise,t) all_ok L2R t in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
-    (fun env c h -> 
-      try find_T env c h (fun env c _ -> body env t c)
+    (fun env c _ h -> 
+      try find_T env c h (fun env c _ _ -> body env t c)
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm (str"No occurrence of "
         ++ pr_constr_pat t ++ spc() ++ str "in " ++ pr_constr c)),
@@ -4690,7 +4706,7 @@ let unfoldintac occ rdx t (kt,_) gl =
       | NoMatch when easy -> fake_pmatcher_end () 
       | NoMatch -> anomaly "unfoldintac")
   | _ -> 
-    (fun env (c as orig_c) h ->
+    (fun env (c as orig_c) _ h ->
       if const then
           let rec aux c = 
             match kind_of_term c with
@@ -4728,10 +4744,10 @@ let foldtac occ rdx ft gl =
     let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in
-    (fun env c h -> try find_T env c h (fun env t _ -> t) with NoMatch -> c),
+    (fun env c _ h -> try find_T env c h (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 c t in fs sigma t
+    (fun env c _ h -> try let sigma = unify_HO env sigma c t in fs sigma t
     with _ -> errorstrm (str "fold pattern " ++ pr_constr_pat t ++ spc ()
       ++ str "does not match redex " ++ pr_constr_pat c)), 
     fake_pmatcher_end in
@@ -4896,7 +4912,7 @@ let closed0_check cl p gl =
   if closed0 cl then
     errorstrm (str"No occurrence of redex "++pf_pr_constr gl (project gl) p)
 
-let rwrxtac occ rdx_pat dir rule gl =
+let rwprocess_rule dir rule gl =
   let env = pf_env gl in
   let coq_prod = lz_coq_prod () in
   let is_setoid = ssr_is_setoid env in
@@ -4967,7 +4983,13 @@ let rwrxtac occ rdx_pat dir rule gl =
         in
     let sigma, r = rule in
     let t = Retyping.get_type_of env sigma r in
-    loop dir sigma r t [] 0 in
+    loop dir sigma r t [] 0
+  in
+    r_sigma, rules
+
+let rwrxtac occ rdx_pat dir rule gl =
+  let env = pf_env gl in
+  let r_sigma, rules = rwprocess_rule dir rule gl in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
@@ -4992,11 +5014,11 @@ let rwrxtac 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
-      find_R ~k:(fun _ _ h -> mkRel h), 
+      (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
-      (fun env c h -> do_once r (fun () -> find_rule c, c); mkRel h),
+      (fun env c _ h -> do_once r (fun () -> find_rule c, c); mkRel h),
       (fun concl -> closed0_check concl e gl; assert_done r) in
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
@@ -5009,6 +5031,32 @@ let rwrxtac occ rdx_pat dir rule gl =
   prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
 ;;
 
+let ssrinstancesofrule ist dir arg gl =
+  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
+  let rule = interp_term ist gl arg in
+  let r_sigma, rules = rwprocess_rule dir rule gl in
+  let find, conclude =
+    let upats_origin = dir, snd rule in
+    let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
+      let sigma, pat =
+        mk_tpattern env sigma0 (sigma,r) (rw_progress rhs) d lhs in
+      sigma, pats @ [pat] in
+    let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
+    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  ppnl (str"BEGIN INSTANCES");
+  try
+    while true do
+      ignore(find env0 concl0 1 ~k:print)
+    done; raise NoMatch
+  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+
+TACTIC EXTEND ssrinstofruleL2R
+| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist L2R arg) ]
+END
+TACTIC EXTEND ssrinstofruleR2L
+| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist R2L arg) ]
+END
 
 (* Resolve forward reference *)
 let _ = 
@@ -5490,7 +5538,7 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
 END
 
 let ssrposetac ist (id, (_, t)) gl =
-  let sigma, t, ucst = pf_abs_ssrterm ist gl t in
+  let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in
   posetac id t (pf_merge_uc ucst gl)
 
 
@@ -5648,7 +5696,7 @@ let unfold cl =
     (List.map (fun c -> F.fCONST (fst (destConst c))) cl @ [F.fBETA; F.fIOTA])))
 
 let havegentac ist t gl =
-  let sigma, c, ucst = pf_abs_ssrterm ist gl t in
+  let sigma, c, ucst, _ = pf_abs_ssrterm ist gl t in
   let gl = pf_merge_uc ucst gl in
   let gl, cty = pf_type_of gl c in
   apply_type (mkArrow cty (pf_concl gl)) [c] gl
@@ -5704,7 +5752,7 @@ let havetac ist
      errorstrm (str"Suff have does not accept a proof term")
    | FwdHave, false, true ->
      let cty = combineCG cty hole (mkCArrow loc) mkRArrow in
-     let _, t, uc = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
+     let _,t,uc,_ = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
      let gl = pf_merge_uc uc gl in
      let gl, ty = pf_type_of gl t in
      let ctx, _ = decompose_prod_n 1 ty in
@@ -5720,8 +5768,12 @@ let havetac ist
      let skols_args =
        List.map (fun id -> examine_abstract (mkVar id) gl) skols in
      let gl = List.fold_right unlock_abs skols_args gl in
-     let sigma, t, uc =
+     let sigma, t, uc, n_evars =
        interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
+     if skols <> [] && n_evars <> 0 then
+       Errors.error ("Automatic generalization of unresolved implicit "^
+                     "arguments together with abstract variables is "^
+                     "not supported");
      let gl = re_sig (sig_it gl) (Evd.merge_universe_context sigma uc) in
      let gs =
        List.map (fun (_,a) ->
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index c47c946..74f42f6 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -621,7 +621,7 @@ let match_upats_FO upats env sigma0 ise c =
 ;;
 
 
-let match_upats_HO upats env sigma0 ise c =
+let match_upats_HO ~on_instance upats env sigma0 ise c =
  let it_did_match = ref false in
  let rec aux upats env sigma0 ise c =
   let f, a = splay_app ise c in let i0 = ref (-1) in
@@ -650,7 +650,7 @@ let match_upats_HO upats env sigma0 ise c =
         let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in
         let lhs = mkSubApp f i a in
         let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in
-        raise (FoundUnif (ungen_upat lhs pt' u))
+        on_instance (ungen_upat lhs pt' u)
       with FoundUnif _ as sigma_u -> raise sigma_u 
       | NoProgress -> it_did_match := true
       | _ -> () in
@@ -663,8 +663,8 @@ let match_upats_HO upats env sigma0 ise c =
  if !it_did_match then raise NoProgress
 
 let prof_HO = mk_profiler "match_upats_HO";;
-let match_upats_HO upats env sigma0 ise c =
-  prof_HO.profile (match_upats_HO upats env sigma0) ise c
+let match_upats_HO ~on_instance upats env sigma0 ise c =
+  prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c
 ;;
 
 
@@ -677,7 +677,14 @@ let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
 let assert_done r = 
   match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called")
 
-type subst = Environ.env -> Term.constr -> int -> Term.constr
+let assert_done_multires r = 
+  match !r with
+  | None -> Errors.anomaly (str"do_once never called")
+  | Some (n, xs) ->
+      r := Some (n+1,xs);
+      try List.nth xs n with Failure _ -> raise NoMatch
+
+type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr
 type find_P = 
   Environ.env -> Term.constr -> int ->
   k:subst ->
@@ -686,7 +693,7 @@ type conclude = unit ->
   Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * Term.constr)
 
 (* upats_origin makes a better error message only            *)
-let mk_tpattern_matcher
+let mk_tpattern_matcher ?(all_instances=false)
   ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats)
 =
   let nocc = ref 0 and skip_occ = ref false in
@@ -729,13 +736,35 @@ let source () = match upats_origin, upats with
       pr_constr_pat rule ++ spc()
   | _, [] | None, _::_::_ ->
       Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
+let on_instance, instances =
+  let instances = ref [] in
+  (fun x ->
+    if all_instances then instances := !instances @ [x]
+    else raise (FoundUnif x)),
+  (fun () -> !instances) in
+let rec uniquize = function
+  | [] -> []
+  | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs ->
+    let t = Reductionops.nf_evar sigma t in
+    let f = Reductionops.nf_evar sigma f in
+    let a = Array.map (Reductionops.nf_evar sigma) a in
+    let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) =
+      let t1 = Reductionops.nf_evar sigma1 t1 in
+      let f1 = Reductionops.nf_evar sigma1 f1 in
+      let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in
+      not (Term.eq_constr t t1 &&
+           Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in
+    x :: uniquize (List.filter neq xs) in
+
 ((fun env c h ~k -> 
   do_once upat_that_matched (fun () -> 
     try
-      match_upats_FO upats env sigma0 ise c;
-      match_upats_HO upats env sigma0 ise c;
+      if not all_instances then match_upats_FO upats env sigma0 ise c;
+      match_upats_HO ~on_instance upats env sigma0 ise c;
       raise NoMatch
-    with FoundUnif sigma_u -> sigma_u
+    with FoundUnif sigma_u -> 0,[sigma_u]
+    | (NoMatch|NoProgress) when all_instances && instances () <> [] ->
+      0, uniquize (instances ())
     | NoMatch when (not raise_NoMatch) ->
       errorstrm (source () ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
@@ -744,9 +773,11 @@ let source () = match upats_origin, upats with
         errorstrm (str"all matches of "++source()++
           str"are equal to the " ++ pr_dir_side (inv_dir dir))
     | NoProgress -> raise NoMatch);
-  let sigma, _, ({up_f = pf; up_a = pa} as u) = assert_done upat_that_matched in
-  pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma));
-  if !skip_occ then (ignore(k env u.up_t 0); c) else
+  let sigma, _, ({up_f = pf; up_a = pa} as u) =
+    if all_instances then assert_done_multires upat_that_matched
+    else List.hd (snd(assert_done upat_that_matched)) in
+(*   pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *)
+  if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else
   let match_EQ = match_EQ env sigma u in
   let pn = Array.length pa in
   let rec subst_loop (env,h as acc) c' =
@@ -755,7 +786,7 @@ let source () = match upats_origin, upats with
     if Array.length a >= pn && match_EQ f && unif_EQ_args env sigma pa a then
       let a1, a2 = Array.chop (Array.length pa) a in
       let fa1 = mkApp (f, a1) in
-      let f' = if subst_occ () then k env u.up_t h else fa1 in
+      let f' = if subst_occ () then k env u.up_t fa1 h else fa1 in
       mkApp (f', Array.map_left (subst_loop acc) a2)
     else
       (* TASSI: clear letin values to avoid unfolding *)
@@ -766,7 +797,7 @@ let source () = match upats_origin, upats with
 ((fun () ->
   let sigma, uc, ({up_f = pf; up_a = pa} as u) =
     match !upat_that_matched with
-    | Some x -> x | None when raise_NoMatch -> raise NoMatch
+    | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch
     | None -> Errors.anomaly (str"companion function never called") in
   let p' = mkApp (pf, pa) in
   if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
@@ -815,7 +846,7 @@ let pr_pattern_aux pr_constr = function
   | E_As_X_In_T (e,x,t) ->
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
 let pp_pattern (sigma, p) =
-  pr_pattern_aux (fun t -> pr_constr (pi3 (nf_open_term sigma sigma t))) p
+  pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
@@ -1088,7 +1119,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in
     sigma, [pat] in
   match pattern with
-  | None -> do_subst env0 concl0 1
+  | None -> do_subst env0 concl0 concl0 1
   | Some (sigma, (T rp | In_T rp)) -> 
     let rp = fs sigma rp in
     let ise = create_evar_defs sigma in
@@ -1107,7 +1138,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     (* we start from sigma, so hole is considered a rigid head *)
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in
-    let concl = find_T env0 concl0 1 (fun env c h ->
+    let concl = find_T env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
       fs p_sigma (find_X env (fs sigma p) h 
@@ -1123,10 +1154,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_X, end_X = mk_tpattern_matcher sigma noindex holep in
     let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in
     let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in
-    let concl = find_T env0 concl0 1 (fun env c h ->
+    let concl = find_T env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c h ->
+      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
         find_E env e_body h do_subst))) in
     let _ = end_E () in let _ = end_X () in let _ = end_T () in
     concl
@@ -1140,13 +1171,13 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher sigma occ holep in
-    let concl = find_TE env0 concl0 1 (fun env c h ->
+    let concl = find_TE env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c h ->
+      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
         let e_sigma = unify_HO env sigma e_body e in
         let e_body = fs e_sigma e in
-        do_subst env e_body h))) in
+        do_subst env e_body e_body h))) in
     let _ = end_X () in let _ = end_TE () in
     concl
 ;;
@@ -1161,9 +1192,13 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
   Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma
 
 let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
-  let find_R, conclude = let r = ref None in
-    (fun env c h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context);
-                     mkRel (h'+h-1)),
+  let do_make_rel, occ =
+    if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in
+  let find_R, conclude =
+    let r = ref None in
+    (fun env c _ h' ->
+       do_once r (fun () -> c, Evd.empty_evar_universe_context);
+       if do_make_rel then mkRel (h'+h-1) else c),
     (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in
   let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in
   let e = conclude cl in
@@ -1180,7 +1215,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in
  let find_U, end_U =
    mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
- let concl = find_U env concl h (fun _ _ -> mkRel) in
+ let concl = find_U env concl h (fun _ _ _ -> mkRel) in
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, p, concl, rdx
 
@@ -1238,6 +1273,27 @@ TACTIC EXTEND ssrat
 | [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ]
 END
 
+let ssrinstancesof ist arg gl =
+  let ok rhs lhs ise = true in
+(*   not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *)
+  let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
+  let sigma0, cpat = interp_cpattern ist gl arg None in
+  let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in
+  let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in
+  let find, conclude =
+    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true
+      sigma None (etpat,[tpat]) in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  ppnl (str"BEGIN INSTANCES");
+  try
+    while true do
+      ignore(find env concl 1 ~k:print)
+    done; raise NoMatch
+  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+
+TACTIC EXTEND ssrinstoftpat
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ]
+END
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
index 0976be7..b7d8d18 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
@@ -77,9 +77,9 @@ val interp_cpattern :
  *  to signal the complement of this set (i.e. {-1 3}) *)
 type occ = (bool * int list) option
 
-(** Substitution function. The [int] argument is the number of binders
-    traversed so far *)
-type subst = env -> constr -> int -> constr
+(** [subst e p t i]. [i] is the number of binders
+    traversed so far, [p] the term from the pattern, [t] the matched one *)
+type subst = env -> constr -> constr -> int -> constr
 
 (** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every
     [occ] occurrence of [pat]. The [int] argument is the number of 
@@ -120,7 +120,7 @@ val pr_dir_side : ssrdir -> Pp.std_ppcmds
 (** a pattern for a term with wildcards *)
 type tpattern
 
-(** [mk_tpattern env sigma0 sigma_t ok p_origin dir p] compiles a term [t] 
+(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] 
     living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern].
     The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok]
     callback is used to filter occurrences.
@@ -161,6 +161,7 @@ type conclude =
     be passed to tune the [UserError] eventually raised (useful if the 
     pattern is coming from the LHS/RHS of an equation) *)
 val mk_tpattern_matcher :
+  ?all_instances:bool ->
   ?raise_NoMatch:bool ->
   ?upats_origin:ssrdir * constr ->
   evar_map -> occ -> evar_map * tpattern list ->