plugin that compiles with 8.5

6 files changed, 98 insertions, 207 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 931570d..7fa256f 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -66,6 +66,9 @@ open Notation_ops
 open Locus
 open Locusops
 
+open Compat
+open Tok
+
 open Ssrmatching
 
 
@@ -862,7 +865,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let evplist = 
     let depev = List.fold_left (fun evs (_,(_,t,_)) -> 
         Intset.union evs (Evarutil.undefined_evars_of_term sigma t)) Intset.empty evlist in
-    List.filter (fun i,(_,_,b) -> b && Intset.mem i depev) evlist in
+    List.filter (fun (i,(_,_,b)) -> b && Intset.mem i depev) evlist in
   let evlist, evplist, sigma = 
     if evplist = [] then evlist, [], sigma else
     List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) ->
@@ -1835,14 +1838,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
 
 let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
-let id_of_Cterm t = match id_of_cpattern t with
-  | Some x -> x
-  | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here"
-let ssrhyp_of_ssrterm = function
-  | k, (_, Some c) as o ->
-     SsrHyp (constr_loc c, id_of_Cterm (cpattern_of_term o)), String.make 1 k
-  | _, (_, None) -> assert false
-
 (* terms *)
 let pr_ssrterm _ _ _ = pr_term
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
@@ -2006,7 +2001,7 @@ let check_wgen_uniq gens =
   check [] ids
 
 let pf_clauseids gl gens clseq =
-  let keep_clears = List.map (fun x, _ -> x, None) in
+  let keep_clears = List.map (fun (x, _) -> x, None) in
   if gens <> [] then (check_wgen_uniq gens; gens) else
   if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else
   Errors.error "assumptions should be named explicitly"
@@ -2640,7 +2635,7 @@ END
 let reject_ssrhid strm =
   match Compat.get_tok (stream_nth 0 strm) with
   | Tok.KEYWORD "[" ->
-      (match Compat.get_tok (stream_nth 0 strm) with
+      (match Compat.get_tok (stream_nth 1 strm) with
       | Tok.KEYWORD ":" -> raise Stream.Failure
       | _ -> ())
   | _ -> ()
@@ -3160,7 +3155,7 @@ let check_seqtacarg dir arg = match snd arg, dir with
     loc_error loc "expected \"first\""
   | _, _ -> arg
 
-let ssrorelse = Gram.Entry.create "ssrorelse"
+let ssrorelse = Gram.entry_create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
@@ -3697,10 +3692,12 @@ ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg
 END
 
 let viewmovetac_aux clear name_ref (_, vl as v) _ gen ist gl =
-  let cl, c, clr, gl = pf_interp_gen ist gl false gen in
+  let cl, c, clr, gl, gen_pat =
+    let _, gen_pat, a, b, c, ucst = pf_interp_gen_aux ist gl false gen in
+    a, b ,c, pf_merge_uc ucst gl, gen_pat in
   let cl, c, gl = if vl = [] then cl, c, gl else pf_with_view ist gl v cl c in
   let clr = if clear then clr else [] in
-  name_ref := (match id_of_cpattern (snd gen) with Some id -> id | _ -> top_id);
+  name_ref := (match id_of_pattern gen_pat with Some id -> id | _ -> top_id);
   genclrtac cl [c] clr gl
 
 let () = move_top_with_view := 
@@ -5763,7 +5760,8 @@ let ssrabstract ist gens (*last*) gl =
     let fire gl t = Reductionops.nf_evar (project gl) t in
     let abstract, gl = pf_mkSsrConst "abstract" gl in
     let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
-    let id = mkVar (Option.get (id_of_cpattern cid)) in
+    let cid_interpreted = interp_cpattern ist gl cid None in
+    let id = mkVar (Option.get (id_of_pattern cid_interpreted)) in
     let idty, args_id = examine_abstract id gl in
     let abstract_n = args_id.(1) in
     let abstract_proof = pf_find_abstract_proof true gl abstract_n in 
@@ -5807,7 +5805,7 @@ let ssrabstract ist gens (*last*) gl =
   in
   let introback ist (gens, _) =
     introstac ~ist
-      (List.map (fun (_,cp) -> match id_of_cpattern cp with
+      (List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern ist gl cp None) with
         | None -> IpatAnon
         | Some id -> IpatId id)
         (List.tl (List.hd gens))) in
@@ -6058,9 +6056,6 @@ END
 
 (** Canonical Structure alias *)
 
-let def_body : Vernacexpr.definition_expr Gram.Entry.e = Obj.magic
-   (Grammar.Entry.find (Obj.magic gallina_ext) "vernac:def_body") in
-
 GEXTEND Gram
   GLOBAL: gallina_ext;
 
@@ -6071,7 +6066,7 @@ GEXTEND Gram
       | IDENT "Canonical"; ntn = Prim.by_notation ->
 	  Vernacexpr.VernacCanonical (ByNotation ntn)
       | IDENT "Canonical"; qid = Constr.global;
-          d = def_body ->
+          d = G_vernac.def_body ->
           let s = coerce_reference_to_id qid in
 	  Vernacexpr.VernacDefinition
 	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
@@ -6093,18 +6088,11 @@ END
 (* Coq v8.3 defines "by" as a keyword, some hacks are not needed any   *)
 (* longer and thus comment out. Such comments are marked with v8.3     *)
 
-let tac_ent = List.fold_left Grammar.Entry.find (Obj.magic simple_tactic) in
-let hypident_ent =
-  tac_ent ["clause_dft_all"; "in_clause"; "hypident_occ"; "hypident"] in
-let id_or_meta : Obj.t Gram.Entry.e = Obj.magic
-   (Grammar.Entry.find hypident_ent "id_or_meta") in
-let hypident : (Obj.t * hyp_location_flag) Gram.Entry.e =
-   Obj.magic hypident_ent in
 GEXTEND Gram
-  GLOBAL: hypident;
-hypident: [
-  [ "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id, InHypTypeOnly
-  | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id, InHypValueOnly
+  GLOBAL: Tactic.hypident;
+  Tactic.hypident: [
+  [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly
+  | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly
   ] ];
 END
 
@@ -6118,13 +6106,9 @@ hloc: [
   ] ];
 END
 
-let constr_eval
- : (Constrexpr.constr_expr,Obj.t,Obj.t) Genredexpr.may_eval Gram.Entry.e
- = Obj.magic (Grammar.Entry.find (Obj.magic constr_may_eval) "constr_eval")
- 
 GEXTEND Gram
-  GLOBAL: constr_eval;
-  constr_eval: [
+  GLOBAL: Tactic.constr_eval;
+  Tactic.constr_eval: [
     [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ]
   ];
 END
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index 29580a6..cb791ca 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
@@ -1059,6 +1059,10 @@ let interp_pattern ist gl red redty =
 let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;;
 let interp_rpattern ist gl red = interp_pattern ist gl red None;;
 
+let id_of_pattern = function
+  | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None)
+  | _ -> None
+
 (* The full occurrence set *)
 let noindex = Some(false,[])
 
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
index b355dc1..58ee875 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
@@ -3,6 +3,7 @@
 open Genarg
 open Tacexpr
 open Environ
+open Tacmach
 open Evd
 open Proof_type
 open Term
@@ -60,7 +61,7 @@ val redex_of_pattern :
 (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
 val interp_rpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   rpattern ->
     pattern
 
@@ -68,7 +69,7 @@ val interp_rpattern :
     in the current [Ltac] interpretation signature [ise] and tactic input [gl].
     [ty] is an optional type for the redex of [cpat] *)
 val interp_cpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   cpattern -> glob_constr_and_expr option ->
     pattern
 
@@ -191,8 +192,7 @@ val mk_tpattern_matcher :
 (* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns
  * the conclusion of [gl] where [occ] occurrences of [t] have been replaced
  * by [Rel 1] and the instance of [t] *)
-val pf_fill_occ_term :
-  goal Tacmach.sigma -> occ -> evar_map * constr -> constr * constr
+val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr
 
 (* It may be handy to inject a simple term into the first form of cpattern *)
 val cpattern_of_term : char * glob_constr_and_expr -> cpattern
@@ -215,13 +215,13 @@ val assert_done : 'a option ref -> 'a
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map
-val pf_unify_HO : goal Tacmach.sigma -> constr -> constr -> goal Tacmach.sigma
+val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma
 
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
 val tag_of_cpattern : cpattern -> char
 val loc_of_cpattern : cpattern -> Loc.t
-val id_of_cpattern : cpattern -> Names.variable option
+val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
 val cpattern_of_id : Names.variable -> cpattern
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index f598c21..d9a2581 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -66,6 +66,9 @@ open Notation_ops
 open Locus
 open Locusops
 
+open Compat
+open Tok
+
 open Ssrmatching
 
 
@@ -862,7 +865,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let evplist = 
     let depev = List.fold_left (fun evs (_,(_,t,_)) -> 
         Intset.union evs (Evarutil.undefined_evars_of_term sigma t)) Intset.empty evlist in
-    List.filter (fun i,(_,_,b) -> b && Intset.mem i depev) evlist in
+    List.filter (fun (i,(_,_,b)) -> b && Intset.mem i depev) evlist in
   let evlist, evplist, sigma = 
     if evplist = [] then evlist, [], sigma else
     List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) ->
@@ -1829,14 +1832,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
 
 let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
-let id_of_Cterm t = match id_of_cpattern t with
-  | Some x -> x
-  | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here"
-let ssrhyp_of_ssrterm = function
-  | k, (_, Some c) as o ->
-     SsrHyp (constr_loc c, id_of_Cterm (cpattern_of_term o)), String.make 1 k
-  | _, (_, None) -> assert false
-
 (* terms *)
 let pr_ssrterm _ _ _ = pr_term
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
@@ -2000,7 +1995,7 @@ let check_wgen_uniq gens =
   check [] ids
 
 let pf_clauseids gl gens clseq =
-  let keep_clears = List.map (fun x, _ -> x, None) in
+  let keep_clears = List.map (fun (x, _) -> x, None) in
   if gens <> [] then (check_wgen_uniq gens; gens) else
   if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else
   Errors.error "assumptions should be named explicitly"
@@ -2634,7 +2629,7 @@ END
 let reject_ssrhid strm =
   match Compat.get_tok (stream_nth 0 strm) with
   | Tok.KEYWORD "[" ->
-      (match Compat.get_tok (stream_nth 0 strm) with
+      (match Compat.get_tok (stream_nth 1 strm) with
       | Tok.KEYWORD ":" -> raise Stream.Failure
       | _ -> ())
   | _ -> ()
@@ -3154,7 +3149,7 @@ let check_seqtacarg dir arg = match snd arg, dir with
     loc_error loc "expected \"first\""
   | _, _ -> arg
 
-let ssrorelse = Gram.Entry.create "ssrorelse"
+let ssrorelse = Gram.entry_create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
@@ -3691,10 +3686,12 @@ ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg
 END
 
 let viewmovetac_aux clear name_ref (_, vl as v) _ gen ist gl =
-  let cl, c, clr, gl = pf_interp_gen ist gl false gen in
+  let cl, c, clr, gl, gen_pat =
+    let _, gen_pat, a, b, c, ucst = pf_interp_gen_aux ist gl false gen in
+    a, b ,c, pf_merge_uc ucst gl, gen_pat in
   let cl, c, gl = if vl = [] then cl, c, gl else pf_with_view ist gl v cl c in
   let clr = if clear then clr else [] in
-  name_ref := (match id_of_cpattern (snd gen) with Some id -> id | _ -> top_id);
+  name_ref := (match id_of_pattern gen_pat with Some id -> id | _ -> top_id);
   genclrtac cl [c] clr gl
 
 let () = move_top_with_view := 
@@ -4636,7 +4633,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
@@ -4674,8 +4671,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)),
@@ -4683,7 +4680,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
@@ -4721,10 +4718,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
@@ -4889,7 +4886,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 rwprocess_rule dir rule gl =
+let rwrxtac occ rdx_pat dir rule gl =
   let env = pf_env gl in
   let coq_prod = lz_coq_prod () in
   let is_setoid = ssr_is_setoid env in
@@ -4960,13 +4957,7 @@ let rwprocess_rule 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
-    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
+    loop dir sigma r t [] 0 in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
@@ -4991,11 +4982,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
-      (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), 
+      find_R ~k:(fun _ _ h -> mkRel h), 
       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
@@ -5008,32 +4999,6 @@ 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 _ = 
@@ -5789,7 +5754,8 @@ let ssrabstract ist gens (*last*) gl =
     let fire gl t = Reductionops.nf_evar (project gl) t in
     let abstract, gl = pf_mkSsrConst "abstract" gl in
     let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
-    let id = mkVar (Option.get (id_of_cpattern cid)) in
+    let cid_interpreted = interp_cpattern ist gl cid None in
+    let id = mkVar (Option.get (id_of_pattern cid_interpreted)) in
     let idty, args_id = examine_abstract id gl in
     let abstract_n = args_id.(1) in
     let abstract_proof = pf_find_abstract_proof true gl abstract_n in 
@@ -5833,7 +5799,7 @@ let ssrabstract ist gens (*last*) gl =
   in
   let introback ist (gens, _) =
     introstac ~ist
-      (List.map (fun (_,cp) -> match id_of_cpattern cp with
+      (List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern ist gl cp None) with
         | None -> IpatAnon
         | Some id -> IpatId id)
         (List.tl (List.hd gens))) in
@@ -6084,9 +6050,6 @@ END
 
 (** Canonical Structure alias *)
 
-let def_body : Vernacexpr.definition_expr Gram.Entry.e = Obj.magic
-   (Grammar.Entry.find (Obj.magic gallina_ext) "vernac:def_body") in
-
 GEXTEND Gram
   GLOBAL: gallina_ext;
 
@@ -6097,7 +6060,7 @@ GEXTEND Gram
       | IDENT "Canonical"; ntn = Prim.by_notation ->
 	  Vernacexpr.VernacCanonical (ByNotation ntn)
       | IDENT "Canonical"; qid = Constr.global;
-          d = def_body ->
+          d = G_vernac.def_body ->
           let s = coerce_reference_to_id qid in
 	  Vernacexpr.VernacDefinition
 	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
@@ -6119,18 +6082,11 @@ END
 (* Coq v8.3 defines "by" as a keyword, some hacks are not needed any   *)
 (* longer and thus comment out. Such comments are marked with v8.3     *)
 
-let tac_ent = List.fold_left Grammar.Entry.find (Obj.magic simple_tactic) in
-let hypident_ent =
-  tac_ent ["clause_dft_all"; "in_clause"; "hypident_occ"; "hypident"] in
-let id_or_meta : Obj.t Gram.Entry.e = Obj.magic
-   (Grammar.Entry.find hypident_ent "id_or_meta") in
-let hypident : (Obj.t * hyp_location_flag) Gram.Entry.e =
-   Obj.magic hypident_ent in
 GEXTEND Gram
-  GLOBAL: hypident;
-hypident: [
-  [ "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id, InHypTypeOnly
-  | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id, InHypValueOnly
+  GLOBAL: Tactic.hypident;
+  Tactic.hypident: [
+  [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly
+  | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly
   ] ];
 END
 
@@ -6144,13 +6100,9 @@ hloc: [
   ] ];
 END
 
-let constr_eval
- : (Constrexpr.constr_expr,Obj.t,Obj.t) Genredexpr.may_eval Gram.Entry.e
- = Obj.magic (Grammar.Entry.find (Obj.magic constr_may_eval) "constr_eval")
- 
 GEXTEND Gram
-  GLOBAL: constr_eval;
-  constr_eval: [
+  GLOBAL: Tactic.constr_eval;
+  Tactic.constr_eval: [
     [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ]
   ];
 END
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index 2fd0fe6..cb791ca 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -619,7 +619,7 @@ let match_upats_FO upats env sigma0 ise c =
 ;;
 
 
-let match_upats_HO ~on_instance upats env sigma0 ise c =
+let match_upats_HO 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
@@ -648,7 +648,7 @@ let match_upats_HO ~on_instance 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
-        on_instance (ungen_upat lhs pt' u)
+        raise (FoundUnif (ungen_upat lhs pt' u))
       with FoundUnif _ as sigma_u -> raise sigma_u 
       | NoProgress -> it_did_match := true
       | _ -> () in
@@ -661,8 +661,8 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
  if !it_did_match then raise NoProgress
 
 let prof_HO = mk_profiler "match_upats_HO";;
-let match_upats_HO ~on_instance upats env sigma0 ise c =
-  prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c
+let match_upats_HO upats env sigma0 ise c =
+  prof_HO.profile (match_upats_HO upats env sigma0) ise c
 ;;
 
 
@@ -675,14 +675,7 @@ 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")
 
-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 subst = Environ.env -> Term.constr -> int -> Term.constr
 type find_P = 
   Environ.env -> Term.constr -> int ->
   k:subst ->
@@ -691,7 +684,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 ?(all_instances=false)
+let mk_tpattern_matcher
   ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats)
 =
   let nocc = ref 0 and skip_occ = ref false in
@@ -734,35 +727,13 @@ 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
-      if not all_instances then match_upats_FO upats env sigma0 ise c;
-      match_upats_HO ~on_instance upats env sigma0 ise c;
+      match_upats_FO upats env sigma0 ise c;
+      match_upats_HO upats env sigma0 ise c;
       raise NoMatch
-    with FoundUnif sigma_u -> 0,[sigma_u]
-    | (NoMatch|NoProgress) when all_instances && instances () <> [] ->
-      0, uniquize (instances ())
+    with FoundUnif sigma_u -> sigma_u
     | NoMatch when (not raise_NoMatch) ->
       errorstrm (source () ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
@@ -771,11 +742,9 @@ let rec uniquize = function
         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) =
-    if all_instances then assert_done_multires upat_that_matched
-    else List.hd (snd(assert_done upat_that_matched)) in
+  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
+  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' =
@@ -784,7 +753,7 @@ let rec uniquize = function
     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 fa1 h else fa1 in
+      let f' = if subst_occ () then k env u.up_t h else fa1 in
       mkApp (f', Array.map_left (subst_loop acc) a2)
     else
       (* TASSI: clear letin values to avoid unfolding *)
@@ -795,7 +764,7 @@ let rec uniquize = function
 ((fun () ->
   let sigma, uc, ({up_f = pf; up_a = pa} as u) =
     match !upat_that_matched with
-    | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch
+    | Some x -> 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)
@@ -1090,6 +1059,10 @@ let interp_pattern ist gl red redty =
 let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;;
 let interp_rpattern ist gl red = interp_pattern ist gl red None;;
 
+let id_of_pattern = function
+  | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None)
+  | _ -> None
+
 (* The full occurrence set *)
 let noindex = Some(false,[])
 
@@ -1112,7 +1085,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 concl0 1
+  | None -> do_subst env0 concl0 1
   | Some (sigma, (T rp | In_T rp)) -> 
     let rp = fs sigma rp in
     let ise = create_evar_defs sigma in
@@ -1131,7 +1104,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 
@@ -1147,10 +1120,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
@@ -1164,13 +1137,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 e_body h))) in
+        do_subst env e_body h))) in
     let _ = end_X () in let _ = end_TE () in
     concl
 ;;
@@ -1186,7 +1159,7 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
 
 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);
+    (fun env c h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context);
                      mkRel (h'+h-1)),
     (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
@@ -1204,7 +1177,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
 
@@ -1259,27 +1232,6 @@ 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 e8b4d81..58ee875 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
@@ -3,6 +3,7 @@
 open Genarg
 open Tacexpr
 open Environ
+open Tacmach
 open Evd
 open Proof_type
 open Term
@@ -60,7 +61,7 @@ val redex_of_pattern :
 (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
 val interp_rpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   rpattern ->
     pattern
 
@@ -68,7 +69,7 @@ val interp_rpattern :
     in the current [Ltac] interpretation signature [ise] and tactic input [gl].
     [ty] is an optional type for the redex of [cpat] *)
 val interp_cpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   cpattern -> glob_constr_and_expr option ->
     pattern
 
@@ -76,9 +77,9 @@ val interp_cpattern :
  *  to signal the complement of this set (i.e. {-1 3}) *)
 type occ = (bool * int list) option
 
-(** [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
+(** Substitution function. The [int] argument is the number of binders
+    traversed so far *)
+type subst = env -> 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 
@@ -119,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_p ok p_origin dir t] compiles a term [t] 
+(** [mk_tpattern env sigma0 sigma_t ok p_origin dir p] 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.
@@ -160,7 +161,6 @@ 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 ->
@@ -192,8 +192,7 @@ val mk_tpattern_matcher :
 (* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns
  * the conclusion of [gl] where [occ] occurrences of [t] have been replaced
  * by [Rel 1] and the instance of [t] *)
-val pf_fill_occ_term :
-  goal Tacmach.sigma -> occ -> evar_map * constr -> constr * constr
+val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr
 
 (* It may be handy to inject a simple term into the first form of cpattern *)
 val cpattern_of_term : char * glob_constr_and_expr -> cpattern
@@ -216,13 +215,13 @@ val assert_done : 'a option ref -> 'a
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map
-val pf_unify_HO : goal Tacmach.sigma -> constr -> constr -> goal Tacmach.sigma
+val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma
 
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
 val tag_of_cpattern : cpattern -> char
 val loc_of_cpattern : cpattern -> Loc.t
-val id_of_cpattern : cpattern -> Names.variable option
+val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
 val cpattern_of_id : Names.variable -> cpattern