Merge remote-tracking branch 'upstream/master' into fixdoc

4 files changed, 152 insertions, 1734 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 6d512b1..72161e7 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -1,34 +1,35 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
 (* This line is read by the Makefile's dist target: do not remove. *)
-DECLARE PLUGIN "ssreflect"
+DECLARE PLUGIN "ssreflect_plugin"
 let ssrversion = "1.6";;
 let ssrAstVersion = 1;;
 let () = Mltop.add_known_plugin (fun () ->
   if Flags.is_verbose () && not !Flags.batch_mode then begin
     Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion;
-    Printf.printf "Copyright 2005-2014 Microsoft Corporation and INRIA.\n";
+    Printf.printf "Copyright 2005-2016 Microsoft Corporation and INRIA.\n";
     Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n"
   end)
-  "ssreflect"
+  "ssreflect_plugin"
 ;;
 
 (* Defining grammar rules with "xx" in it automatically declares keywords too,
  * we thus save the lexer to restore it at the end of the file *)
-let frozen_lexer = Lexer.freeze () ;;
+let frozen_lexer = CLexer.freeze () ;;
 
 (*i camlp4use: "pa_extend.cmo" i*)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Names
 open Pp
+open Feedback
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
 open Genarg
 open Stdarg
-open Constrarg
+open Tacarg
 open Term
 open Vars
 open Context
@@ -44,6 +45,7 @@ open Coqlib
 open Glob_term
 open Util
 open Evd
+open Proofview.Notations
 open Sigma.Notations
 open Extend
 open Goptions
@@ -51,7 +53,7 @@ open Tacexpr
 open Tacinterp
 open Pretyping
 open Constr
-open Tactic
+open Pltac
 open Extraargs
 open Ppconstr
 open Printer
@@ -70,8 +72,11 @@ open Locusops
 open Compat
 open Tok
 
+open Ssrmatching_plugin
 open Ssrmatching
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 (* Tentative patch from util.ml *)
 
@@ -95,9 +100,13 @@ module Intset = Evar.Set
 
 type loc = Loc.t
 let dummy_loc = Loc.ghost
-let errorstrm = Errors.errorlabstrm "ssreflect"
-let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg)
-let anomaly s = Errors.anomaly (str s)
+let errorstrm msg = CErrors.user_err ~hdr:"ssreflect" msg
+let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
+let anomaly s = CErrors.anomaly (str s)
+
+(* Compatibility with Coq 8.6 *)
+let ppnl  = msg_info
+let msgnl = msg_info
 
 (** look up a name in the ssreflect internals module *)
 let ssrdirpath = make_dirpath [id_of_string "ssreflect"]
@@ -108,7 +117,7 @@ let locate_reference qid =
 let mkSsrRef name =
   try locate_reference (ssrqid name) with Not_found ->
   try locate_reference (ssrtopqid name) with Not_found ->
-  Errors.error "Small scale reflection library not loaded"
+  CErrors.error "Small scale reflection library not loaded"
 let mkSsrRRef name = GRef (dummy_loc, mkSsrRef name,None), None
 let mkSsrConst name env sigma =
   Sigma.fresh_global env sigma (mkSsrRef name)
@@ -136,13 +145,13 @@ let pf_fresh_global name gl =
 let ssr_loaded = Summary.ref ~name:"SSR:loaded" false
 let is_ssr_loaded () =
   !ssr_loaded ||
-  (if Lexer.is_keyword "SsrSyntax_is_Imported" then ssr_loaded:=true;
+  (if CLexer.is_keyword "SsrSyntax_is_Imported" then ssr_loaded:=true;
    !ssr_loaded)
 
 (* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
 (* or if SsrDebug is Set                                                  *)
 let pp_ref = ref (fun _ -> ())
-let ssr_pp s = pperrnl (str"SSR: "++Lazy.force s)
+let ssr_pp s = msg_error (str"SSR: "++Lazy.force s)
 let _ = try ignore(Sys.getenv "SSRDEBUG"); pp_ref := ssr_pp with Not_found -> ()
 let _ =
   Goptions.declare_bool_option
@@ -209,13 +218,15 @@ let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c
 (** Adding a new uninterpreted generic argument type *)
 let add_genarg tag pr =
   let wit = Genarg.make0 tag in
+  let tag = Geninterp.Val.create tag in
   let glob ist x = (ist, x) in
   let subst _ x = x in
-  let interp ist x = Ftactic.return x in
+  let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
   let gen_pr _ _ _ = pr in
   let () = Genintern.register_intern0 wit glob in
   let () = Genintern.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit interp in
+  let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
   Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
   wit
 
@@ -447,7 +458,7 @@ let mk_profiler s =
 let inVersion = Libobject.declare_object {
   (Libobject.default_object "SSRASTVERSION") with
   Libobject.load_function = (fun _ (_,v) -> 
-    if v <> ssrAstVersion then Errors.error "Please recompile your .vo files");
+    if v <> ssrAstVersion then CErrors.error "Please recompile your .vo files");
   Libobject.classify_function = (fun v -> Libobject.Keep v);
 }
 
@@ -461,7 +472,7 @@ let _ =
       Goptions.optwrite = (fun _ -> 
         Lib.add_anonymous_leaf (inVersion ssrAstVersion)) }
 
-let tactic_expr = Tactic.tactic_expr
+let tactic_expr = Pltac.tactic_expr
 let gallina_ext = Vernac_.gallina_ext 
 let sprintf = Printf.sprintf
 let tactic_mode = G_ltac.tactic_mode
@@ -555,7 +566,7 @@ let is_pf_var c = isVar c && not_section_id (destVar c)
 
 let pf_ids_of_proof_hyps gl =
   let add_hyp decl ids =
-    let id = Named.Declaration.get_id decl in
+    let id = NamedDecl.get_id decl in
     if not_section_id id then id :: ids else ids in
   Context.Named.fold_outside add_hyp (pf_hyps gl) ~init:[]
 
@@ -590,15 +601,15 @@ let apply_type x xs = Proofview.V82.of_tactic (apply_type x xs)
 
 (* we reduce head beta redexes *)
 let betared env = 
-  Closure.create_clos_infos 
-   (Closure.RedFlags.mkflags [Closure.RedFlags.fBETA])
+  CClosure.create_clos_infos 
+   (CClosure.RedFlags.mkflags [CClosure.RedFlags.fBETA])
     env
 ;;
 let introid name = tclTHEN (fun gl ->
    let g, env = pf_concl gl, pf_env gl in
    match kind_of_term g with
    | App (hd, _) when isLambda hd -> 
-     let g = Closure.whd_val (betared env) (Closure.inject g) in
+     let g = CClosure.whd_val (betared env) (CClosure.inject g) in
      Proofview.V82.of_tactic (convert_concl_no_check g) gl
    | _ -> tclIDTAC gl)
   (Proofview.V82.of_tactic (intro_mustbe_force name))
@@ -747,7 +758,7 @@ let mk_anon_id t gl =
 let ssr_anon_hyp = "Hyp"
 
 let anontac decl gl =
-  let id =  match Rel.Declaration.get_name decl with
+  let id =  match RelDecl.get_name decl with
   | Name id ->
     if is_discharged_id id then id else mk_anon_id (string_of_id id) gl
   | _ -> mk_anon_id ssr_anon_hyp gl in
@@ -797,9 +808,9 @@ let pf_abs_evars gl (sigma, c0) =
   let abs_evar n k =
     let evi = Evd.find sigma k in
     let dc = List.firstn n (evar_filtered_context evi) in
-    let abs_dc c decl = match Named.Declaration.to_tuple decl with
-    | x, Some b, t -> mkNamedLetIn x b t (mkArrow t c)
-    | x, None, t -> mkNamedProd x t c in
+    let abs_dc c = function
+    | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c)
+    | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
     let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
     Evarutil.nf_evar sigma t in
   let rec put evlist c = match kind_of_term c with
@@ -852,9 +863,9 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let abs_evar n k =
     let evi = Evd.find sigma k in
     let dc = List.firstn n (evar_filtered_context evi) in
-    let abs_dc c decl = match Named.Declaration.to_tuple decl with
-    | x, Some b, t -> mkNamedLetIn x b t (mkArrow t c)
-    | x, None, t -> mkNamedProd x t c in
+    let abs_dc c = function
+    | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c)
+    | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
     let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
     Evarutil.nf_evar sigma0 (Evarutil.nf_evar sigma t) in
   let rec put evlist c = match kind_of_term c with
@@ -992,10 +1003,10 @@ let pf_unabs_evars gl ise n c0 =
   let push_rel = Environ.push_rel in
   let rec mk_evar j env i c = match kind_of_term c with
   | Prod (x, t, c1) when i < j ->
-    mk_evar j (push_rel (Rel.Declaration.LocalAssum (x, unabs i t)) env) (i + 1) c1
+    mk_evar j (push_rel (RelDecl.LocalAssum (x, unabs i t)) env) (i + 1) c1
   | LetIn (x, b, t, c1) when i < j ->
     let _, _, c2 = destProd c1 in
-    mk_evar j (push_rel (Rel.Declaration.LocalDef (x, unabs i b, unabs i t)) env) (i + 1) c2
+    mk_evar j (push_rel (RelDecl.LocalDef (x, unabs i b, unabs i t)) env) (i + 1) c2
   | _ -> Evarutil.e_new_evar env ise (unabs i c) in
   let rec unabs_evars c =
     if !nev = n then unabs n c else match kind_of_term c with
@@ -1021,7 +1032,7 @@ let pf_unabs_evars gl ise n c0 =
 type ssrargfmt = ArgSsr of string | ArgCoq of argument_type | ArgSep of string
 
 let ssrtac_name name = {
-  mltac_plugin = "ssreflect";
+  mltac_plugin = "ssreflect_plugin";
   mltac_tactic = "ssr" ^ name;
 }
 
@@ -1082,7 +1093,7 @@ let interp_refine ist gl rc =
   let kind = OfType (pf_concl gl) in
   let flags = {
     use_typeclasses = true;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = None;
     fail_evar = false;
     expand_evars = true }
@@ -1128,7 +1139,7 @@ let interp_view_nbimps ist gl rc =
     let si = sig_it gl in
     let gl = re_sig si sigma in
     let pl, c = splay_open_constr gl t in
-    if isAppInd gl c then List.length pl else ~-(List.length pl)
+    if isAppInd gl c then List.length pl else (-(List.length pl))
   with _ -> 0
 
 (* }}} *)
@@ -1212,18 +1223,18 @@ let interp_search_notation loc s opt_scope =
         let ambig = "This string refers to a complex or ambiguous notation." in
         str ambig ++ str "\nTry searching with one of\n" ++ ntns
       with _ -> str "This string is not part of an identifier or notation." in
-    Errors.user_err_loc (loc, "interp_search_notation", diagnosis)
+    CErrors.user_err ~loc ~hdr:"interp_search_notation" diagnosis
 
 let pr_ssr_search_item _ _ _ = pr_search_item
 
 (* Workaround the notation API that can only print notations *)
 
-let is_ident s = try Lexer.check_ident s; true with _ -> false
+let is_ident s = try CLexer.check_ident s; true with _ -> false
 
 let is_ident_part s = is_ident ("H" ^ s)
 
 let interp_search_notation loc tag okey =
-  let err msg = Errors.user_err_loc (loc, "interp_search_notation", msg) in
+  let err msg = CErrors.user_err ~loc ~hdr:"interp_search_notation" msg in
   let mk_pntn s for_key =
     let n = String.length s in
     let s' = String.make (n + 2) ' ' in
@@ -1347,7 +1358,7 @@ let rec splay_search_pattern na = function
   | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp
   | Pattern.PLetIn (_, _, bp) -> splay_search_pattern na bp
   | Pattern.PRef hr -> hr, na
-  | _ -> Errors.error "no head constant in head search pattern"
+  | _ -> CErrors.error "no head constant in head search pattern"
 
 let coerce_search_pattern_to_sort hpat =
   let env = Global.env () and sigma = Evd.empty in
@@ -1358,7 +1369,7 @@ let coerce_search_pattern_to_sort hpat =
   let dc, ht =
     Reductionops.splay_prod env sigma (Universes.unsafe_type_of_global hr) in
   let np = List.length dc in
-  if np < na then Errors.error "too many arguments in head search pattern" else
+  if np < na then CErrors.error "too many arguments in head search pattern" else
   let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
   let warn () =
     msg_warning (str "Listing only lemmas with conclusion matching " ++ 
@@ -1409,7 +1420,7 @@ let interp_search_arg arg =
       try
         let intern = Constrintern.intern_constr_pattern in 
         Search.GlobSearchSubPattern (snd (intern (Global.env()) p))
-      with e -> let e = Errors.push e in iraise (Cerrors.process_vernac_interp_error e)) arg in
+      with e -> let e = CErrors.push e in iraise (ExplainErr.process_vernac_interp_error e)) arg in
   let hpat, a1 = match arg with
   | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a'
   | (true, Search.GlobSearchSubPattern p) :: a' ->
@@ -1444,7 +1455,7 @@ let interp_modloc mr =
   let interp_mod (_, mr) =
     let (loc, qid) = qualid_of_reference mr in
     try Nametab.full_name_module qid with Not_found ->
-    Errors.user_err_loc (loc, "interp_modloc", str "No Module " ++ pr_qualid qid) in
+    CErrors.user_err ~loc ~hdr:"interp_modloc" (str "No Module " ++ pr_qualid qid) in
   let mr_out, mr_in = List.partition fst mr in
   let interp_bmod b = function
   | [] -> fun _ _ _ -> true
@@ -1455,7 +1466,7 @@ let interp_modloc mr =
 (* The unified, extended vernacular "Search" command *)
 
 let ssrdisplaysearch gr env t =
-  let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
+  let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
   msg_info (hov 2 pr_res ++ fnl ())
 
 VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
@@ -1576,7 +1587,7 @@ let donetac gl =
   let tacname = 
     try Nametab.locate_tactic (qualid_of_ident (id_of_string "done"))
     with Not_found -> try Nametab.locate_tactic (ssrqid "done")
-    with Not_found -> Errors.error "The ssreflect library was not loaded" in
+    with Not_found -> CErrors.error "The ssreflect library was not loaded" in
   let tacexpr = dummy_loc, Tacexpr.Reference (ArgArg (dummy_loc, tacname)) in
   Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
 
@@ -1750,7 +1761,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
 let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
 
 let hyp_err loc msg id =
-  Errors.user_err_loc (loc, "ssrhyp", str msg ++ pr_id id)
+  CErrors.user_err ~loc ~hdr:"ssrhyp" (str msg ++ pr_id id)
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
   let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in
@@ -1862,8 +1873,8 @@ ARGUMENT EXTEND ssrterm
      PRINTED BY pr_ssrterm
      INTERPRETED BY interp_ssrterm
      GLOBALIZED BY glob_ssrterm SUBSTITUTED BY subst_ssrterm
-     RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm
-     GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm
+     RAW_PRINTED BY pr_ssrterm
+     GLOB_PRINTED BY pr_ssrterm
 | [ "YouShouldNotTypeThis" constr(c) ] -> [ mk_lterm c ]
 END
 
@@ -1904,7 +1915,7 @@ ARGUMENT EXTEND ssrclear TYPED AS ssrclear_ne PRINTED BY pr_ssrclear
 | [ ] -> [ [] ]
 END
 
-let cleartac clr = check_hyps_uniq [] clr; clear (hyps_ids clr)
+let cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (clear (hyps_ids clr))
 
 (* type ssrwgen = ssrclear * ssrhyp * string *)
 
@@ -1988,10 +1999,10 @@ let rec safe_depth c = match kind_of_term c with
 let red_safe r e s c0 =
   let rec red_to e c n = match kind_of_term c with
   | Prod (x, t, c') when n > 0 ->
-    let t' = r e s t in let e' = Environ.push_rel (Rel.Declaration.LocalAssum (x, t')) e in
+    let t' = r e s t in let e' = Environ.push_rel (RelDecl.LocalAssum (x, t')) e in
     mkProd (x, t', red_to e' c' (n - 1))
   | LetIn (x, b, t, c') when n > 0 ->
-    let t' = r e s t in let e' = Environ.push_rel (Rel.Declaration.LocalAssum (x, t')) e in
+    let t' = r e s t in let e' = Environ.push_rel (RelDecl.LocalAssum (x, t')) e in
     mkLetIn (x, r e s b, t', red_to e' c' (n - 1))
   | _ -> r e s c in
   red_to e c0 (safe_depth c0)
@@ -2012,7 +2023,7 @@ let pf_clauseids gl gens clseq =
   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"
+  CErrors.error "assumptions should be named explicitly"
 
 let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
 
@@ -2023,10 +2034,10 @@ let hidetacs clseq idhide cl0 =
 
 let discharge_hyp (id', (id, mode)) gl =
   let cl' = subst_var id (pf_concl gl) in
-  match Named.Declaration.to_tuple (pf_get_hyp gl id), mode with
-  | (_, None, t), _ | (_, Some _, t), "(" -> 
+  match pf_get_hyp gl id, mode with
+  | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" ->
      apply_type (mkProd (Name id', t, cl')) [mkVar id] gl
-  | (_, Some v, t), _ ->
+  | NamedDecl.LocalDef (_, v, t), _ ->
      Proofview.V82.of_tactic (convert_concl (mkLetIn (Name id', v, t, cl'))) gl
 
 let endclausestac id_map clseq gl_id cl0 gl =
@@ -2036,7 +2047,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
   let hide_goal = hidden_clseq clseq in
   let c_hidden = hide_goal && c = mkVar gl_id in
   let rec fits forced = function
-  | (id, _) :: ids, decl :: dc' when Rel.Declaration.get_name decl = Name id ->
+  | (id, _) :: ids, decl :: dc' when RelDecl.get_name decl = Name id ->
     fits true (ids, dc')
   | ids, dc' ->
     forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in
@@ -2049,18 +2060,18 @@ let endclausestac id_map clseq gl_id cl0 gl =
   | _ -> map_constr unmark c in
   let utac hyp =
     Proofview.V82.of_tactic 
-     (convert_hyp_no_check (Context.Named.Declaration.map_constr unmark hyp)) in
+     (convert_hyp_no_check (NamedDecl.map_constr unmark hyp)) in
   let utacs = List.map utac (pf_hyps gl) in
   let ugtac gl' =
     Proofview.V82.of_tactic
       (convert_concl_no_check (unmark (pf_concl gl'))) gl' in
-  let ctacs = if hide_goal then [clear [gl_id]] else [] in
+  let ctacs = if hide_goal then [Proofview.V82.of_tactic (clear [gl_id])] else [] in
   let mktac itacs = tclTHENLIST (itacs @ utacs @ ugtac :: ctacs) in
   let itac (_, id) = Proofview.V82.of_tactic (introduction id) in
   if fits false (id_map, List.rev dc) then mktac (List.map itac id_map) gl else
   let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in
   if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
-  Errors.error "tampering with discharged assumptions of \"in\" tactical"
+  CErrors.error "tampering with discharged assumptions of \"in\" tactical"
 
 let is_id_constr c = match kind_of_term c with
   | Lambda(_,_,c) when isRel c -> 1 = destRel c
@@ -2074,19 +2085,20 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
   let sigma, env = project gl, pf_env gl in
   let evar_closed t p =
     if occur_existential t then
-      Errors.user_err_loc (loc_of_cpattern p,"ssreflect",
-        pr_constr_pat t ++
+      CErrors.user_err ~loc:(loc_of_cpattern p) ~hdr:"ssreflect"
+        (pr_constr_pat t ++
         str" contains holes and matches no subterm of the goal") in
   match gen with
   | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) ->
      let x = hoi_id x in
-     let _, bo, ty = Named.Declaration.to_tuple (pf_get_hyp gl x) in
+     let decl = pf_get_hyp gl x in
      gl,
-     (if bo <> None then args else mkVar x :: args),
-     mkProd_or_LetIn (Rel.Declaration.of_tuple (Name (f x),bo,ty)) (subst_var x c)
+     (if NamedDecl.is_local_def decl then args else mkVar x :: args),
+     mkProd_or_LetIn (decl |> NamedDecl.to_rel_decl |> RelDecl.set_name (Name (f x)))
+                     (subst_var x c)
   | _, Some ((x, _), None) ->
      let x = hoi_id x in
-     gl, mkVar x :: args, mkProd (Name (f x), pf_get_hyp_typ gl x, subst_var x c)
+     gl, mkVar x :: args, mkProd (Name (f x),pf_get_hyp_typ gl x, subst_var x c)
   | _, Some ((x, "@"), Some p) -> 
      let x = hoi_id x in
      let cp = interp_cpattern ist gl p None in
@@ -2381,7 +2393,7 @@ END
 (* Populating the table *)
 
 let cache_viewhint (_, (i, lvh)) =
-  let mem_raw h = List.exists (Notation_ops.eq_glob_constr h) in
+  let mem_raw h = List.exists (Glob_ops.glob_constr_eq h) in
   let add_hint h hdb = if mem_raw h hdb then hdb else h :: hdb in
   viewtab.(i) <- List.fold_right add_hint lvh viewtab.(i)
 
@@ -2513,7 +2525,7 @@ let rec ipat_of_intro_pattern = function
   | IntroNaming IntroAnonymous -> IpatAnon
   | IntroAction (IntroRewrite b) -> IpatRw (allocc, if b then L2R else R2L)
   | IntroNaming (IntroFresh id) -> IpatAnon
-  | IntroAction (IntroApplyOn _) -> (* to do *) Errors.error "TO DO"
+  | IntroAction (IntroApplyOn _) -> (* to do *) CErrors.error "TO DO"
   | IntroAction (IntroInjection ips) ->
       IpatCase [List.map ipat_of_intro_pattern (List.map remove_loc ips)]
   | IntroForthcoming _ -> (* Unable to determine which kind of ipat interp_introid could return [HH] *)
@@ -2678,7 +2690,7 @@ END
 
 (* subsets of patterns *)
 let check_ssrhpats loc w_binders ipats =
-  let err_loc s = Errors.user_err_loc (loc, "ssreflect", s) in
+  let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in
   let clr, ipats =
     let rec aux clr = function
       | IpatSimpl (cl, Nop) :: tl -> aux (clr @ cl) tl
@@ -2771,8 +2783,8 @@ let equality_inj l b id c gl =
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj l b None c) gl
   with
-    | Compat.Exc_located(_,Errors.UserError (_,s))
-    | Errors.UserError (_,s)
+    | Compat.Exc_located(_,CErrors.UserError (_,s))
+    | CErrors.UserError (_,s)
   when msg := Pp.string_of_ppcmds s;
        !msg = "Not a projectable equality but a discriminable one." ||
        !msg = "Nothing to inject." ->
@@ -2786,7 +2798,7 @@ let injectl2rtac c = match kind_of_term c with
 | Var id -> injectidl2rtac id (mkVar id, NoBindings)
 | _ ->
   let id = injecteq_id in
-  tclTHENLIST [havetac id c; injectidl2rtac id (mkVar id, NoBindings); clear [id]]
+  tclTHENLIST [havetac id c; injectidl2rtac id (mkVar id, NoBindings); Proofview.V82.of_tactic (clear [id])]
 
 let is_injection_case c gl =
   let gl, cty = pf_type_of gl c in
@@ -2799,7 +2811,7 @@ let perform_injection c gl =
   let dc, eqt = decompose_prod t in
   if dc = [] then injectl2rtac c gl else
   if not (closed0 eqt) then
-    Errors.error "can't decompose a quantified equality" else
+    CErrors.error "can't decompose a quantified equality" else
   let cl = pf_concl gl in let n = List.length dc in
   let c_eq = mkEtaApp c n 2 in
   let cl1 = mkLambda (Anonymous, mkArrow eqt cl, mkApp (mkRel 1, [|c_eq|])) in
@@ -2822,10 +2834,10 @@ let intro_all gl =
 let rec intro_anon gl =
   try anontac (List.hd (fst (Term.decompose_prod_n_assum 1 (pf_concl gl)))) gl
   with err0 -> try tclTHEN (Proofview.V82.of_tactic red_in_concl) intro_anon gl with _ -> raise err0
-  (* with _ -> Errors.error "No product even after reduction" *)
+  (* with _ -> CErrors.error "No product even after reduction" *)
 
 let with_top tac =
-  tclTHENLIST [introid top_id; tac (mkVar top_id); clear [top_id]]
+  tclTHENLIST [introid top_id; tac (mkVar top_id); Proofview.V82.of_tactic (clear [top_id])]
 
 let rec mapLR f = function [] -> [] | x :: s -> let y = f x in y :: mapLR f s
 
@@ -2838,16 +2850,16 @@ let new_wild_id () =
   id
 
 let clear_wilds wilds gl =
-  clear (List.filter (fun id -> List.mem id wilds) (pf_ids_of_hyps gl)) gl
+  Proofview.V82.of_tactic (clear (List.filter (fun id -> List.mem id wilds) (pf_ids_of_hyps gl))) gl
 
 let clear_with_wilds wilds clr0 gl =
   let extend_clr clr nd =
-    let id = Named.Declaration.get_id nd in
+    let id = NamedDecl.get_id nd in
     if List.mem id clr || not (List.mem id wilds) then clr else
     let vars = global_vars_set_of_decl (pf_env gl) nd in
     let occurs id' = Idset.mem id' vars in
     if List.exists occurs clr then id :: clr else clr in
-  clear (Context.Named.fold_inside extend_clr ~init:clr0 (pf_hyps gl)) gl
+  Proofview.V82.of_tactic (clear (Context.Named.fold_inside extend_clr ~init:clr0 (pf_hyps gl))) gl
 
 let tclTHENS_nonstrict tac tacl taclname gl =
   let tacres = tac gl in
@@ -2896,7 +2908,7 @@ let ssrmkabs id gl =
       let Sigma (m, sigma, p5) = Evarutil.new_evar env sigma abstract_ty in
       Sigma ((m, abstract_ty), sigma, p1 +> p2 +> p3 +> p4 +> p5) in
     let sigma, kont =
-      let rd = Rel.Declaration.LocalAssum (Name id, abstract_ty) in
+      let rd = RelDecl.LocalAssum (Name id, abstract_ty) 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)
@@ -3072,12 +3084,12 @@ let tclDO n tac =
   let tac_err_at i gl =
     try tac gl
     with 
-    | Errors.UserError (l, s) as e ->
-        let _, info = Errors.push e in
-        let e' = Errors.UserError (l, prefix i ++ s) in
+    | CErrors.UserError (l, s) as e ->
+        let _, info = CErrors.push e in
+        let e' = CErrors.UserError (l, prefix i ++ s) in
         Util.iraise (e', info)
-    | Compat.Exc_located(loc, Errors.UserError (l, s))  -> 
-        raise (Compat.Exc_located(loc, Errors.UserError (l, prefix i ++ s))) in
+    | Compat.Exc_located(loc, CErrors.UserError (l, s))  -> 
+        raise (Compat.Exc_located(loc, CErrors.UserError (l, prefix i ++ s))) in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in
@@ -3244,7 +3256,7 @@ let tclREV tac gl = tclPERM List.rev tac gl
 let rot_hyps dir i hyps =
   let n = List.length hyps in
   if i = 0 then List.rev hyps else
-  if i > n then Errors.error "Not enough subgoals" else
+  if i > n then CErrors.error "Not enough subgoals" else
   let rec rot i l_hyps = function
     | hyp :: hyps' when i > 0 -> rot (i - 1) (hyp :: l_hyps) hyps'
     | hyps' -> hyps' @ (List.rev l_hyps) in
@@ -3397,7 +3409,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   | AtomicType _ ->
       let ty = 
         prof_saturate_whd.profile      
-        (Reductionops.whd_betadeltaiota env sigma) ty in
+        (Reductionops.whd_all env sigma) ty in
       match kind_of_type ty with
       | ProdType _ -> loop ty args sigma n
       | _ -> raise NotEnoughProducts
@@ -3447,9 +3459,9 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) =
     if tag_of_cpattern t = '@' then 
       if not (isVar c) then
 	errorstrm (str "@ can be used with variables only")
-      else match Named.Declaration.to_tuple (pf_get_hyp gl (destVar c)) with
-      | _, None, _ -> errorstrm (str "@ can be used with let-ins only")
-      | name, Some bo, ty -> true, pat, mkLetIn (Name name,bo,ty,cl),c,clr,ucst,gl
+      else match pf_get_hyp gl (destVar c) with
+      | NamedDecl.LocalAssum _ -> errorstrm (str "@ can be used with let-ins only")
+      | NamedDecl.LocalDef (name, b, ty) -> true, pat, mkLetIn (Name name,b,ty,cl),c,clr,ucst,gl
     else let gl, ccl =  pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl
   else if to_ind && occ = None then
     let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in
@@ -3462,7 +3474,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) =
 let genclrtac cl cs clr =
   let tclmyORELSE tac1 tac2 gl =
     try tac1 gl
-    with e when Errors.noncritical e -> tac2 e gl in
+    with e when CErrors.noncritical e -> tac2 e gl in
   (* apply_type may give a type error, but the useful message is
    * the one of clear.  You type "move: x" and you get
    * "x is used in hyp H" instead of
@@ -3521,7 +3533,7 @@ let cons_gen gen = function
 
 let cons_dep (gensl, clr) =
   if List.length gensl = 1 then ([] :: gensl, clr) else
-  Errors.error "multiple dependents switches '/'"
+  CErrors.error "multiple dependents switches '/'"
 
 ARGUMENT EXTEND ssrdgens_tl TYPED AS ssrgen list list * ssrclear
                             PRINTED BY pr_ssrdgens
@@ -3566,7 +3578,7 @@ let with_dgens (gensl, clr) maintac ist = match gensl with
 
 let first_goal gls =
   let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
-  if List.is_empty gl then Errors.error "first_goal";
+  if List.is_empty gl then CErrors.error "first_goal";
   { Evd.it = List.hd gl; Evd.sigma = sig_0; }
 
 let with_deps deps0 maintac cl0 cs0 clr0 ist gl0 =
@@ -3706,13 +3718,13 @@ let rec improper_intros = function
 
 let check_movearg = function
   | view, (eqid, _) when view <> [] && eqid <> None ->
-    Errors.error "incompatible view and equation in move tactic"
+    CErrors.error "incompatible view and equation in move tactic"
   | view, (_, (([gen :: _], _), _)) when view <> [] && has_occ gen ->
-    Errors.error "incompatible view and occurrence switch in move tactic"
+    CErrors.error "incompatible view and occurrence switch in move tactic"
   | _, (_, ((dgens, _), _)) when List.length dgens > 1 ->
-    Errors.error "dependents switch `/' in move tactic"
+    CErrors.error "dependents switch `/' in move tactic"
   | _, (eqid, (_, ipats)) when eqid <> None && improper_intros ipats ->
-    Errors.error "no proper intro pattern for equation in move tactic"
+    CErrors.error "no proper intro pattern for equation in move tactic"
   | arg -> arg
 
 ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg
@@ -3771,11 +3783,11 @@ let analyze_eliminator elimty env sigma =
   | AtomicType (hd, args) when isRel hd -> 
     ctx, destRel hd, not (noccurn 1 t), Array.length args
   | CastType (t, _) -> loop ctx t
-  | ProdType (x, ty, t) -> loop (Rel.Declaration.LocalAssum (x, ty) :: ctx) t
-  | LetInType (x,b,ty,t) -> loop (Rel.Declaration.LocalDef (x, b, ty) :: ctx) (subst1 b t)
+  | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t
+  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (subst1 b t)
   | _ ->
     let env' = Environ.push_rel_context ctx env in
-    let t' = Reductionops.whd_betadeltaiota env' sigma t in
+    let t' = Reductionops.whd_all env' sigma t in
     if not (Term.eq_constr t t') then loop ctx t' else
       errorstrm (str"The eliminator has the wrong shape."++spc()++
       str"A (applied) bound variable was expected as the conclusion of "++
@@ -3807,14 +3819,16 @@ let unprotecttac gl =
     let hyploc = Option.map (fun id -> id, InHyp) idopt in
     Proofview.V82.of_tactic (reduct_option 
       (Reductionops.clos_norm_flags 
-        (Closure.RedFlags.mkflags 
-          [Closure.RedFlags.fBETA;
-           Closure.RedFlags.fCONST prot;
-           Closure.RedFlags.fIOTA]), DEFAULTcast) hyploc))
+        (CClosure.RedFlags.mkflags 
+          [CClosure.RedFlags.fBETA;
+           CClosure.RedFlags.fCONST prot;
+           CClosure.RedFlags.fMATCH;
+           CClosure.RedFlags.fFIX;
+           CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc))
     allHypsAndConcl gl
 
 let dependent_apply_error =
-  try Errors.error "Could not fill dependent hole in \"apply\"" with err -> err
+  try CErrors.error "Could not fill dependent hole in \"apply\"" with err -> err
 
 (* TASSI: Sometimes Coq's apply fails. According to my experience it may be
  * related to goals that are products and with beta redexes. In that case it
@@ -3868,7 +3882,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
   in
   pp(lazy(str"after: " ++ pr_constr oc));
   try applyn ~with_evars ~with_shelve:true ?beta n oc gl
-  with e when Errors.noncritical e -> raise dependent_apply_error
+  with e when CErrors.noncritical e -> raise dependent_apply_error
 
 let pf_fresh_inductive_instance ind gl =
   let sigma, env, it = project gl, pf_env gl, sig_it gl in
@@ -3941,7 +3955,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
     | X_In_T (e, p) -> sigma, E_As_X_In_T (t, e, p)
     | _ ->
        try unify_HO env sigma t (fst (redex_of_pattern env p)), r
-       with e when Errors.noncritical e -> p in
+       with e when CErrors.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 *)
@@ -3954,7 +3968,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let elim, elimty, elim_args, 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
+      let elimty = Reductionops.whd_all env (project gl) elimty in
       let cty, gl =
         if Option.is_empty oc then None, gl
         else
@@ -3992,7 +4006,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
         | 0, Some p -> interp_cpattern (Option.get ist) orig_gl p None 
         | _ -> mkTpat gl c in
       let cty = Some (c, c_ty, pc) in
-      let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in
+      let elimty = Reductionops.whd_all env (project gl) elimty in
       cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
   pp(lazy(str"elim= "++ pr_constr_pat elim));
@@ -4007,7 +4021,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       Some (c, c_ty, gl, gl')
     with
     | NotEnoughProducts -> None
-    | e when Errors.noncritical e -> loop (n+1) in loop 0 in
+    | e when CErrors.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' *)
@@ -4221,7 +4235,7 @@ let _ = simplest_newcase_ref := simplest_newcase
 
 let check_casearg = function
 | view, (_, (([_; gen :: _], _), _)) when view <> [] && has_occ gen ->
-  Errors.error "incompatible view and occurrence switch in dependent case tactic"
+  CErrors.error "incompatible view and occurrence switch in dependent case tactic"
 | arg -> arg
 
 ARGUMENT EXTEND ssrcasearg TYPED AS ssrarg PRINTED BY pr_ssrarg
@@ -4376,7 +4390,7 @@ let refine_interp_apply_view i ist gl gv =
   loop (pair i viewtab.(i) @ if i = 2 then pair 1 viewtab.(1) else [])
 
 let apply_top_tac gl =
-  tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); clear [top_id]] gl
+  tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); Proofview.V82.of_tactic (clear [top_id])] gl
     
 let inner_ssrapplytac gviews ggenl gclr ist gl =
  let _, clr = interp_hyps ist gl gclr in
@@ -4420,12 +4434,15 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg
   [ mk_exactarg [] ([], clr) ]
 END
 
-let vmexacttac pf gl = exact_no_check (mkCast (pf, VMcast, pf_concl gl)) gl
+let vmexacttac pf =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  exact_no_check (mkCast (pf, VMcast, Tacmach.New.pf_concl gl))
+  end }
 
 TACTIC EXTEND ssrexact
 | [ "exact" ssrexactarg(arg) ] -> [ Proofview.V82.tactic (tclBY (ssrapplytac ist arg)) ]
 | [ "exact" ] -> [ Proofview.V82.tactic (tclORELSE donetac (tclBY apply_top_tac)) ]
-| [ "exact" "<:" lconstr(pf) ] -> [ Proofview.V82.tactic (vmexacttac pf) ]
+| [ "exact" "<:" lconstr(pf) ] -> [ vmexacttac pf ]
 END
 
 (** The "congr" tactic *)
@@ -4634,11 +4651,11 @@ let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) =
                      && (clr = None || clr = Some []) then
      anomaly "Improper rewrite clear switch";
    if d = R2L && rt <> RWdef then
-     Errors.error "Right-to-left switch on simplification";
+     CErrors.error "Right-to-left switch on simplification";
    if n <> 1 && rt = RWred Cut then
-     Errors.error "Bad or useless multiplier";
+     CErrors.error "Bad or useless multiplier";
    if occ <> None && rx = None && rt <> RWdef then
-     Errors.error "Missing redex for simplification occurrence"
+     CErrors.error "Missing redex for simplification occurrence"
  end; (d, m), ((docc, rx), r)
 
 let norwmult = L2R, nomult
@@ -4721,7 +4738,7 @@ let unfoldintac occ rdx t (kt,_) gl =
   let body env t c =
     Tacred.unfoldn [OnlyOccurrences [1], get_evalref t] env sigma0 c in
   let easy = occ = None && rdx = None in
-  let red_flags = if easy then Closure.betaiotazeta else Closure.betaiota in
+  let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in
   let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
   let unfold, conclude = match rdx with
   | Some (_, (In_T _ | In_X_In_T _)) | None ->
@@ -4812,7 +4829,7 @@ exception PRindetermined_rhs of constr
 let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
 (*   pp(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
   let env = pf_env gl in
-  let beta = Reductionops.clos_norm_flags Closure.beta env sigma in
+  let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in
   let sigma, p = 
     let sigma = create_evar_defs sigma in
     let sigma = Sigma.Unsafe.of_evar_map sigma in
@@ -4845,7 +4862,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     | App (hd, args) -> 
         let hd_ty = Retyping.get_type_of env sigma hd in
         let names = let rec aux t = function 0 -> [] | n ->
-          let t = Reductionops.whd_betadeltaiota env sigma t in
+          let t = Reductionops.whd_all env sigma t in
           match kind_of_type t with
           | ProdType (name, _, t) -> name :: aux t (n-1)
           | _ -> assert false in aux hd_ty (Array.length args) in
@@ -4880,7 +4897,7 @@ let rwcltac cl rdx dir sr gl =
       let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, build_coq_eq () in
       let sigma, c_ty = Typing.type_of env sigma c in
         pp(lazy(str"c_ty@rwcltac=" ++ pr_constr c_ty));
-      match kind_of_type (Reductionops.whd_betadeltaiota env sigma c_ty) with
+      match kind_of_type (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when is_ind_ref e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
@@ -4898,7 +4915,7 @@ let rwcltac cl rdx dir sr gl =
       let cl' = mkNamedProd rule_id (compose_prod dc r3t) (lift 1 cl) in
       let cl'' = mkNamedProd pattern_id rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
-      let cltac = clear [pattern_id; rule_id] in
+      let cltac = Proofview.V82.of_tactic (clear [pattern_id; rule_id]) in
       let rwtacs = [rewritetac dir (mkVar rule_id); cltac] in
       apply_type cl'' [rdx; compose_lam dc r3], tclTHENLIST (itacs @ rwtacs), gl
   in
@@ -4909,7 +4926,7 @@ let rwcltac cl rdx dir sr gl =
       then errorstrm (str "Rewriting impacts evars")
       else errorstrm (str "Dependent type error in rewrite of "
         ++ pf_pr_constr gl (project gl) (mkNamedLambda pattern_id rdxt cl))
-    | Errors.UserError _ as e -> raise e
+    | CErrors.UserError _ as e -> raise e
     | e -> anomaly ("cvtac's exception: " ^ Printexc.to_string e);
   in
   tclTHEN cvtac' rwtac gl
@@ -5185,7 +5202,7 @@ END
 let unfoldtac occ ko t kt gl =
   let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term t kt)) in
   let cl' = subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref c] gl c) cl in
-  let f = if ko = None then Closure.betaiotazeta else Closure.betaiota in
+  let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
   Proofview.V82.of_tactic
     (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
 
@@ -5533,7 +5550,7 @@ let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
 
 let bvar_locid = function
   | CRef (Ident (loc, id), _) -> loc, id
-  | _ -> Errors.error "Missing identifier after \"(co)fix\""
+  | _ -> CErrors.error "Missing identifier after \"(co)fix\""
 
 
 ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
@@ -5550,7 +5567,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
           (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id')
           | [l', Name id'] when sid = None -> false, (l', id')
           | _ :: bn -> loop bn
-          | [] -> Errors.error "Bad structural argument" in
+          | [] -> CErrors.error "Bad structural argument" in
         loop (names_of_local_assums lb) in
       let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
       let fix = CFix (loc, lid, [lid, (Some i, CStructRec), lb, t', c']) in
@@ -5687,7 +5704,7 @@ ARGUMENT EXTEND ssrhavefwdwbinders
     tr, ((((clr, pats), allbinders), simpl), hint) ]
 END
 
-(* Tactic. *)
+(* Pltac. *)
 
 let is_Evar_or_CastedMeta x =
   isEvar_or_Meta x ||
@@ -5730,9 +5747,10 @@ let pf_find_abstract_proof check_lock gl abstract_n =
            strbrk"Did you tamper with it?")
 
 let unfold cl =
-  let module R = Reductionops in let module F = Closure.RedFlags in
+  let module R = Reductionops in let module F = CClosure.RedFlags in
   reduct_in_concl (R.clos_norm_flags (F.mkflags
-    (List.map (fun c -> F.fCONST (fst (destConst c))) cl @ [F.fBETA; F.fIOTA])))
+    (List.map (fun c -> F.fCONST (fst (destConst c))) cl @
+       [F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX])))
 
 let havegentac ist t gl =
   let sigma, c, ucst, _ = pf_abs_ssrterm ist gl t in
@@ -5810,7 +5828,7 @@ let havetac ist
      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 "^
+       CErrors.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
@@ -5998,8 +6016,8 @@ END
 
 let destProd_or_LetIn c =
   match kind_of_term c with
-  | Prod (n,ty,c) -> Rel.Declaration.LocalAssum (n, ty), c
-  | LetIn (n,bo,ty,c) -> Rel.Declaration.LocalDef (n, bo, ty), c
+  | Prod (n,ty,c) -> RelDecl.LocalAssum (n, ty), c
+  | LetIn (n,bo,ty,c) -> RelDecl.LocalDef (n, bo, ty), c
   | _ -> raise DestKO
         
 let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
@@ -6035,14 +6053,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       | Sort _, [] -> Vars.subst_vars s ct
       | LetIn(Name id as n,b,ty,c), _::g -> mkLetIn (n,b,ty,var2rel c g (id::s))
       | Prod(Name id as n,ty,c), _::g -> mkProd (n,ty,var2rel c g (id::s))
-      | _ -> Errors.anomaly(str"SSR: wlog: var2rel: " ++ pr_constr c) in
+      | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_constr c) in
     let c = var2rel c gens [] in
     let rec pired c = function
       | [] -> c
       | t::ts as args -> match kind_of_term c with
          | Prod(_,_,c) -> pired (subst1 t c) ts
          | LetIn(id,b,ty,c) -> mkLetIn (id,b,ty,pired c args)
-         | _ -> Errors.anomaly(str"SSR: wlog: pired: " ++ pr_constr c) in
+         | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_constr c) in
     c, args, pired c args, pf_merge_uc uc gl in
   let tacipat pats = introstac ~ist pats in
   let tacigens = 
@@ -6064,7 +6082,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       | Some (Some id),_ -> Some id, introid id, clear0, pats
       | Some _,_ ->
           let id = mk_anon_id "tmp" gl in
-          Some id, introid id, tclTHEN clear0 (clear [id]), pats in
+          Some id, introid id, tclTHEN clear0 (Proofview.V82.of_tactic (clear [id])), pats in
       let tac_specialize = match id with
       | None -> tclIDTAC
       | Some id ->
@@ -6188,8 +6206,8 @@ END
 (* longer and thus comment out. Such comments are marked with v8.3     *)
 
 GEXTEND Gram
-  GLOBAL: Tactic.hypident;
-  Tactic.hypident: [
+  GLOBAL: Pltac.hypident;
+  Pltac.hypident: [
   [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly
   | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly
   ] ];
@@ -6206,8 +6224,8 @@ hloc: [
 END
 
 GEXTEND Gram
-  GLOBAL: Tactic.constr_eval;
-  Tactic.constr_eval: [
+  GLOBAL: Pltac.constr_eval;
+  Pltac.constr_eval: [
     [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ]
   ];
 END
@@ -6216,6 +6234,6 @@ END
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
 (* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
 (* consequence the extended ssreflect grammar.                             *)
-let () = Lexer.unfreeze frozen_lexer ;;
+let () = CLexer.unfreeze frozen_lexer ;;
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.mllib b/mathcomp/ssreflect/plugin/trunk/ssreflect_plugin.mlpack
index 006b70f..006b70f 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.mllib
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect_plugin.mlpack
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
deleted file mode 100644
index cc2643a..0000000
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ /dev/null
@@ -1,1359 +0,0 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-
-(* Defining grammar rules with "xx" in it automatically declares keywords too,
- * we thus save the lexer to restore it at the end of the file *)
-let frozen_lexer = Lexer.freeze () ;;
-
-(*i camlp4use: "pa_extend.cmo" i*)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Names
-open Pp
-open Pcoq
-open Genarg
-open Constrarg
-open Term
-open Vars
-open Topconstr
-open Libnames
-open Tactics
-open Tacticals
-open Termops
-open Namegen
-open Recordops
-open Tacmach
-open Coqlib
-open Glob_term
-open Util
-open Evd
-open Extend
-open Goptions
-open Tacexpr
-open Proofview.Notations
-open Tacinterp
-open Pretyping
-open Constr
-open Tactic
-open Extraargs
-open Ppconstr
-open Printer
-
-open Globnames
-open Misctypes
-open Decl_kinds
-open Evar_kinds
-open Constrexpr
-open Constrexpr_ops
-open Notation_term
-open Notation_ops
-open Locus
-open Locusops
-
-DECLARE PLUGIN "ssreflect"
-
-type loc = Loc.t
-let dummy_loc = Loc.ghost
-let errorstrm = Errors.errorlabstrm "ssreflect"
-let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg)
-
-(* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
-(* or if SsrDebug is Set                                                  *)
-let pp_ref = ref (fun _ -> ())
-let ssr_pp s = pperrnl (str"SSR: "++Lazy.force s)
-let _ = try ignore(Sys.getenv "SSRDEBUG"); pp_ref := ssr_pp with Not_found -> ()
-let debug b =
-  if b then pp_ref := ssr_pp else pp_ref := fun _ -> ()
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = false;
-      Goptions.optname  = "ssrmatching debugging";
-      Goptions.optkey   = ["SsrMatchingDebug"];
-      Goptions.optdepr  = false;
-      Goptions.optread  = (fun _ -> !pp_ref == ssr_pp);
-      Goptions.optwrite = debug }
-let pp s = !pp_ref s
-
-(** Utils {{{ *****************************************************************)
-let env_size env = List.length (Environ.named_context env)
-let safeDestApp c =
-  match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |]
-let get_index = function ArgArg i -> i | _ ->
-  Errors.anomaly (str"Uninterpreted index")
-(* Toplevel constr must be globalized twice ! *)
-let glob_constr ist genv = function
-  | _, Some ce ->
-    let vars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in
-    let ltacvars = { Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
-    Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv ce
-  | rc, None -> rc
-
-(* Term printing utilities functions for deciding bracketing.  *)
-let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")")
-(* String lexing utilities *)
-let skip_wschars s =
-  let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop
-(* We also guard characters that might interfere with the ssreflect   *)
-(* tactic syntax.                                                     *)
-let guard_term ch1 s i = match s.[i] with
-  | '(' -> false
-  | '{' | '/' | '=' -> true
-  | _ -> ch1 = '('
-(* The call 'guard s i' should return true if the contents of s *)
-(* starting at i need bracketing to avoid ambiguities.          *)
-let pr_guarded guard prc c =
-  msg_with Format.str_formatter (prc c);
-  let s = Format.flush_str_formatter () ^ "$" in
-  if guard s (skip_wschars s 0) then pr_paren prc c else prc c
-(* More sensible names for constr printers *)
-let pr_constr = pr_constr
-let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c
-let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c
-let prl_constr_expr = pr_lconstr_expr
-let pr_constr_expr = pr_constr_expr
-let prl_glob_constr_and_expr = function
-  | _, Some c -> prl_constr_expr c
-  | c, None -> prl_glob_constr c
-let pr_glob_constr_and_expr = function
-  | _, Some c -> pr_constr_expr c
-  | c, None -> pr_glob_constr c
-let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
-let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c
-
-(** Adding a new uninterpreted generic argument type *)
-let add_genarg tag pr =
-  let wit = Genarg.make0 tag in
-  let glob ist x = (ist, x) in
-  let subst _ x = x in
-  let interp ist x = Ftactic.return x in
-  let gen_pr _ _ _ = pr in
-  let () = Genintern.register_intern0 wit glob in
-  let () = Genintern.register_subst0 wit subst in
-  let () = Geninterp.register_interp0 wit interp in
-  Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
-  wit
-
-(** Constructors for cast type *)
-let dC t = CastConv t
-(** Constructors for constr_expr *)
-let isCVar = function CRef (Ident _, _) -> true | _ -> false
-let destCVar = function CRef (Ident (_, id), _) -> id | _ ->
-  Errors.anomaly (str"not a CRef")
-let mkCHole loc = CHole (loc, None, IntroAnonymous, None)
-let mkCLambda loc name ty t = 
-   CLambdaN (loc, [[loc, name], Default Explicit, ty], t)
-let mkCLetIn loc name bo t = 
-   CLetIn (loc, (loc, name), bo, t)
-let mkCCast loc t ty = CCast (loc,t, dC ty)
-(** Constructors for rawconstr *)
-let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None)
-let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args)
-let mkRCast rc rt =  GCast (dummy_loc, rc, dC rt)
-let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t)
-
-(* ssrterm conbinators *)
-let combineCG t1 t2 f g = match t1, t2 with
- | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
- | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2))
- | _, (_, (_, None)) -> Errors.anomaly (str"have: mixed C-G constr")
- | _ -> Errors.anomaly (str"have: mixed G-C constr")
-let loc_ofCG = function
- | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s
- | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s
-
-let mk_term k c = k, (mkRHole, Some c)
-let mk_lterm = mk_term ' '
-
-let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl)  sigma, ty
-
-(* }}} *)
-
-(** Profiling {{{ *************************************************************)
-type profiler = { 
-  profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
-  reset : unit -> unit;
-  print : unit -> unit }
-let profile_now = ref false
-let something_profiled = ref false
-let profilers = ref []
-let add_profiler f = profilers := f :: !profilers;;
-let profile b =
-  profile_now := b;
-  if b then List.iter (fun f -> f.reset ()) !profilers;
-  if not b then List.iter (fun f -> f.print ()) !profilers
-;;
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = false;
-      Goptions.optname  = "ssrmatching profiling";
-      Goptions.optkey   = ["SsrMatchingProfiling"];
-      Goptions.optread  = (fun _ -> !profile_now);
-      Goptions.optdepr  = false;
-      Goptions.optwrite = profile }
-let () =
-  let prof_total = 
-    let init = ref 0.0 in { 
-    profile = (fun f x -> assert false);
-    reset = (fun () -> init := Unix.gettimeofday ());
-    print = (fun () -> if !something_profiled then
-        prerr_endline 
-           (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
-           "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in
-  let prof_legenda = {
-    profile = (fun f x -> assert false);
-    reset = (fun () -> ());
-    print = (fun () -> if !something_profiled then begin
-        prerr_endline 
-           (Printf.sprintf "!! %39s ---------- --------- --------- ---------" 
-           (String.make 39 '-'));
-        prerr_endline 
-           (Printf.sprintf "!! %-39s %10s %9s %9s %9s" 
-           "function" "#calls" "total" "max" "average") end) } in
-  add_profiler prof_legenda;
-  add_profiler prof_total
-;;
-
-let mk_profiler s =
-  let total, calls, max = ref 0.0, ref 0, ref 0.0 in
-  let reset () = total := 0.0; calls := 0; max := 0.0 in
-  let profile f x =
-    if not !profile_now then f x else
-    let before = Unix.gettimeofday () in
-    try
-      incr calls;
-      let res = f x in
-      let after = Unix.gettimeofday () in
-      let delta = after -. before in
-      total := !total +. delta;
-      if delta > !max then max := delta;
-      res
-    with exc ->
-      let after = Unix.gettimeofday () in
-      let delta = after -. before in
-      total := !total +. delta;
-      if delta > !max then max := delta;
-      raise exc in
-  let print () =
-     if !calls <> 0 then begin
-       something_profiled := true;
-       prerr_endline
-         (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" 
-         s !calls !total !max (!total /. (float_of_int !calls))) end in
-  let prof = { profile = profile; reset = reset; print = print } in
-  add_profiler prof;
-  prof
-;;
-(* }}} *)
-
-exception NoProgress
-
-(** Unification procedures.                                *)
-
-(* To enforce the rigidity of the rooted match we always split  *)
-(* top applications, so the unification procedures operate on   *)
-(* arrays of patterns and terms.                                *)
-(* We perform three kinds of unification:                       *)
-(*  EQ: exact conversion check                                  *)
-(*  FO: first-order unification of evars, without conversion    *)
-(*  HO: higher-order unification with conversion                *)
-(* The subterm unification strategy is to find the first FO     *)
-(* match, if possible, and the first HO match otherwise, then   *)
-(* compute all the occurrences that are EQ matches for the      *)
-(* relevant subterm.                                            *)
-(*   Additional twists:                                         *)
-(*    - If FO/HO fails then we attempt to fill evars using      *)
-(*      typeclasses before raising an outright error. We also   *)
-(*      fill typeclasses even after a successful match, since   *)
-(*      beta-reduction and canonical instances may leave        *)
-(*      undefined evars.                                        *)
-(*    - We do postchecks to rule out matches that are not       *)
-(*      closed or that assign to a global evar; these can be    *)
-(*      disabled for rewrite or dependent family matches.       *)
-(*    - We do a full FO scan before turning to HO, as the FO    *)
-(*      comparison can be much faster than the HO one.          *)
-
-let unif_EQ env sigma p c =
-  let evars = existential_opt_value sigma, Evd.universes sigma in 
-  try let _ = Reduction.conv env p ~evars c in true with _ -> false
-
-let unif_EQ_args env sigma pa a =
-  let n = Array.length pa in
-  let rec loop i = (i = n) || unif_EQ env sigma pa.(i) a.(i) && loop (i + 1) in
-  loop 0
-
-let prof_unif_eq_args = mk_profiler "unif_EQ_args";;
-let unif_EQ_args env sigma pa a =
-  prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a 
-;;
-
-let unif_HO env ise p c = Evarconv.the_conv_x env p c ise
-
-let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise
-
-let unif_HO_args env ise0 pa i ca =
-  let n = Array.length pa in
-  let rec loop ise j =
-    if j = n then ise else loop (unif_HO env ise pa.(j) ca.(i + j)) (j + 1) in
-  loop ise0 0
-
-(* FO unification should boil down to calling w_unify with no_delta, but  *)
-(* alas things are not so simple: w_unify does partial type-checking,     *)
-(* which breaks down when the no-delta flag is on (as the Coq type system *)
-(* requires full convertibility. The workaround here is to convert all    *)
-(* evars into metas, since 8.2 does not TC metas. This means some lossage *)
-(* for HO evars, though hopefully Miller patterns can pick up some of     *)
-(* those cases, and HO matching will mop up the rest.                     *)
-let flags_FO =
-  let flags =
-    { (Unification.default_no_delta_unify_flags ()).Unification.core_unify_flags
-      with
-        Unification.modulo_conv_on_closed_terms = None;
-        Unification.modulo_eta = true;
-        Unification.modulo_betaiota = true;
-        Unification.modulo_delta_types = full_transparent_state}
-  in
-  { Unification.core_unify_flags = flags;
-    Unification.merge_unify_flags = flags;
-    Unification.subterm_unify_flags = flags;
-    Unification.allow_K_in_toplevel_higher_order_unification = false;
-    Unification.resolve_evars =
-      (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars
-  }
-let unif_FO env ise p c =
-  Unification.w_unify env ise Reduction.CONV ~flags:flags_FO p c
-
-(* Perform evar substitution in main term and prune substitution. *)
-let nf_open_term sigma0 ise c =
-  let s = ise and s' = ref sigma0 in
-  let rec nf c' = match kind_of_term c' with
-  | Evar ex ->
-    begin try nf (existential_value s ex) with _ ->
-    let k, a = ex in let a' = Array.map nf a in
-    if not (Evd.mem !s' k) then
-      s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k));
-    mkEvar (k, a')
-    end
-  | _ -> map_constr nf c' in
-  let copy_def k evi () =
-    if evar_body evi != Evd.Evar_empty then () else
-    match Evd.evar_body (Evd.find s k) with
-    | Evar_defined c' -> s' := Evd.define k (nf c') !s'
-    | _ -> () in
-  let c' = nf c in let _ = Evd.fold copy_def sigma0 () in
-  !s', Evd.evar_universe_context s, c'
-
-let unif_end env sigma0 ise0 pt ok =
-  let ise = Evarconv.consider_remaining_unif_problems env ise0 in
-  let s, uc, t = nf_open_term sigma0 ise pt in
-  let ise1 = create_evar_defs s in
-  let ise1 = Evd.set_universe_context ise1 uc in
-  let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
-  if not (ok ise) then raise NoProgress else
-  if ise2 == ise1 then (s, uc, t)
-  else
-    let s, uc', t = nf_open_term sigma0 ise2 t in
-    s, Evd.union_evar_universe_context uc uc', t
-
-let pf_unif_HO gl sigma pt p c =
-  let env = pf_env gl in
-  let ise = unif_HO env (create_evar_defs sigma) p c in
-  unif_end env (project gl) ise pt (fun _ -> true)
-
-let unify_HO env sigma0 t1 t2 =
-  let sigma = unif_HO env sigma0 t1 t2 in
-  let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in
-  Evd.set_universe_context sigma uc
-
-let pf_unify_HO gl t1 t2 =
-  let env, sigma0, si = pf_env gl, project gl, sig_it gl in
-  let sigma = unify_HO env sigma0 t1 t2 in
-  re_sig si sigma
-
-(* This is what the definition of iter_constr should be... *)
-let iter_constr_LR f c = match kind_of_term c with
-  | Evar (k, a) -> Array.iter f a
-  | Cast (cc, _, t) -> f cc; f t  
-  | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
-  | LetIn (_, v, t, b) -> f v; f t; f b
-  | App (cf, a) -> f cf; Array.iter f a
-  | Case (_, p, v, b) -> f v; f p; Array.iter f b
-  | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
-    for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
-  | _ -> ()
-
-(* The comparison used to determine which subterms matches is KEYED        *)
-(* CONVERSION. This looks for convertible terms that either have the same  *)
-(* same head constant as pat if pat is an application (after beta-iota),   *)
-(* or start with the same constr constructor (esp. for LetIn); this is     *)
-(* disregarded if the head term is let x := ... in x, and casts are always *)
-(* ignored and removed).                                                   *)
-(* Record projections get special treatment: in addition to the projection *)
-(* constant itself, ssreflect also recognizes head constants of canonical  *)
-(* projections.                                                            *)
-
-exception NoMatch
-type ssrdir = L2R | R2L
-let pr_dir_side = function L2R -> str "LHS" | R2L -> str "RHS"
-let inv_dir = function L2R -> R2L | R2L -> L2R
-
-
-type pattern_class =
-  | KpatFixed
-  | KpatConst
-  | KpatEvar of existential_key
-  | KpatLet
-  | KpatLam
-  | KpatRigid
-  | KpatFlex
-  | KpatProj of constant
-
-type tpattern = {
-  up_k : pattern_class;
-  up_FO : constr;
-  up_f : constr;
-  up_a : constr array;
-  up_t : constr;                      (* equation proof term or matched term *)
-  up_dir : ssrdir;                    (* direction of the rule *)
-  up_ok : constr -> evar_map -> bool; (* progess test for rewrite *)
-  }
-
-let all_ok _ _ = true
-
-let proj_nparams c =
-  try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
-
-let isFixed c = match kind_of_term c with
-  | Var _ | Ind _ | Construct _ | Const _ -> true
-  | _ -> false
-
-let isRigid c = match kind_of_term c with
-  | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
-  | _ -> false
-
-exception UndefPat
-
-let hole_var = mkVar (id_of_string "_")
-let pr_constr_pat c0 =
-  let rec wipe_evar c =
-    if isEvar c then hole_var else map_constr wipe_evar c in
-  pr_constr (wipe_evar c0)
-
-(* Turn (new) evars into metas *)
-let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
-  let ise = ref ise0 in
-  let sigma = ref ise0 in
-  let nenv = env_size env + if hack then 1 else 0 in
-  let rec put c = match kind_of_term c with
-  | Evar (k, a as ex) ->
-    begin try put (existential_value !sigma ex)
-    with NotInstantiatedEvar ->
-    if Evd.mem sigma0 k then map_constr put c else
-    let evi = Evd.find !sigma k in
-    let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in
-    let abs_dc (d, c) = function
-    | Context.Named.Declaration.LocalDef (x, b, t) ->
-        d, mkNamedLetIn x (put b) (put t) c
-    | Context.Named.Declaration.LocalAssum (x, t) ->
-        mkVar x :: d, mkNamedProd x (put t) c in
-    let a, t =
-      Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in
-    let m = Evarutil.new_meta () in
-    ise := meta_declare m t !ise;
-    sigma := Evd.define k (applist (mkMeta m, a)) !sigma;
-    put (existential_value !sigma ex)
-    end
-  | _ -> map_constr put c in
-  let c1 = put c0 in !ise, c1
-
-(* Compile a match pattern from a term; t is the term to fill. *)
-(* p_origin can be passed to obtain a better error message     *)
-let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
-  let k, f, a =
-    let f, a = Reductionops.whd_betaiota_stack ise p in
-    match kind_of_term f with
-    | Const (p,_) ->
-      let np = proj_nparams p in
-      if np = 0 || np > List.length a then KpatConst, f, a else
-      let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2
-    | Var _ | Ind _ | Construct _ -> KpatFixed, f, a
-    | Evar (k, _) ->
-      if Evd.mem sigma0 k then KpatEvar k, f, a else
-      if a <> [] then KpatFlex, f, a else 
-      (match p_origin with None -> Errors.error "indeterminate pattern"
-      | Some (dir, rule) ->
-	errorstrm (str "indeterminate " ++ pr_dir_side dir
-          ++ str " in " ++ pr_constr_pat rule))
-    | LetIn (_, v, _, b) ->
-      if b <> mkRel 1 then KpatLet, f, a else KpatFlex, v, a
-    | Lambda _ -> KpatLam, f, a
-    | _ -> KpatRigid, f, a in
-  let aa = Array.of_list a in
-  let ise', p' = evars_for_FO ~hack env sigma0 ise (mkApp (f, aa)) in
-  ise',
-  { up_k = k; up_FO = p'; up_f = f; 
-    up_a = aa; up_ok = ok; up_dir = dir; up_t = t}
-
-(* Specialize a pattern after a successful match: assign a precise head *)
-(* kind and arity for Proj and Flex patterns.                           *)
-let ungen_upat lhs (sigma, uc, t) u =
-  let f, a = safeDestApp lhs in
-  let k = match kind_of_term f with
-  | Var _ | Ind _ | Construct _ -> KpatFixed
-  | Const _ -> KpatConst
-  | Evar (k, _) -> if is_defined sigma k then raise NoMatch else KpatEvar k
-  | LetIn _ -> KpatLet
-  | Lambda _ -> KpatLam
-  | _ -> KpatRigid in
-  sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t}
-
-let nb_cs_proj_args pc f u =
-  let na k =
-    List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in
-  try match kind_of_term f with
-  | Prod _ -> na Prod_cs
-  | Sort s -> na (Sort_cs (family_of_sort s))
-  | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f))
-  | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
-  | _ -> -1
-  with Not_found -> -1
-
-let isEvar_k k f =
-  match kind_of_term f with Evar (k', _) -> k = k' | _ -> false
-
-let nb_args c =
-  match kind_of_term c with App (_, a) -> Array.length a | _ -> 0
-
-let mkSubArg i a = if i = Array.length a then a else Array.sub a 0 i
-let mkSubApp f i a = if i = 0 then f else mkApp (f, mkSubArg i a)
-
-let splay_app ise =
-  let rec loop c a = match kind_of_term c with
-  | App (f, a') -> loop f (Array.append a' a)
-  | Cast (c', _, _) -> loop c' a
-  | Evar ex ->
-    (try loop (existential_value ise ex) a with _ -> c, a)
-  | _ -> c, a in
-  fun c -> match kind_of_term c with
-  | App (f, a) -> loop f a
-  | Cast _ | Evar _ -> loop c [| |]
-  | _ -> c, [| |]
-
-let filter_upat i0 f n u fpats =
-  let na = Array.length u.up_a in
-  if n < na then fpats else
-  let np = match u.up_k with
-  | KpatConst when Term.eq_constr u.up_f f -> na
-  | KpatFixed when Term.eq_constr u.up_f f -> na 
-  | KpatEvar k when isEvar_k k f -> na
-  | KpatLet when isLetIn f -> na
-  | KpatLam when isLambda f -> na
-  | KpatRigid when isRigid f -> na
-  | KpatFlex -> na
-  | KpatProj pc ->
-    let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np
-  | _ -> -1 in
-  if np < na then fpats else
-  let () = if !i0 < np then i0 := n in (u, np) :: fpats
-
-let filter_upat_FO i0 f n u fpats =
-  let np = nb_args u.up_FO in
-  if n < np then fpats else
-  let ok = match u.up_k with
-  | KpatConst -> Term.eq_constr u.up_f f 
-  | KpatFixed -> Term.eq_constr u.up_f f 
-  | KpatEvar k -> isEvar_k k f
-  | KpatLet -> isLetIn f
-  | KpatLam -> isLambda f
-  | KpatRigid -> isRigid f
-  | KpatProj pc -> Term.eq_constr f (mkConst pc)
-  | KpatFlex -> i0 := n; true in
-  if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats
-
-exception FoundUnif of (evar_map * evar_universe_context * tpattern)
-(* Note: we don't update env as we descend into the term, as the primitive *)
-(* unification procedure always rejects subterms with bound variables.     *)
-
-let dont_impact_evars_in cl =
-  let evs_in_cl = Evd.evars_of_term cl in
-  fun sigma -> Evar.Set.for_all (fun k ->
-    try let _ = Evd.find_undefined sigma k in true
-    with Not_found -> false) evs_in_cl
-
-(* We are forced to duplicate code between the FO/HO matching because we    *)
-(* have to work around several kludges in unify.ml:                         *)
-(*  - w_unify drops into second-order unification when the pattern is an    *)
-(*    application whose head is a meta.                                     *)
-(*  - w_unify tries to unify types without subsumption when the pattern     *)
-(*    head is an evar or meta (e.g., it fails on ?1 = nat when ?1 : Type).  *)
-(*  - w_unify expands let-in (zeta conversion) eagerly, whereas we want to  *)
-(*    match a head let rigidly.                                             *)
-let match_upats_FO upats env sigma0 ise orig_c =
-  let dont_impact_evars = dont_impact_evars_in orig_c in
-  let rec loop c =
-    let f, a = splay_app ise c in let i0 = ref (-1) in
-    let fpats =
-      List.fold_right (filter_upat_FO i0 f (Array.length a)) upats [] in
-    while !i0 >= 0 do
-      let i = !i0 in i0 := -1;
-      let c' = mkSubApp f i a in
-      let one_match (u, np) =
-         let skip =
-           if i <= np then i < np else
-           if u.up_k == KpatFlex then begin i0 := i - 1; false end else
-           begin if !i0 < np then i0 := np; true end in
-         if skip || not (closed0 c') then () else try
-           let _ = match u.up_k with
-           | KpatFlex ->
-             let kludge v = mkLambda (Anonymous, mkProp, v) in
-             unif_FO env ise (kludge u.up_FO) (kludge c')
-           | KpatLet ->
-             let kludge vla =
-               let vl, a = safeDestApp vla in
-               let x, v, t, b = destLetIn vl in
-               mkApp (mkLambda (x, t, b), Array.cons v a) in
-             unif_FO env ise (kludge u.up_FO) (kludge c')
-           | _ -> unif_FO env ise u.up_FO c' in
-           let ise' = (* Unify again using HO to assign evars *)
-             let p = mkApp (u.up_f, u.up_a) in
-             try unif_HO env ise p c' with _ -> raise NoMatch 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))
-       with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
-       | Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO")
-       | _ -> () in
-    List.iter one_match fpats
-  done;
-  iter_constr_LR loop f; Array.iter loop a in
-  try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO")
-
-let prof_FO = mk_profiler "match_upats_FO";;
-let match_upats_FO upats env sigma0 ise c =
-  prof_FO.profile (match_upats_FO upats env sigma0) ise c
-;;
-
-
-let match_upats_HO ~on_instance upats env sigma0 ise c =
-  let dont_impact_evars = dont_impact_evars_in c in
- let it_did_match = ref false in
- let failed_because_of_TC = ref false in
- let rec aux upats env sigma0 ise c =
-  let f, a = splay_app ise c in let i0 = ref (-1) in
-  let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
-  while !i0 >= 0 do
-    let i = !i0 in i0 := -1;
-    let one_match (u, np) =
-      let skip =
-        if i <= np then i < np else
-        if u.up_k == KpatFlex then begin i0 := i - 1; false end else
-        begin if !i0 < np then i0 := np; true end in
-      if skip then () else try
-        let ise' = match u.up_k with
-        | KpatFixed | KpatConst -> ise
-        | KpatEvar _ ->
-          let _, pka = destEvar u.up_f and _, ka = destEvar f in
-          unif_HO_args env ise pka 0 ka
-        | KpatLet ->
-          let x, v, t, b = destLetIn f in
-          let _, pv, _, pb = destLetIn u.up_f in
-          let ise' = unif_HO env ise pv v in
-          unif_HO
-            (Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env)
-            ise' pb b
-        | KpatFlex | KpatProj _ ->
-          unif_HO env ise u.up_f (mkSubApp f (i - Array.length u.up_a) a)
-        | _ -> unif_HO env ise u.up_f f in
-        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)
-      with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
-      | NoProgress -> it_did_match := true
-      | Pretype_errors.PretypeError
-         (_,_,Pretype_errors.UnsatisfiableConstraints _) ->
-          failed_because_of_TC:=true
-      | e when Errors.noncritical e -> () in
-    List.iter one_match fpats
-  done;
-  iter_constr_LR (aux upats env sigma0 ise) f;
-  Array.iter (aux upats env sigma0 ise) a
- in
- aux upats env sigma0 ise c;
- if !it_did_match then raise NoProgress;
- !failed_because_of_TC
-
-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 fixed_upat = function
-| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false 
-| {up_t = t} -> not (occur_existential t)
-
-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 find_P = 
-  Environ.env -> Term.constr -> int ->
-  k:subst ->
-     Term.constr
-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)
-  ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats)
-=
-  let nocc = ref 0 and skip_occ = ref false in
-  let use_occ, occ_list = match occ with
-  | Some (true, ol) -> ol = [], ol
-  | Some (false, ol) -> ol <> [], ol
-  | None -> false, [] in
-  let max_occ = List.fold_right max occ_list 0 in
-  let subst_occ =
-    let occ_set = Array.make max_occ (not use_occ) in
-    let _ = List.iter (fun i -> occ_set.(i - 1) <- use_occ) occ_list in
-    let _ = if max_occ = 0 then skip_occ := use_occ in
-    fun () -> incr nocc;
-    if !nocc = max_occ then skip_occ := use_occ;
-    if !nocc <= max_occ then occ_set.(!nocc - 1) else not use_occ in
-  let upat_that_matched = ref None in
-  let match_EQ env sigma u = 
-    match u.up_k with
-    | KpatLet ->
-      let x, pv, t, pb = destLetIn u.up_f in
-      let env' =
-        Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in
-      let match_let f = match kind_of_term f with
-      | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b
-      | _ -> false in match_let
-    | KpatFixed -> Term.eq_constr u.up_f
-    | KpatConst -> Term.eq_constr u.up_f
-    | KpatLam -> fun c ->
-       (match kind_of_term c with
-       | Lambda _ -> unif_EQ env sigma u.up_f c
-       | _ -> false)
-    | _ -> unif_EQ env sigma u.up_f in
-let p2t p = mkApp(p.up_f,p.up_a) in 
-let source () = match upats_origin, upats with
-  | None, [p] -> 
-      (if fixed_upat p then str"term " else str"partial term ") ++ 
-      pr_constr_pat (p2t p) ++ spc()
-  | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
-      pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()
-  | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
-      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 () -> 
-    let failed_because_of_TC = ref false in
-    try
-      if not all_instances then match_upats_FO upats env sigma0 ise c;
-      failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c;
-      raise NoMatch
-    with FoundUnif sigma_u -> 0,[sigma_u]
-    | (NoMatch|NoProgress) when all_instances && instances () <> [] ->
-      0, uniquize (instances ())
-    | NoMatch when (not raise_NoMatch) ->
-      if !failed_because_of_TC then
-        errorstrm (source ()++strbrk"matches but type classes inference fails")
-      else
-        errorstrm (source () ++ str "does not match any subterm of the goal")
-    | NoProgress when (not raise_NoMatch) ->
-        let dir = match upats_origin with Some (d,_) -> d | _ ->
-          Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
-        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
-(*   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' =
-    if !skip_occ then c' else
-    let f, a = splay_app sigma c' in
-    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
-      mkApp (f', Array.map_left (subst_loop acc) a2)
-    else
-      (* TASSI: clear letin values to avoid unfolding *)
-      let inc_h rd (env,h') =
-        let ctx_item =
-          match rd with
-          | Context.Rel.Declaration.LocalAssum _ as x -> x
-          | Context.Rel.Declaration.LocalDef (x,_,y) ->
-              Context.Rel.Declaration.LocalAssum(x,y) in
-        Environ.push_rel ctx_item env, h' + 1 in
-      let f' = map_constr_with_binders_left_to_right inc_h subst_loop acc f in
-      mkApp (f', Array.map_left (subst_loop acc) a) in
-  subst_loop (env,h) c) : find_P),
-((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
-    | 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)
-  else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++
-        str(String.plural !nocc " occurence") ++ match upats_origin with
-        | None -> str" of" ++ spc() ++ pr_constr_pat p'
-        | Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++
-            ws 4 ++ pr_constr_pat p' ++ fnl () ++ 
-            str"of " ++ pr_constr_pat rule)) : conclude)
-
-type ('ident, 'term) ssrpattern = 
-  | T of 'term
-  | In_T of 'term
-  | X_In_T of 'ident * 'term     
-  | In_X_In_T of 'ident * 'term     
-  | E_In_X_In_T of 'term * 'ident * 'term     
-  | E_As_X_In_T of 'term * 'ident * 'term     
-        
-let pr_pattern = function
-  | T t -> prl_term t
-  | In_T t -> str "in " ++ prl_term t
-  | X_In_T (x,t) -> prl_term x ++ str " in " ++ prl_term t
-  | In_X_In_T (x,t) -> str "in " ++ prl_term x ++ str " in " ++ prl_term t
-  | E_In_X_In_T (e,x,t) ->
-      prl_term e ++ str " in " ++ prl_term x ++ str " in " ++ prl_term t
-  | E_As_X_In_T (e,x,t) ->
-      prl_term e ++ str " as " ++ prl_term x ++ str " in " ++ prl_term t
-
-let pr_pattern_w_ids = function
-  | T t -> prl_term t
-  | In_T t -> str "in " ++ prl_term t
-  | X_In_T (x,t) -> pr_id x ++ str " in " ++ prl_term t
-  | In_X_In_T (x,t) -> str "in " ++ pr_id x ++ str " in " ++ prl_term t
-  | E_In_X_In_T (e,x,t) ->
-      prl_term e ++ str " in " ++ pr_id x ++ str " in " ++ prl_term t
-  | E_As_X_In_T (e,x,t) ->
-      prl_term e ++ str " as " ++ pr_id x ++ str " in " ++ prl_term t
-
-let pr_pattern_aux pr_constr = function
-  | T t -> pr_constr t
-  | In_T t -> str "in " ++ pr_constr t
-  | X_In_T (x,t) -> pr_constr x ++ str " in " ++ pr_constr t
-  | In_X_In_T (x,t) -> str "in " ++ pr_constr x ++ str " in " ++ pr_constr t
-  | E_In_X_In_T (e,x,t) ->
-      pr_constr e ++ str " in " ++ pr_constr x ++ str " in " ++ pr_constr t
-  | 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_pat (pi3 (nf_open_term sigma sigma t))) p
-let pr_cpattern = pr_term
-let pr_rpattern _ _ _ = pr_pattern
-
-let pr_option f = function None -> mt() | Some x -> f x
-let pr_ssrpattern _ _ _ = pr_option pr_pattern
-let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]")
-let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep
-let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")")
-let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
-
-let wit_rpatternty = add_genarg "rpatternty" pr_pattern
-
-ARGUMENT EXTEND rpattern TYPED AS rpatternty PRINTED BY pr_rpattern
-  | [ lconstr(c) ] -> [ T (mk_lterm c) ]
-  | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c) ]
-  | [ lconstr(x) "in" lconstr(c) ] -> 
-    [ X_In_T (mk_lterm x, mk_lterm c) ]
-  | [ "in" lconstr(x) "in" lconstr(c) ] -> 
-    [ In_X_In_T (mk_lterm x, mk_lterm c) ]
-  | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> 
-    [ E_In_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ]
-  | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> 
-    [ E_As_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ]
-END
-
-type cpattern = char * glob_constr_and_expr
-let tag_of_cpattern = fst
-let loc_of_cpattern = loc_ofCG
-let cpattern_of_term t = t
-type occ = (bool * int list) option
-
-type rpattern = (cpattern, cpattern) ssrpattern
-let pr_rpattern = pr_pattern
-
-type pattern = Evd.evar_map * (Term.constr, Term.constr) ssrpattern
-
-
-let id_of_cpattern = function
-  | _,(_,Some (CRef (Ident (_, x), _))) -> Some x
-  | _,(_,Some (CAppExpl (_, (_, Ident (_, x), _), []))) -> Some x
-  | _,(GRef (_, VarRef x, _) ,None) -> Some x
-  | _ -> None
-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 of_ftactic ftac gl =
-  let r = ref None in
-  let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in
-  let tac = Proofview.V82.of_tactic tac in
-  let { sigma = sigma } = tac gl in
-  let ans = match !r with
-  | None -> assert false (** If the tactic failed we should not reach this point *)
-  | Some ans -> ans
-  in
-  (sigma, ans)
-
-let interp_wit wit ist gl x = 
-  let globarg = in_gen (glbwit wit) x in
-  let arg = interp_genarg ist globarg in
-  let (sigma, arg) = of_ftactic arg gl in
-  sigma, Value.cast (topwit wit) arg
-let interp_constr = interp_wit wit_constr
-let interp_open_constr ist gl gc =
-  interp_wit wit_open_constr ist gl gc
-let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
-let interp_term ist gl (_, c) = (interp_open_constr ist gl c)
-let glob_ssrterm gs = function
-  | k, (_, Some c) -> k, Tacintern.intern_constr gs c
-  | ct -> ct
-let subst_ssrterm s (k, c) = k, Tacsubst.subst_glob_constr_and_expr s c
-let pr_ssrterm _ _ _ = pr_term
-let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
-  | Tok.KEYWORD "(" -> '('
-  | Tok.KEYWORD "@" -> '@'
-  | _ -> ' '
-let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
-
-(* This piece of code asserts the following notations are reserved *)
-(* Reserved Notation "( a 'in' b )"        (at level 0).           *)
-(* Reserved Notation "( a 'as' b )"        (at level 0).           *)
-(* Reserved Notation "( a 'in' b 'in' c )" (at level 0).           *)
-(* Reserved Notation "( a 'as' b 'in' c )" (at level 0).           *)
-let glob_cpattern gs p =
-  pp(lazy(str"globbing pattern: " ++ pr_term p));
-  let glob x = snd (glob_ssrterm gs (mk_lterm x)) in
-  let encode k s l =
-    let name = Name (id_of_string ("_ssrpat_" ^ s)) in
-    k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in
-  let bind_in t1 t2 =
-    let d = dummy_loc in let n = Name (destCVar t1) in
-    fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in
-  let check_var t2 = if not (isCVar t2) then
-    loc_error (constr_loc t2) "Only identifiers are allowed here" in
-  match p with
-  | _, (_, None) as x -> x
-  | k, (v, Some t) as orig ->
-     if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else
-     match t with
-     | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) ->
-         (try match glob t1, glob t2 with
-         | (r1, None), (r2, None) -> encode k "In" [r1;r2]
-         | (r1, Some _), (r2, Some _) when isCVar t1 ->
-             encode k "In" [r1; r2; bind_in t1 t2]
-         | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
-         | _ -> Errors.anomaly (str"where are we?")
-         with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
-     | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) ->
-         check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
-     | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) ->
-         encode k "As" [fst (glob t1); fst (glob t2)]
-     | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) ->
-         check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
-     | _ -> glob_ssrterm gs orig
-;;
-
-let interp_ssrterm _ gl t = Tacmach.project gl, t
-
-ARGUMENT EXTEND cpattern
-     PRINTED BY pr_ssrterm
-     INTERPRETED BY interp_ssrterm
-     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
-     RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm
-     GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" constr(c) ] -> [ mk_lterm c ]
-END
-
-let (!@) = Compat.to_coqloc
-
-GEXTEND Gram
-  GLOBAL: cpattern;
-  cpattern: [[ k = ssrtermkind; c = constr ->
-    let pattern = mk_term k c in
-    if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]];
-END
-
-ARGUMENT EXTEND lcpattern
-     PRINTED BY pr_ssrterm
-     INTERPRETED BY interp_ssrterm
-     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
-     RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm
-     GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" lconstr(c) ] -> [ mk_lterm c ]
-END
-
-GEXTEND Gram
-  GLOBAL: lcpattern;
-  lcpattern: [[ k = ssrtermkind; c = lconstr ->
-    let pattern = mk_term k c in
-    if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]];
-END
-
-let interp_pattern ist gl red redty =
-  pp(lazy(str"interpreting: " ++ pr_pattern red));
-  let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in
-  let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in
-  let eAsXInT e x t = E_As_X_In_T(e,x,t) in
-  let mkG ?(k=' ') x = k,(x,None) in
-  let decode t f g =
-    try match (pf_intern_term ist gl t) with
-    | GCast(_,GHole _,CastConv(GLambda(_,Name x,_,_,c))) -> f x (' ',(c,None))
-    | it -> g t with _ -> g t in
-  let decodeG t f g = decode (mkG t) f g in
-  let bad_enc id _ = Errors.anomaly (str"bad encoding for pattern "++str id) in
-  let cleanup_XinE h x rp sigma =
-    let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in
-    let to_clean, update = (* handle rename if x is already used *)
-      let ctx = pf_hyps gl in
-      let len = Context.Named.length ctx in
-      let name = ref None in
-      try ignore(Context.Named.lookup x ctx); (name, fun k ->
-        if !name = None then
-        let nctx = Evd.evar_context (Evd.find sigma k) in
-        let nlen = Context.Named.length nctx in
-        if nlen > len then begin
-          name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1)))
-        end)
-      with Not_found -> ref (Some x), fun _ -> () in
-    let sigma0 = project gl in
-    let new_evars =
-      let rec aux acc t = match kind_of_term t with
-      | Evar (k,_) ->
-          if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else
-          (update k; k::acc)
-      | _ -> fold_constr aux acc t in 
-      aux [] (Evarutil.nf_evar sigma rp) in
-    let sigma = 
-      List.fold_left (fun sigma e ->
-        if Evd.is_defined sigma e then sigma else (* clear may be recursive *)
-        if Option.is_empty !to_clean then sigma else
-        let name = Option.get !to_clean in
-        pp(lazy(pr_id name));
-        try snd(Logic.prim_refiner (Proof_type.Thin [name]) sigma e)
-        with Evarutil.ClearDependencyError _ -> sigma)
-      sigma new_evars in
-    sigma in
-  let red = match red with
-    | T(k,(GCast (_,GHole _,(CastConv(GLambda (_,Name id,_,_,t)))),None))
-        when let id = string_of_id id in let len = String.length id in
-        (len > 8 && String.sub id 0 8 = "_ssrpat_") ->
-        let id = string_of_id id in let len = String.length id in
-        (match String.sub id 8 (len - 8), t with
-        | "In", GApp(_, _, [t]) -> decodeG t xInT (fun x -> T x)
-        | "In", GApp(_, _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id)
-        | "In", GApp(_, _, [e; t; e_in_t]) ->
-            decodeG t (eInXInT (mkG e))
-              (fun _ -> decodeG e_in_t xInT (fun _ -> assert false))
-        | "As", GApp(_, _, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
-        | _ -> bad_enc id ())
-    | T t -> decode t xInT (fun x -> T x)
-    | In_T t -> decode t inXInT inT
-    | X_In_T (e,t) -> decode t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x)
-    | In_X_In_T (e,t) -> inXInT (id_of_Cterm e) t
-    | E_In_X_In_T (e,x,rp) -> eInXInT e (id_of_Cterm x) rp
-    | E_As_X_In_T (e,x,rp) -> eAsXInT e (id_of_Cterm x) rp in
-  pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red));
-  let red = match redty with None -> red | Some ty -> let ty = ' ', ty in
-  match red with
-  | T t -> T (combineCG t ty (mkCCast (loc_ofCG t)) mkRCast)
-  | X_In_T (x,t) ->
-      let ty = pf_intern_term ist gl ty in
-      E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t)
-  | E_In_X_In_T (e,x,t) ->
-      let ty = mkG (pf_intern_term ist gl ty) in
-      E_In_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t)
-  | E_As_X_In_T (e,x,t) ->
-      let ty = mkG (pf_intern_term ist gl ty) in
-      E_As_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t)
-  | red -> red in
-  pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
-  let mkXLetIn loc x (a,(g,c)) = match c with
-  | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b))
-  | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in
-  match red with
-  | T t -> let sigma, t = interp_term ist gl t in sigma, T t
-  | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
-  | X_In_T (x, rp) | In_X_In_T (x, rp) ->
-    let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in
-    let rp = mkXLetIn dummy_loc (Name x) rp in
-    let sigma, rp = interp_term ist gl rp in
-    let _, h, _, rp = destLetIn rp in
-    let sigma = cleanup_XinE h x rp sigma in
-    let rp = subst1 h (Evarutil.nf_evar sigma rp) in
-    sigma, mk h rp
-  | E_In_X_In_T(e, x, rp) | E_As_X_In_T (e, x, rp) ->
-    let mk e x p =
-      match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in
-    let rp = mkXLetIn dummy_loc (Name x) rp in
-    let sigma, rp = interp_term ist gl rp in
-    let _, h, _, rp = destLetIn rp in
-    let sigma = cleanup_XinE h x rp sigma in
-    let rp = subst1 h (Evarutil.nf_evar sigma rp) in
-    let sigma, e = interp_term ist (re_sig (sig_it gl) sigma) e in
-    sigma, mk e h rp
-;;
-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,[])
-
-(* calls do_subst on every sub-term identified by (pattern,occ) *)
-let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
-  let fs sigma x = Reductionops.nf_evar sigma x in
-  let pop_evar sigma e p =
-    let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in
-    let e_body = match e_body with Evar_defined c -> c
-    | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++
-          str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++
-          str "Does the variable bound by the \"in\" construct occur "++
-          str "in the pattern?") in
-    let sigma = 
-      Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in
-    sigma, e_body in
-  let ex_value hole =
-    match kind_of_term hole with Evar (e,_) -> e | _ -> assert false in
-  let mk_upat_for ?hack env sigma0 (sigma, t) ?(p=t) ok =
-    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
-  | Some (sigma, (T rp | In_T rp)) -> 
-    let rp = fs sigma rp in
-    let ise = create_evar_defs sigma in
-    let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in
-    let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in
-    let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in
-    let concl = find_T env0 concl0 1 do_subst in
-    let _ = end_T () in
-    concl
-  | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) ->
-    let p = fs sigma p in
-    let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in
-    let ex = ex_value hole in
-    let rp = mk_upat_for ~hack:true env0 sigma0 (sigma, p) all_ok in
-    let find_T, end_T = mk_tpattern_matcher sigma0 noindex rp in
-    (* 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 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 _ -> do_subst env e_body))) in
-    let _ = end_X () in let _ = end_T () in 
-    concl
-  | Some (sigma, E_In_X_In_T (e, hole, p)) ->
-    let p, e = fs sigma p, fs sigma e in
-    let ex = ex_value hole in
-    let rp = mk_upat_for ~hack:true env0 sigma0 (sigma, p) all_ok in
-    let find_T, end_T = 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 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 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 ->
-        find_E env e_body h do_subst))) in
-    let _ = end_E () in let _ = end_X () in let _ = end_T () in
-    concl
-  | Some (sigma, E_As_X_In_T (e, hole, p)) ->
-    let p, e = fs sigma p, fs sigma e in
-    let ex = ex_value hole in
-    let rp = 
-      let e_sigma = unify_HO env0 sigma hole e in
-      e_sigma, fs e_sigma p in
-    let rp = mk_upat_for ~hack:true env0 sigma0 rp all_ok in
-    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 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 ->
-        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
-    let _ = end_X () in let _ = end_TE () in
-    concl
-;;
-
-let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
-  let e = match p with
-  | In_T _ | In_X_In_T _ -> Errors.anomaly (str"pattern without redex")
-  | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in
-  let sigma =
-    if not resolve_typeclasses then sigma
-    else Typeclasses.resolve_typeclasses ~fail:false env sigma in
-  Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma
-
-let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
-  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
-  e, cl
-;;
-
-(* clenup interface for external use *)
-let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = 
-  mk_tpattern ?p_origin env sigma0 sigma_t f dir c
-;;
-
-let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
- let ise = create_evar_defs sigma in
- 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 rdx, _, (sigma, uc, p) = end_U () in
- sigma, uc, p, concl, rdx
-
-let fill_occ_term env cl occ sigma0 (sigma, t) =
-  try
-    let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in
-    if sigma' != sigma0 then Errors.error "matching impacts evars"
-    else cl, (Evd.merge_universe_context sigma' uc, t')
-  with NoMatch -> try
-    let sigma', uc, t' =
-      unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in
-    if sigma' != sigma0 then raise NoMatch
-    else cl, (Evd.merge_universe_context sigma' uc, t')
-  with _ ->
-    errorstrm (str "partial term " ++ pr_constr_pat t
-            ++ str " does not match any subterm of the goal")
-
-let pf_fill_occ_term gl occ t =
-  let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in
-  let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
-  cl, t
-
-let cpattern_of_id id = ' ', (GRef (dummy_loc, VarRef  id, None), None)
-
-let is_wildcard = function
-  | _,(_,Some (CHole _)|GHole _,None) -> true
-  | _ -> false
-
-(* "ssrpattern" *)
-let pr_ssrpatternarg _ _ _ cpat = pr_rpattern cpat
-
-ARGUMENT EXTEND ssrpatternarg
-  TYPED AS rpattern
-  PRINTED BY pr_ssrpatternarg
-| [ "[" rpattern(pat) "]" ] -> [ pat ]
-END
-  
-let pf_merge_uc uc gl =
-  re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc)
-
-let pf_unsafe_merge_uc uc gl =
-  re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc)
-
-let ssrpatterntac ist arg gl =
-  let pat = interp_rpattern ist gl arg in
-  let sigma0 = project gl in
-  let concl0 = pf_concl gl in
-  let (t, uc), concl_x =
-    fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
-  let gl, tty = pf_type_of gl t in
-  let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
-  Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
-
-(* Register "ssrpattern" tactic *)
-let () =
-  let mltac _ ist =
-    let arg =
-      let v = Id.Map.find (Names.Id.of_string "ssrpatternarg") ist.lfun in
-      Value.cast (topwit wit_ssrpatternarg) v in
-    Proofview.V82.tactic (ssrpatterntac ist arg) in
-  let name = { mltac_plugin = "ssrmatching"; mltac_tactic = "ssrpattern"; } in
-  let () = Tacenv.register_ml_tactic name [|mltac|] in
-  let tac =
-    TacFun ([Some (Id.of_string "ssrpatternarg")],
-      TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in
-  let obj () =
-    Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
-  Mltop.declare_cache_obj obj "ssreflect"
-
-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   *)
-(* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
-(* consequence the extended ssreflect grammar.                             *)
-let () = Lexer.unfreeze frozen_lexer ;;
-
-(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
deleted file mode 100644
index 74a603e..0000000
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
+++ /dev/null
@@ -1,241 +0,0 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-
-open Genarg
-open Tacexpr
-open Environ
-open Tacmach
-open Evd
-open Proof_type
-open Term
-
-(** ******** Small Scale Reflection pattern matching facilities ************* *)
-
-(** Pattern parsing *)
-
-(** The type of context patterns, the patterns of the [set] tactic and 
-    [:] tactical. These are patterns that identify a precise subterm. *)
-type cpattern
-val pr_cpattern : cpattern -> Pp.std_ppcmds
-
-(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
-val cpattern         : cpattern Pcoq.Gram.entry
-val wit_cpattern     : cpattern uniform_genarg_type
-
-(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
-val lcpattern         : cpattern Pcoq.Gram.entry
-val wit_lcpattern     : cpattern uniform_genarg_type
-
-(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
-    These patterns also include patterns that identify all the subterms
-    of a context (i.e. "in" prefix) *)
-type rpattern
-val pr_rpattern : rpattern -> Pp.std_ppcmds
-
-(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
-val rpattern         : rpattern Pcoq.Gram.entry
-val wit_rpattern     : rpattern uniform_genarg_type
-
-(** Pattern interpretation and matching *)
-
-exception NoMatch
-exception NoProgress
-
-(** AST for [rpattern] (and consequently [cpattern]) *)
-type ('ident, 'term) ssrpattern =
-  | T of 'term
-  | In_T of 'term
-  | X_In_T of 'ident * 'term
-  | In_X_In_T of 'ident * 'term
-  | E_In_X_In_T of 'term * 'ident * 'term
-  | E_As_X_In_T of 'term * 'ident * 'term
-
-type pattern = evar_map * (constr, constr) ssrpattern
-val pp_pattern : pattern -> Pp.std_ppcmds
-
-(** Extracts the redex and applies to it the substitution part of the pattern.
-  @raise Anomaly if called on [In_T] or [In_X_In_T] *)
-val redex_of_pattern :
-  ?resolve_typeclasses:bool -> env -> pattern ->
-     constr Evd.in_evar_universe_context
-
-(** [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 sigma ->
-  rpattern ->
-    pattern
-
-(** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat]
-    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 sigma ->
-  cpattern -> glob_constr_and_expr option ->
-    pattern
-
-(** The set of occurrences to be matched. The boolean is set to true
- *  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
-
-(** [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 
-    binders traversed. If [pat] is [None] then then subst is called on [t].
-    [t] must live in [env] and [sigma], [pat] must have been interpreted in 
-    (an extension of) [sigma]. 
-  @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false])
-  @return [t] where all [occ] occurrences of [pat] have been mapped using
-    [subst] *)
-val eval_pattern :
-  ?raise_NoMatch:bool ->
-  env -> evar_map -> constr ->
-  pattern option -> occ -> subst ->
-    constr
-
-(** [fill_occ_pattern b env sigma t pat occ h] is a simplified version of 
-    [eval_pattern]. 
-    It replaces all [occ] occurrences of [pat] in [t] with Rel [h]. 
-    [t] must live in [env] and [sigma], [pat] must have been interpreted in 
-    (an extension of) [sigma]. 
-  @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) 
-  @return the instance of the redex of [pat] that was matched and [t]
-    transformed as described above. *)
-val fill_occ_pattern :
-  ?raise_NoMatch:bool ->
-  env -> evar_map -> constr ->
-  pattern -> occ -> int ->
-    constr Evd.in_evar_universe_context * constr
-
-(** *************************** Low level APIs ****************************** *)
-
-(* The primitive matching facility. It matches of a term with holes, like 
-   the T pattern above, and calls a continuation on its occurrences. *)
-
-type ssrdir = L2R | R2L
-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] 
-    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.
-  @return the compiled [tpattern] and its [evar_map]
-  @raise UserEerror is the pattern is a wildcard *)
-val mk_tpattern :
-  ?p_origin:ssrdir * constr ->
-  env -> evar_map ->
-  evar_map * constr ->
-  (constr -> evar_map -> bool) ->
-  ssrdir -> constr ->
-    evar_map * tpattern
-
-(** [findP env t i k] is a stateful function that finds the next occurrence 
-    of a tpattern and calls the callback [k] to map the subterm matched. 
-    The [int] argument passed to [k] is the number of binders traversed so far 
-    plus the initial value [i]. 
-  @return [t] where the subterms identified by the selected occurrences of 
-    the patter have been mapped using [k]
-  @raise NoMatch if the raise_NoMatch flag given to [mk_tpattern_matcher] is
-    [true] and if the pattern did not match 
-  @raise UserEerror if the raise_NoMatch flag given to [mk_tpattern_matcher] is
-    [false] and if the pattern did not match *)
-type find_P =
-  env -> constr -> int -> k:subst -> constr
-
-(** [conclude ()] asserts that all mentioned ocurrences have been visited.
-  @return the instance of the pattern, the evarmap after the pattern
-    instantiation, the proof term and the ssrdit stored in the tpattern
-  @raise UserEerror if too many occurrences were specified *)
-type conclude =
-  unit -> constr * ssrdir * (evar_map * Evd.evar_universe_context * constr)
-
-(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair 
-    a function [find_P] and [conclude] with the behaviour explained above.
-    The flag [b] (default [false]) changes the error reporting behaviour
-    of [find_P] if none of the [tpattern] matches. The argument [o] can
-    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 ->
-    find_P * conclude
-
-(** Example of [mk_tpattern_matcher] to implement 
-    [rewrite \{occ\}\[in t\]rules].
-    It first matches "in t" (called [pat]), then in all matched subterms 
-    it matches the LHS of the rules using [find_R].
-    [concl0] is the initial goal, [concl] will be the goal where some terms
-    are replaced by a De Bruijn index. The [rw_progress] extra check
-    selects only occurrences that are not rewritten to themselves (e.g.
-    an occurrence "x + x" rewritten with the commutativity law of addition 
-    is skipped) {[
-  let find_R, conclude = match pat with
-  | Some (_, In_T _) ->
-      let aux (sigma, pats) (d, r, lhs, rhs) =
-        let sigma, pat = 
-          mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in
-        sigma, pats @ [pat] in
-      let rpats = List.fold_left aux (r_sigma, []) rules in
-      let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in
-      find_R ~k:(fun _ _ h -> mkRel h), 
-      fun cl -> let rdx, d, r = end_R () in (d,r),rdx
-  | _ -> ... in
-  let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in
-  let (d, r), rdx = conclude concl in ]} *)
-
-(* 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 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
-
-(** Helpers to make stateful closures. Example: a [find_P] function may be 
-    called many times, but the pattern instantiation phase is performed only the
-    first time. The corresponding [conclude] has to return the instantiated
-    pattern redex. Since it is up to [find_P] to raise [NoMatch] if the pattern
-    has no instance, [conclude] considers it an anomaly if the pattern did
-    not match *)
-
-(** [do_once r f] calls [f] and updates the ref only once *)
-val do_once : 'a option ref -> (unit -> 'a) -> unit
-(** [assert_done r] return the content of r. @raise Anomaly is r is [None] *)
-val assert_done : 'a option ref -> 'a
-
-(** Very low level APIs.
-    these are calls to evarconv's [the_conv_x] followed by
-    [consider_remaining_unif_problems] and [resolve_typeclasses].
-    In case of failure they raise [NoMatch] *)
-
-val unify_HO : env -> evar_map -> constr -> constr -> evar_map
-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_pattern : pattern -> Names.variable option
-val is_wildcard : cpattern -> bool
-val cpattern_of_id : Names.variable -> cpattern
-val cpattern_of_id : Names.variable -> cpattern
-val pr_constr_pat : constr -> Pp.std_ppcmds
-val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma
-val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma
-
-(* One can also "Set SsrMatchingDebug" from a .v *)
-val debug : bool -> unit
-
-(* One should delimit a snippet with "Set SsrMatchingProfiling" and
- * "Unset SsrMatchingProfiling" to get timings *)
-val profile : bool -> unit
-
-(* eof *)