2 files changed, 10 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
index b24b0a6..eb28351 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
@@ -1025,6 +1025,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/v8.4/ssrmatching.mli b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli
index 4c6bfac..53d2cff 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.mli
@@ -2,6 +2,7 @@
 
 open Genarg
 open Environ
+open Tacmach
 open Evd
 open Proof_type
 open Term
@@ -63,7 +64,7 @@ val redex_of_pattern : ?resolve_typeclasses:bool -> env -> pattern -> constr
 (** [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
 
@@ -71,7 +72,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
 
@@ -208,8 +209,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
@@ -232,13 +232,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 -> Util.loc
-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 rawltacctx : ltacctx