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

10 files changed, 440 insertions, 144 deletions

diff --git a/mathcomp/ssreflect/descr b/mathcomp/ssreflect/descr
index 7621878..f3aeba5 100644
--- a/mathcomp/ssreflect/descr
+++ b/mathcomp/ssreflect/descr
@@ -3,4 +3,6 @@ Small Scale Reflection
 This library includes the small scale reflection proof language
 extension and the minimal set of libraries to take advantage of it.
 This includes libraries on lists (seq), boolean and boolean
-predicates, natural numbers and types with decidable equality.
+predicates, natural numbers and types with decidable equality,
+finite types, finite sets, finite functions, finite graphs, basic arithmetics
+and prime numbers, big operators
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 ->
diff --git a/mathcomp/ssrtest/abstract_var2.v b/mathcomp/ssrtest/abstract_var2.v
new file mode 100644
index 0000000..5372c5c
--- /dev/null
+++ b/mathcomp/ssrtest/abstract_var2.v
@@ -0,0 +1,16 @@
+Require Import ssreflect.
+
+Set Implicit Arguments.
+
+Axiom P : nat -> nat -> Prop.
+
+Axiom tr :
+  forall x y z, P x y -> P y z -> P x z.
+
+Lemma test a b c : P a c -> P a b.
+Proof.
+intro H.
+Fail have [: s1 s2] H1 : P a b := @tr _ _ _ s1 s2.
+have [: w s1 s2] H1 : P a b := @tr _ w _ s1 s2.
+Abort.
+
diff --git a/mathcomp/ssrtest/derive_inversion.v b/mathcomp/ssrtest/derive_inversion.v
new file mode 100644
index 0000000..71257d8
--- /dev/null
+++ b/mathcomp/ssrtest/derive_inversion.v
@@ -0,0 +1,19 @@
+Require Import ssreflect ssrbool.
+
+Set Implicit Arguments.
+
+  Inductive wf T : bool -> option T -> Type :=
+  | wf_f : wf false None
+  | wf_t : forall x, wf true (Some x).
+
+  Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop.
+
+  Lemma Problem T b (o : option T) :
+    wf b o ->
+    match b with
+    | true  => exists x, o = Some x
+    | false => o = None
+    end.
+  Proof.
+  by case: b; elim/wf_inv=>//;case: o=>// a *; exists a.
+  Qed.
diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v
new file mode 100644
index 0000000..b79453b
--- /dev/null
+++ b/mathcomp/ssrtest/explain_match.v
@@ -0,0 +1,12 @@
+Require Import ssreflect ssrbool ssrnat.
+
+Definition addnAC := (addnA, addnC).
+
+Lemma test x y z : x + y + z =  x + y.
+
+ssrinstancesoftpat (_ + _).
+ssrinstancesofruleL2R addnC.
+ssrinstancesofruleR2L addnA.
+ssrinstancesofruleR2L addnAC.
+Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
+Admitted.
\ No newline at end of file