Merge branch 'master' into econstr

15 files changed, 17 insertions, 3145 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
deleted file mode 100644
index 29ecb94ca..000000000
--- a/plugins/decl_mode/decl_expr.mli
+++ /dev/null
@@ -1,102 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Tacexpr
-
-type 'it statement =
-    {st_label:Name.t;
-     st_it:'it}
-
-type thesis_kind =
-    Plain
-  | For of Id.t
-
-type 'this or_thesis =
-    This of 'this
-  | Thesis of thesis_kind
-
-type side = Lhs | Rhs
-
-type elim_type =
-    ET_Case_analysis
-  | ET_Induction
-
-type block_type =
-    B_proof
-  | B_claim
-  | B_focus
-  | B_elim of elim_type
-
-type ('it,'constr,'tac) cut =
-    {cut_stat: 'it;
-     cut_by: 'constr list option;
-     cut_using: 'tac option}
-
-type ('var,'constr) hyp =
-    Hvar of 'var
-  | Hprop of 'constr statement
-
-type ('constr,'tac) casee =
-    Real of 'constr
-  | Virtual of ('constr statement,'constr,'tac) cut
-
-type ('var,'constr,'pat,'tac) bare_proof_instr =
-  | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr
-  | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr
-  | Phence of ('var,'constr,'pat,'tac) bare_proof_instr
-  | Pcut of ('constr or_thesis statement,'constr,'tac) cut
-  | Prew of side * ('constr statement,'constr,'tac) cut
-  | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
-  | Passume of ('var,'constr) hyp list
-  | Plet of ('var,'constr) hyp list
-  | Pgiven of ('var,'constr) hyp list
-  | Pconsider of 'constr*('var,'constr) hyp list
-  | Pclaim of 'constr statement
-  | Pfocus of 'constr statement
-  | Pdefine of Id.t * 'var list * 'constr
-  | Pcast of Id.t or_thesis * 'constr
-  | Psuppose of ('var,'constr) hyp list
-  | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list)
-  | Ptake of 'constr list
-  | Pper of elim_type * ('constr,'tac) casee
-  | Pend of block_type
-  | Pescape
-
-type emphasis = int
-
-type ('var,'constr,'pat,'tac) gen_proof_instr=
-    {emph: emphasis;
-     instr: ('var,'constr,'pat,'tac) bare_proof_instr }
-
-
-type raw_proof_instr =
-    ((Id.t * (Constrexpr.constr_expr option)) Loc.located,
-     Constrexpr.constr_expr,
-     Constrexpr.cases_pattern_expr,
-     raw_tactic_expr) gen_proof_instr
-
-type glob_proof_instr =
-    ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located,
-     Tacexpr.glob_constr_and_expr,
-     Constrexpr.cases_pattern_expr,
-     Tacexpr.glob_tactic_expr) gen_proof_instr
-
-type proof_pattern =
-    {pat_vars: Term.types statement list;
-     pat_aliases: (Term.constr*Term.types) statement list;
-     pat_constr: Term.constr;
-     pat_typ: Term.types;
-     pat_pat: Glob_term.cases_pattern;
-     pat_expr: Constrexpr.cases_pattern_expr}
-
-type proof_instr =
-    (Term.constr statement,
-     Term.constr,
-     proof_pattern,
-     Geninterp.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
deleted file mode 100644
index a29480a55..000000000
--- a/plugins/decl_mode/decl_interp.ml
+++ /dev/null
@@ -1,471 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Util
-open Names
-open Constrexpr
-open Tacintern
-open Decl_expr
-open Decl_mode
-open Pretyping
-open Glob_term
-open Term
-open Vars
-open Pp
-open Decl_kinds
-open Misctypes
-
-(* INTERN *)
-
-let glob_app (loc,hd,args) = if List.is_empty args then hd else GApp(loc,hd,args)
-
-let intern_justification_items globs =
-  Option.map (List.map (intern_constr globs))
-
-let intern_justification_method globs =
-  Option.map (intern_pure_tactic globs)
-
-let intern_statement intern_it globs st =
-  {st_label=st.st_label;
-   st_it=intern_it globs st.st_it}
-
-let intern_no_bind intern_it globs x =
-  globs,intern_it globs x
-
-let intern_constr_or_thesis globs = function
-    Thesis n -> Thesis n
-  | This c -> This (intern_constr globs c)
-
-let add_var id globs=
-    {globs with ltacvars = Id.Set.add id globs.ltacvars}
-
-let add_name nam globs=
- match nam with
-     Anonymous -> globs
-   | Name id -> add_var id globs
-
-let intern_hyp iconstr globs = function
-    Hvar (loc,(id,topt)) -> add_var id globs,
-      Hvar (loc,(id,Option.map (intern_constr globs) topt))
-  | Hprop st -> add_name st.st_label globs,
-      Hprop (intern_statement iconstr globs st)
-
-let intern_hyps iconstr globs hyps =
-  snd (List.fold_map (intern_hyp iconstr) globs hyps)
-
-let intern_cut intern_it globs cut=
-  let nglobs,nstat=intern_it globs cut.cut_stat in
-    {cut_stat=nstat;
-     cut_by=intern_justification_items nglobs cut.cut_by;
-     cut_using=intern_justification_method nglobs cut.cut_using}
-
-let intern_casee globs = function
-    Real c -> Real (intern_constr globs c)
-  | Virtual cut -> Virtual
-      (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut)
-
-let intern_hyp_list args globs =
-  let intern_one globs (loc,(id,opttyp)) =
-    (add_var id globs),
-    (loc,(id,Option.map (intern_constr globs) opttyp)) in
-  List.fold_map intern_one globs args
-
-let intern_suffices_clause globs (hyps,c) =
-  let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in
-    nglobs,(nhyps,intern_constr_or_thesis nglobs c)
-
-let intern_fundecl args body globs=
-  let nglobs,nargs = intern_hyp_list args globs in
-    nargs,intern_constr nglobs body
-
-let rec add_vars_of_simple_pattern globs = function
-    CPatAlias (loc,p,id) ->
-      add_vars_of_simple_pattern (add_var id globs) p
-(*      Loc.raise loc
-	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
-  | CPatOr (loc, _)->
-      Loc.raise ~loc
-	(UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
-  | CPatDelimiters (_,_,p) ->
-      add_vars_of_simple_pattern globs p
-  | CPatCstr (_,_,pl1,pl2) ->
-    List.fold_left add_vars_of_simple_pattern
-      (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2
-  | CPatNotation(_,_,(pl,pll),pl') ->
-      List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll))
-  | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
-  |  _  -> globs
-
-let rec intern_bare_proof_instr globs = function
-    Pthus i -> Pthus (intern_bare_proof_instr globs i)
-  | Pthen i -> Pthen (intern_bare_proof_instr globs i)
-  | Phence i -> Phence (intern_bare_proof_instr globs i)
-  | Pcut c -> Pcut
-      (intern_cut
-	 (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c)
-  | Psuffices c ->
-      Psuffices (intern_cut intern_suffices_clause globs c)
-  | Prew (s,c) -> Prew
-      (s,intern_cut
-	 (intern_no_bind  (intern_statement intern_constr)) globs c)
-  | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
-  | Pcase (params,pat,hyps) ->
-      let nglobs,nparams = intern_hyp_list params globs in
-      let nnglobs= add_vars_of_simple_pattern nglobs pat in
-      let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in
-	Pcase (nparams,pat,nhyps)
-  | Ptake witl -> Ptake (List.map (intern_constr globs) witl)
-  | Pconsider (c,hyps) -> Pconsider (intern_constr globs c,
-				      intern_hyps intern_constr globs hyps)
-  | Pper (et,c) -> Pper (et,intern_casee globs c)
-  | Pend bt -> Pend bt
-  | Pescape -> Pescape
-  | Passume hyps -> Passume (intern_hyps intern_constr globs hyps)
-  | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps)
-  | Plet hyps -> Plet (intern_hyps intern_constr globs hyps)
-  | Pclaim st -> Pclaim (intern_statement intern_constr globs st)
-  | Pfocus st -> Pfocus (intern_statement intern_constr globs st)
-  | Pdefine (id,args,body) ->
-      let nargs,nbody = intern_fundecl args body globs in
-	Pdefine (id,nargs,nbody)
-  | Pcast (id,typ) ->
-      Pcast (id,intern_constr globs typ)
-
-let intern_proof_instr globs instr=
-  {emph = instr.emph;
-   instr = intern_bare_proof_instr globs instr.instr}
-
-(* INTERP *)
-
-let interp_justification_items env sigma =
-    Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c))))
-
-let interp_constr check_sort env sigma c =
-  if check_sort then
-    fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *))
-  else
-    fst (understand env sigma (fst c))
-
-let special_whd env =
-  let infos=CClosure.create_clos_infos CClosure.all env in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
-
-let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
-
-let decompose_eq env id =
-  let typ = Environ.named_type id env in
-  let whd = special_whd env typ in
-    match kind_of_term whd with
-	App (f,args)->
-	  if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
-	  then args.(0)
-	  else error "Previous step is not an equality."
-      | _ -> error "Previous step is not an equality."
-
-let get_eq_typ info env =
-  let typ = decompose_eq env (get_last env) in
-    typ
-
-let interp_constr_in_type typ env sigma c =
-  fst (understand env sigma (fst c) ~expected_type:(OfType (EConstr.of_constr typ)))(*FIXME*)
-
-let interp_statement interp_it env sigma st =
-  {st_label=st.st_label;
-   st_it=interp_it env sigma st.st_it}
-
-let interp_constr_or_thesis check_sort env sigma = function
-    Thesis n -> Thesis n
-  | This c -> This (interp_constr check_sort env sigma c)
-
-let abstract_one_hyp inject h glob =
-  match h with
-      Hvar (loc,(id,None)) ->
-	GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
-    | Hvar (loc,(id,Some typ)) ->
-	GProd (Loc.ghost,Name id, Explicit, fst typ, glob)
-    | Hprop st ->
-	GProd (Loc.ghost,st.st_label, Explicit, inject st.st_it, glob)
-
-let glob_constr_of_hyps inject hyps head =
-  List.fold_right (abstract_one_hyp inject) hyps head
-
-let glob_prop = GSort (Loc.ghost,GProp)
-
-let rec match_hyps blend names constr = function
-    [] -> [],substl names constr
-  | hyp::q ->
-      let (name,typ,body)=destProd constr in
-      let st= {st_label=name;st_it=substl names typ} in
-      let qnames=
-	match name with
-	    Anonymous -> mkMeta 0 :: names
-	  | Name id -> mkVar id :: names in
-      let qhyp = match hyp with
-	  Hprop st' -> Hprop (blend st st')
-	| Hvar _ -> Hvar st in
-      let rhyps,head = match_hyps blend qnames body q in
-	qhyp::rhyps,head
-
-let interp_hyps_gen inject blend env sigma hyps head =
-  let constr= fst(*FIXME*) (understand env sigma (glob_constr_of_hyps inject hyps head)) in
-    match_hyps blend [] constr hyps
-
-let interp_hyps env sigma hyps = fst (interp_hyps_gen fst (fun x _ -> x) env sigma hyps glob_prop)
-
-let dummy_prefix= Id.of_string "__"
-
-let rec deanonymize ids =
-  function
-      PatVar (loc,Anonymous) ->
-	let (found,known) = !ids in
-	let new_id=Namegen.next_ident_away dummy_prefix known in
-	let _= ids:= (loc,new_id) :: found , new_id :: known in
-	  PatVar (loc,Name new_id)
-    | PatVar (loc,Name id) as pat ->
-	let (found,known) = !ids in
-	let _= ids:= (loc,id) :: found , known in
-	  pat
-    | PatCstr(loc,cstr,lpat,nam) ->
-	PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
-
-let rec glob_of_pat =
-  function
-      PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable")
-    | PatVar (loc,Name id) ->
-	  GVar (loc,id)
-    | PatCstr(loc,((ind,_) as cstr),lpat,_) ->
-	let mind= fst (Global.lookup_inductive ind) in
-	let rec add_params n q =
-	  if n<=0 then q else
-	    add_params (pred n) (GHole(Loc.ghost,
-				       Evar_kinds.TomatchTypeParameter(ind,n), Misctypes.IntroAnonymous, None)::q) in
-	    let args = List.map glob_of_pat lpat in
-	      glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None),
-		   add_params mind.Declarations.mind_nparams args)
-
-let prod_one_hyp = function
-    (loc,(id,None)) ->
-      (fun glob ->
-	 GProd (Loc.ghost,Name id, Explicit,
-		GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob))
-  | (loc,(id,Some typ)) ->
-      (fun glob ->
-	 GProd (Loc.ghost,Name id, Explicit, fst typ, glob))
-
-let prod_one_id (loc,id) glob =
-  GProd (Loc.ghost,Name id, Explicit,
-	 GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
-
-let let_in_one_alias (id,pat) glob =
-  GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob)
-
-let rec bind_primary_aliases map pat =
-  match pat with
-      PatVar (_,_) -> map
-    | PatCstr(loc,_,lpat,nam) ->
-	let map1 =
-	  match nam with
-	      Anonymous -> map
-	    | Name id -> (id,pat)::map
-	in
-	  List.fold_left bind_primary_aliases map1 lpat
-
-let bind_secondary_aliases map subst =
-  Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map
-
-let bind_aliases patvars subst patt =
-  let map = bind_primary_aliases [] patt in
-  let map1 = bind_secondary_aliases map subst in
-  List.rev map1
-
-let interp_pattern env pat_expr =
-  let patvars,pats = Constrintern.intern_pattern env pat_expr in
-    match pats with
-	[] -> anomaly (Pp.str "empty pattern list")
-      | [subst,patt] ->
-	  (patvars,bind_aliases patvars subst patt,patt)
-      | _  -> anomaly (Pp.str "undetected disjunctive pattern")
-
-let rec match_args dest names constr = function
-    [] -> [],names,substl names constr
-  | _::q ->
-      let (name,typ,body)=dest constr in
-      let st={st_label=name;st_it=substl names typ} in
-      let qnames=
-	match name with
-	    Anonymous -> assert  false
-	  | Name id -> mkVar id :: names in
-      let args,bnames,body = match_args dest qnames body q in
-	st::args,bnames,body
-
-let rec match_aliases names constr = function
-    [] -> [],names,substl names constr
-  | _::q ->
-      let (name,c,typ,body)=destLetIn constr in
-      let st={st_label=name;st_it=(substl names c,substl names typ)} in
-      let qnames=
-	match name with
-	    Anonymous -> assert false
-	  | Name id -> mkVar id :: names in
-      let args,bnames,body = match_aliases qnames body q in
-	st::args,bnames,body
-
-let detype_ground env c = Detyping.detype false [] env Evd.empty (EConstr.of_constr c)
-
-let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
-  let et,pinfo =
-    match info.pm_stack with
-	Per(et,pi,_,_)::_ -> et,pi
-      | _ -> error "No proof per cases/induction/inversion in progress." in
-  let mib,oib=Global.lookup_inductive  pinfo.per_ind in
-  let num_params = pinfo.per_nparams in
-  let _ =
-    let expected = mib.Declarations.mind_nparams - num_params in
-      if not (Int.equal (List.length params) expected) then
-	user_err ~hdr:"suppose it is" 
-	  (str "Wrong number of extra arguments: " ++ 
-	     (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
-	     str "expected.") in
-  let app_ind =
-    let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
-    let rparams = List.map (detype_ground env) pinfo.per_params in
-    let rparams_rec =
-      List.map
-	(fun (loc,(id,_)) ->
-	   GVar (loc,id)) params in
-    let dum_args=
-      List.init oib.Declarations.mind_nrealargs
-	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),Misctypes.IntroAnonymous, None)) in
-      glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
-  let pat_vars,aliases,patt = interp_pattern env pat in
-  let inject = function
-      Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
-    | Thesis (For rec_occ) ->
-	if not (Id.List.mem rec_occ pat_vars) then
-	  user_err ~hdr:"suppose it is"
-	    (str "Variable " ++ Nameops.pr_id rec_occ ++
-	       str " does not occur in pattern.");
-	Glob_term.GSort(Loc.ghost,GProp)
-    | This (c,_) -> c in
-  let term1 = glob_constr_of_hyps inject hyps glob_prop in
-  let loc_ids,npatt =
-    let rids=ref ([],pat_vars) in
-    let npatt= deanonymize rids patt in
-      List.rev (fst !rids),npatt in
-  let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in
-  let term3=List.fold_right let_in_one_alias aliases term2 in
-  let term4=List.fold_right prod_one_id loc_ids term3 in
-  let term5=List.fold_right prod_one_hyp params term4 in
-  let constr = fst (understand env sigma term5)(*FIXME*) in
-  let tparams,nam4,rest4 = match_args destProd [] constr params in
-  let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
-  let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
-  let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
-  let blend st st' =
-    match st'.st_it with
-	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
-      | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
-  let thyps = fst (match_hyps blend nam2 (Vars.lift (-1) rest1) hyps) in
-    tparams,{pat_vars=tpatvars;
-	     pat_aliases=taliases;
-	     pat_constr=pat_pat;
-	     pat_typ=pat_typ;
-	     pat_pat=patt;
-	     pat_expr=pat},thyps
-
-let interp_cut interp_it env sigma cut=
-  let nenv,nstat = interp_it env sigma cut.cut_stat in
-    { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
-       cut_stat=nstat;
-       cut_by=interp_justification_items nenv sigma cut.cut_by}
-
-let interp_no_bind interp_it env sigma x =
-  env,interp_it env sigma x
-
-let interp_suffices_clause env sigma (hyps,cot)=
-  let (locvars,_) as res =
-    match cot with
-	This (c,_) ->
-	  let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in
-	  nhyps,This nc
-      | Thesis Plain as th  -> interp_hyps env sigma hyps,th
-      | Thesis (For n) -> error "\"thesis for\" is not applicable here." in
-  let push_one hyp env0 =
-    match hyp with
-	(Hprop st | Hvar st) ->
-	  match st.st_label with
-	      Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0
-	    | _ -> env in
-  let nenv = List.fold_right push_one locvars env in
-    nenv,res
-
-let interp_casee env sigma = function
-    Real c -> Real (fst (understand env sigma (fst c)))(*FIXME*)
-  | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) env sigma cut)
-
-let abstract_one_arg = function
-    (loc,(id,None)) ->
-      (fun glob ->
-	 GLambda (Loc.ghost,Name id, Explicit,
-		GHole (loc,Evar_kinds.BinderType (Name id),Misctypes.IntroAnonymous,None), glob))
-  | (loc,(id,Some typ)) ->
-      (fun glob ->
-	 GLambda (Loc.ghost,Name id, Explicit, fst typ, glob))
-
-let glob_constr_of_fun args body =
-  List.fold_right abstract_one_arg args (fst body)
-
-let interp_fun env sigma args body =
-  let constr=fst (*FIXME*) (understand env sigma (glob_constr_of_fun args body)) in
-    match_args destLambda [] constr args
-
-let rec interp_bare_proof_instr info env sigma = function
-    Pthus i -> Pthus (interp_bare_proof_instr info env sigma i)
-  | Pthen i -> Pthen (interp_bare_proof_instr info env sigma i)
-  | Phence i -> Phence (interp_bare_proof_instr info env sigma i)
-  | Pcut c -> Pcut (interp_cut
-		      (interp_no_bind (interp_statement
-					 (interp_constr_or_thesis true)))
-		      env sigma c)
-  | Psuffices c ->
-      Psuffices (interp_cut interp_suffices_clause env sigma c)
-  | Prew (s,c) -> Prew (s,interp_cut
-			  (interp_no_bind (interp_statement
-			     (interp_constr_in_type (get_eq_typ info env))))
-			  env sigma c)
-
-  | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps)
-  | Pcase (params,pat,hyps) ->
-      let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in
-	Pcase (tparams,tpat,thyps)
-  | Ptake witl ->
-      Ptake (List.map (fun c -> fst (*FIXME*) (understand env sigma (fst c))) witl)
-  | Pconsider (c,hyps) -> Pconsider (interp_constr false env sigma c,
-				     interp_hyps env sigma hyps)
-  | Pper (et,c) -> Pper (et,interp_casee env sigma c)
-  | Pend bt -> Pend bt
-  | Pescape -> Pescape
-  | Passume hyps -> Passume (interp_hyps env sigma hyps)
-  | Pgiven hyps -> Pgiven (interp_hyps env sigma hyps)
-  | Plet hyps -> Plet (interp_hyps env sigma hyps)
-  | Pclaim st -> Pclaim (interp_statement (interp_constr true) env sigma st)
-  | Pfocus st -> Pfocus (interp_statement (interp_constr true) env sigma st)
-  | Pdefine (id,args,body) ->
-      let nargs,_,nbody = interp_fun env sigma args body in
-	Pdefine (id,nargs,nbody)
-  | Pcast (id,typ) ->
-      Pcast(id,interp_constr true env sigma typ)
-
-let interp_proof_instr info env sigma instr=
-  {emph = instr.emph;
-   instr = interp_bare_proof_instr info env sigma instr.instr}
-
-
-
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
deleted file mode 100644
index 4303ecdb4..000000000
--- a/plugins/decl_mode/decl_interp.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Tacintern
-open Decl_expr
-
-
-val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
-val interp_proof_instr : Decl_mode.pm_info ->
-  Environ.env -> Evd.evar_map -> glob_proof_instr -> proof_instr
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
deleted file mode 100644
index 92d408901..000000000
--- a/plugins/decl_mode/decl_mode.ml
+++ /dev/null
@@ -1,136 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-open CErrors
-open Util
-
-let daimon_flag = ref false
-
-let set_daimon_flag () = daimon_flag:=true
-let clear_daimon_flag () = daimon_flag:=false
-let get_daimon_flag () = !daimon_flag
-
-
-
-
-type split_tree=
-    Skip_patt of Id.Set.t * split_tree
-  | Split_patt of Id.Set.t * inductive *
-		(bool array * (Id.Set.t * split_tree) option) array
-  | Close_patt of split_tree
-  | End_patt of (Id.t * (int * int))
-
-type elim_kind =
-    EK_dep of split_tree
-  | EK_nodep
-  | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
-    {per_casee:constr;
-     per_ctype:types;
-     per_ind:inductive;
-     per_pred:constr;
-     per_args:constr list;
-     per_params:constr list;
-     per_nparams:int;
-     per_wf:recpath}
-
-type stack_info =
-    Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list
-  | Suppose_case
-  | Claim
-  | Focus_claim
-
-type pm_info =
-    { pm_stack : stack_info list}
-let info = Store.field ()
-
-
-(* Current proof mode *)
-
-type command_mode =
-    Mode_tactic
-  | Mode_proof
-  | Mode_none
-
-let mode_of_pftreestate pts =
-  (* spiwack: it used to be "top_goal_..." but this should be fine *)
-  let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
-  let goal = List.hd goals in
-  match Store.get (Goal.V82.extra sigma goal) info with
-  | None -> Mode_tactic 
-  | Some _ -> Mode_proof
-	  
-let get_current_mode () =
-  try 
-    mode_of_pftreestate (Pfedit.get_pftreestate ())
-  with Proof_global.NoCurrentProof -> Mode_none
-
-let check_not_proof_mode str =
- match get_current_mode () with
- | Mode_proof -> error str
- | _ -> ()
-
-let get_info sigma gl=
-  match Store.get (Goal.V82.extra sigma gl) info with
-  | None ->  invalid_arg "get_info"
-  | Some pm -> pm
-
-let try_get_info sigma gl =
-  Store.get (Goal.V82.extra sigma gl) info
-
-let get_goal_stack pts =
-  let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
-  let info = get_info sigma (List.hd goals) in
-  info.pm_stack
-
-
-let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.done_cond proof_focus
-
-let focus p =
-  let inf = get_goal_stack p in
-  Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
-
-let unfocus () =
-  Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
-
-let get_top_stack pts =
-  try
-    Proof.get_at_focus proof_focus pts
-  with Proof.NoSuchFocus ->
-    let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
-    let info = get_info sigma gl in
-    info.pm_stack
-
-let get_stack pts = Proof.get_at_focus proof_focus pts
-
-let get_last env = match Environ.named_context env with
-  | decl :: _ -> Context.Named.Declaration.get_id decl
-  | [] -> error "no previous statement to use"
-
-
-let get_end_command pts =
-  match get_top_stack pts with
-  | [] -> "\"end proof\""
-  | Claim::_ -> "\"end claim\""
-  | Focus_claim::_-> "\"end focus\""
-  | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _  ->
-      begin
-	match et with
-	  Decl_expr.ET_Case_analysis ->
-	    "\"end cases\" or start a new case"
-	| Decl_expr.ET_Induction ->
-	    "\"end induction\" or start a new case"
-      end
-  | _ -> anomaly (Pp.str"lonely suppose")
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
deleted file mode 100644
index dfeee833c..000000000
--- a/plugins/decl_mode/decl_mode.mli
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-
-val set_daimon_flag : unit -> unit
-val clear_daimon_flag : unit -> unit
-val get_daimon_flag : unit -> bool
-
-type command_mode =
-    Mode_tactic
-  | Mode_proof
-  | Mode_none
-
-val mode_of_pftreestate : Proof.proof -> command_mode
-
-val get_current_mode : unit -> command_mode
-
-val check_not_proof_mode : string -> unit
-
-type split_tree=
-    Skip_patt of Id.Set.t * split_tree
-  | Split_patt of Id.Set.t * inductive *
-		(bool array * (Id.Set.t * split_tree) option) array
-  | Close_patt of split_tree
-  | End_patt of (Id.t * (int * int))
-
-type elim_kind =
-    EK_dep of split_tree
-  | EK_nodep
-  | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
-    {per_casee:constr;
-     per_ctype:types;
-     per_ind:inductive;
-     per_pred:constr;
-     per_args:constr list;
-     per_params:constr list;
-     per_nparams:int;
-     per_wf:recpath}
-
-type stack_info =
-    Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list
-  | Suppose_case
-  | Claim
-  | Focus_claim
-
-type pm_info =
-    {pm_stack : stack_info list }
-
-val info : pm_info Store.field
-
-val get_info : Evd.evar_map -> Proof_type.goal -> pm_info
-
-val try_get_info : Evd.evar_map -> Proof_type.goal -> pm_info option
-
-val get_stack : Proof.proof -> stack_info list
-
-val get_top_stack : Proof.proof -> stack_info list
-
-val get_last:  Environ.env -> Id.t
-(** [get_last] raises a [UserError] when it cannot find a previous
-    statement in the environment. *)
-
-val get_end_command : Proof.proof -> string
-
-val focus : Proof.proof -> unit
-
-val unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack
deleted file mode 100644
index 1b84a0790..000000000
--- a/plugins/decl_mode/decl_mode_plugin.mlpack
+++ /dev/null
@@ -1,5 +0,0 @@
-Decl_mode
-Decl_interp
-Decl_proof_instr
-Ppdecl_proof
-G_decl_mode
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
deleted file mode 100644
index 2ea4538c3..000000000
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ /dev/null
@@ -1,1575 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Util
-open Pp
-open Evd
-
-open Tacmach
-open Tacintern
-open Decl_expr
-open Decl_mode
-open Decl_interp
-open Glob_term
-open Glob_ops
-open Names
-open Nameops
-open Declarations
-open Tactics
-open Tacticals
-open Term
-open Vars
-open Termops
-open Namegen
-open Goptions
-open Misctypes
-open Sigma.Notations
-open Context.Named.Declaration
-
-module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
-
-(* Strictness option *)
-
-let clear ids { it = goal; sigma } =
-  let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
-  let env = Goal.V82.env sigma goal in
-  let sign = Goal.V82.hyps sigma goal in
-  let cl = Goal.V82.concl sigma goal in
-  let evdref = ref (Evd.clear_metas sigma) in
-  let (hyps, concl) =
-    try Evarutil.clear_hyps_in_evi env evdref sign cl ids
-    with Evarutil.ClearDependencyError (id, _) ->
-      user_err  (str "Cannot clear " ++ pr_id id)
-  in
-  let sigma = !evdref in
-  let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
-  let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-  { it = [gl]; sigma }
-
-let get_its_info gls = get_info gls.sigma gls.it
-
-let get_strictness,set_strictness =
-  let strictness = ref false in
-    (fun () -> (!strictness)),(fun b -> strictness:=b)
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "strict proofs";
-      optkey   = ["Strict";"Proofs"];
-      optread  = get_strictness;
-      optwrite = set_strictness }
-
-let tcl_change_info_gen info_gen =
-  (fun gls ->
-     let it = sig_it gls in
-     let concl = pf_concl gls in
-     let hyps = Goal.V82.hyps (project gls) it in
-     let extra = Goal.V82.extra (project gls) it in
-     let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
-     let sigma = Goal.V82.partial_solution sigma it ev in
-     { it = [gl] ; sigma= sigma; } )
-
-let tcl_change_info info gls =
-  let info_gen s = Store.set s Decl_mode.info info in
-  tcl_change_info_gen info_gen gls
-
-let tcl_erase_info gls =
-  let info_gen s = Store.remove s Decl_mode.info in
-  tcl_change_info_gen info_gen gls
-
-let special_whd gl=
-  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
-    (fun t -> CClosure.whd_val infos (CClosure.inject (EConstr.Unsafe.to_constr t)))
-
-let special_nf gl=
-  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
-    (fun t -> CClosure.norm_val infos (CClosure.inject t))
-
-let is_good_inductive env ind =
-  let mib,oib = Inductive.lookup_mind_specif env ind in
-    Int.equal oib.mind_nrealargs 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
-
-let check_not_per pts =
-  if not (Proof.is_done pts) then
-    match get_stack pts with
-	Per (_,_,_,_)::_ ->
-	  error "You are inside a proof per cases/induction.\n\
-Please \"suppose\" something or \"end\" it now."
-      | _ -> ()
-
-let mk_evd metalist gls =
-  let evd0= clear_metas (sig_sig gls) in
-  let add_one (meta,typ) evd =
-    meta_declare meta typ evd in
-    List.fold_right add_one metalist evd0
-
-let is_tmp id = (Id.to_string id).[0] == '_'
-
-let tmp_ids gls =
-  let ctx = pf_hyps gls in
-    match ctx with
-	[] -> []
-      | _::q -> List.filter is_tmp (ids_of_named_context q)
-
-let clean_tmp gls =
-  let clean_id id0 gls0 =
-      tclTRY (clear [id0]) gls0 in
-  let rec clean_all = function
-      [] -> tclIDTAC
-    | id :: rest -> tclTHEN (clean_id id) (clean_all rest)
-  in
-    clean_all (tmp_ids gls) gls
-
-let assert_postpone id t =
-  assert_before (Name id) (EConstr.of_constr t)
-
-(* start a proof *)
-
-
-let start_proof_tac gls=
-  let info={pm_stack=[]} in
-  tcl_change_info info gls
-
-let go_to_proof_mode () =
-  ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac));
-  let p = Proof_global.give_me_the_proof () in
-  Decl_mode.focus p
-
-(* closing gaps *)
-
-(* spiwack: should use [Proofview.give_up] but that would require
-   moving the whole declarative mode into the new proof engine.  It
-   will eventually have to be done.
-
-   As far as I can tell, [daimon_tac] is used after a [thus thesis],
-   it will leave uninstantiated variables instead of giving a relevant
-   message at [Qed]. *)
-let daimon_tac gls =
-  set_daimon_flag ();
-  {it=[];sigma=sig_sig gls;}
-
-let daimon_instr env p =
-  let (p,(status,_)) =
-    Proof.run_tactic env begin
-      Proofview.tclINDEPENDENT Proofview.give_up
-    end p
-  in
-  p,status
-
-let do_daimon () =
-  let env = Global.env () in
-  let status =
-    Proof_global.with_current_proof begin fun _ p ->
-      daimon_instr env p
-    end
-  in
-  if not status then Feedback.feedback Feedback.AddedAxiom else ()
-
-(* post-instruction focus management *)
-
-let goto_current_focus () = 
-  Decl_mode.unfocus ()
-
-(* spiwack: used to catch errors indicating lack of "focusing command"
-   in the proof tree. In the current implementation, however, entering
-   the declarative mode puts a focus first, there should, therefore,
-   never be exception raised here. *)
-let goto_current_focus_or_top () =
-  goto_current_focus ()
-
-(* return *)
-
-let close_tactic_mode () =
-  try do_daimon ();goto_current_focus ()
-  with Not_found ->
-    error "\"return\" cannot be used outside of Declarative Proof Mode."
-
-let return_from_tactic_mode () =
-  close_tactic_mode ()
-
-(* end proof/claim *)
-
-let close_block bt pts =
-    if Proof.no_focused_goal pts then
-      goto_current_focus ()
-    else
-      let stack =
-	if Proof.is_done pts then
-	  get_top_stack pts
-	else
-	  get_stack pts 
-      in
-      match bt,stack with
-	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
-	  do_daimon ();goto_current_focus ()
-      | _, Claim::_ ->
-	  error "\"end claim\" expected."
-      | _, Focus_claim::_ ->
-	  error "\"end focus\" expected."
-      | _, [] ->
- 	  error "\"end proof\" expected."
-      | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
-	  begin
-	    match et with
-		ET_Case_analysis -> error "\"end cases\" expected."
-	      | ET_Induction ->  error "\"end induction\" expected."
-	  end
-      | _,_ -> anomaly (Pp.str "Lonely suppose on stack.")
-
-
-(* utility for suppose / suppose it is *)
-
-let close_previous_case pts =
-  if
-    Proof.is_done pts
-  then
-    match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
-      | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  goto_current_focus ()
-      | _ -> error "Not inside a proof per cases or induction."
-  else
-    match get_stack pts with
-	Per (et,_,_,_) :: _ -> ()
-      | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  do_daimon ();goto_current_focus ()
-      | _ -> error "Not inside a proof per cases or induction."
-
-(* Proof instructions *)
-
-(* automation *)
-
-let filter_hyps f gls =
-  let filter_aux id =
-    let id = NamedDecl.get_id id in
-    if f id then
-      tclIDTAC
-    else
-      tclTRY (clear [id])  in
-    tclMAP filter_aux (pf_hyps gls) gls
-
-let local_hyp_prefix = Id.of_string "___"
-
-let add_justification_hyps keep items gls =
-  let add_aux c gls=
-    match kind_of_term c with
-	Var id ->
-	  keep:=Id.Set.add id !keep;
-	  tclIDTAC gls
-      | _ ->
-	  let id=pf_get_new_id local_hyp_prefix gls in
-	    keep:=Id.Set.add id !keep;
-	    let c = EConstr.of_constr c in
-	    tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
-              (Proofview.V82.of_tactic (clear_body [id])) gls in
-    tclMAP add_aux items gls
-
-let prepare_goal items gls =
-  let tokeep = ref Id.Set.empty in
-  let auxres = add_justification_hyps tokeep items gls in
-   tclTHENLIST
-     [ (fun _ -> auxres);
-       filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
-
-let my_automation_tac = ref
-  (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
-
-let register_automation_tac tac = my_automation_tac:= tac
-
-let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
-
-let warn_insufficient_justification =
-  CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
-    (fun () -> strbrk "Insufficient justification.")
-
-let justification tac gls=
-    tclORELSE
-      (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
-      (fun gls ->
-	 if get_strictness () then
-	   error "Insufficient justification."
-	 else
-	   begin
-             warn_insufficient_justification ();
-	     daimon_tac gls
-	   end) gls
-
-let default_justification elems gls=
-  justification (tclTHEN (prepare_goal elems) (Proofview.V82.of_tactic automation_tac)) gls
-
-(* code for conclusion refining *)
-
-let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s)
-
-let _and       = constant ["Init";"Logic"] "and"
-
-let _and_rect  = constant ["Init";"Logic"] "and_rect"
-
-let _prod      = constant ["Init";"Datatypes"] "prod"
-
-let _prod_rect = constant ["Init";"Datatypes"] "prod_rect"
-
-let _ex        = constant ["Init";"Logic"] "ex"
-
-let _ex_ind    = constant ["Init";"Logic"] "ex_ind"
-
-let _sig       = constant ["Init";"Specif"] "sig"
-
-let _sig_rect  = constant ["Init";"Specif"] "sig_rect"
-
-let _sigT      = constant ["Init";"Specif"] "sigT"
-
-let _sigT_rect = constant ["Init";"Specif"] "sigT_rect"
-
-type stackd_elt =
-{se_meta:metavariable;
- se_type:types;
- se_last_meta:metavariable;
- se_meta_list:(metavariable*types) list;
- se_evd: evar_map}
-
-let rec replace_in_list m l = function
-    [] -> raise Not_found
-  | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q
-
-let enstack_subsubgoals env se stack gls=
-  let hd,params = decompose_app (special_whd gls (EConstr.of_constr se.se_type)) in
-    match kind_of_term hd with
-	Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *)
-	  let mib,oib=
-	    Inductive.lookup_mind_specif env ind in
-          let gentypes=
-            Inductive.arities_of_constructors indu (mib,oib) in
-	  let process i gentyp =
-	    let constructor = mkConstructU ((ind,succ i),u)
-	      (* constructors numbering*) in
-	    let appterm = applist (constructor,params) in
-	    let apptype = Term.prod_applist gentyp params in
-	    let rc,_ = Reduction.dest_prod env apptype in
-	    let rec meta_aux last lenv = function
-		[] -> (last,lenv,[])
-	      | decl::q ->
-		  let nlast=succ last in
-		  let (llast,holes,metas) =
-		    meta_aux nlast (mkMeta nlast :: lenv) q in
-		    (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in
-	    let (nlast,holes,nmetas) =
-		meta_aux se.se_last_meta [] (List.rev rc) in
-	    let refiner = applist (appterm,List.rev holes) in
-	    let evd = meta_assign se.se_meta
-              (refiner,(Conv,TypeProcessed (* ? *))) se.se_evd in
-	    let ncreated = replace_in_list
-	      se.se_meta nmetas se.se_meta_list in
-	    let evd0 = List.fold_left
-	      (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in
-	      List.iter (fun (m,typ) ->
-			   Stack.push
-			     {se_meta=m;
-			      se_type=typ;
-			      se_evd=evd0;
-			      se_meta_list=ncreated;
-			      se_last_meta=nlast} stack) (List.rev nmetas)
-	  in
-	    Array.iteri process gentypes
-      | _ -> ()
-
-let nf_meta sigma c =
-  EConstr.Unsafe.to_constr (Reductionops.nf_meta sigma (EConstr.of_constr c))
-
-let rec nf_list evd =
-  function
-      [] -> []
-    | (m,typ)::others ->
-	if meta_defined evd m then
-	    nf_list evd others
-	else
-	  (m,nf_meta evd typ)::nf_list evd others
-
-let find_subsubgoal c ctyp skip submetas gls =
-  let env= pf_env gls in
-  let concl = pf_concl gls in
-  let concl = EConstr.Unsafe.to_constr concl in
-  let evd = mk_evd ((0,concl)::submetas) gls in
-  let stack = Stack.create () in
-  let max_meta =
-      List.fold_left (fun a (m,_) -> max a m) 0 submetas in
-  let _ = Stack.push
-		{se_meta=0;
-		 se_type=concl;
-		 se_last_meta=max_meta;
-		 se_meta_list=[0,concl];
-		 se_evd=evd} stack  in
-  let rec dfs n =
-    let se = Stack.pop stack in
-      try
-	let unifier =
-	  Unification.w_unify env se.se_evd Reduction.CUMUL
-	    ~flags:(Unification.elim_flags ()) ctyp (EConstr.of_constr se.se_type) in
-	  if n <= 0 then
-	      {se with
-		 se_evd=meta_assign se.se_meta
-                  (c,(Conv,TypeNotProcessed (* ?? *))) unifier;
-	         se_meta_list=replace_in_list
-		  se.se_meta submetas se.se_meta_list}
-	  else
-	      dfs (pred n)
-      with e when CErrors.noncritical e ->
-	begin
-	  enstack_subsubgoals env se stack gls;
-	  dfs n
-	end in
-  let nse= try dfs skip with Stack.Empty -> raise Not_found in
-    nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0)
-
-let concl_refiner metas body gls =
-  let concl = pf_concl gls in
-  let evd = sig_sig gls in
-  let env = pf_env gls in
-  let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
-  let concl = EConstr.Unsafe.to_constr concl in
-  let rec aux env avoid subst = function
-      [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
-    | (n,typ)::rest ->
-	let _A = subst_meta subst typ in
-	let x = id_of_name_using_hdchar env evd (EConstr.of_constr _A) Anonymous in
-	let _x = fresh_id avoid x gls in
-	let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
-	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
-	let nsubst = (n,mkVar _x)::subst in
-	  if List.is_empty rest then
-	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
-	  else
-	    let bsort,_B,nbody =
-	      aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in
-	    let body = mkNamedLambda _x _A nbody in
-	      if local_occur_var evd _x (EConstr.of_constr _B) then
-	        begin
-		  let _P = mkNamedLambda _x _A _B in
-		    match bsort,sort with
-			InProp,InProp ->
-			  let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in
-			    InProp,_AxB,
-			  mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|])
-		    | InProp,_ ->
-			let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in
-			let _P0 = mkLambda(Anonymous,_AxB,concl) in
-			  InType,_AxB,
-			mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|])
-		    | _,_ ->
-			let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in
-			let _P0 = mkLambda(Anonymous,_AxB,concl) in
-			  InType,_AxB,
-			mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|])
-		end
-	      else
-		begin
-		  match asort,bsort with
-		      InProp,InProp ->
-			let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in
-			  InProp,_AxB,
-		     mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|])
-		    |_,_ ->
-		       let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in
-		       let _P0 = mkLambda(Anonymous,_AxB,concl) in
-			 InType,_AxB,
-			mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|])
-		end
-  in
-  let (_,_,prf) = aux env [] [] metas in
-    mkApp(prf,[|mkMeta 1|])
-
-let thus_tac c ctyp submetas gls =
-  let list,proof =
-    try
-      find_subsubgoal c ctyp 0 submetas gls
-    with Not_found ->
-      error "I could not relate this statement to the thesis." in
-  if List.is_empty list then
-    let proof = EConstr.of_constr proof in
-    Proofview.V82.of_tactic (exact_check proof) gls
-  else
-    let refiner = concl_refiner list proof gls in
-      Tacmach.refine (EConstr.of_constr refiner) gls
-
-(* general forward step *)
-
-let mk_stat_or_thesis info gls = function
-    This c -> c
-  | Thesis (For _ ) ->
-      error "\"thesis for ...\" is not applicable here."
-  | Thesis Plain -> EConstr.Unsafe.to_constr (pf_concl gls)
-
-let just_tac _then cut info gls0 =
-  let last_item =
-    if _then then
-      try [mkVar (get_last (pf_env gls0))]
-      with UserError _ ->
-	error "\"then\" and \"hence\" require at least one previous fact"
-    else []
-  in
-  let items_tac gls = 
-    match cut.cut_by with
-	None -> tclIDTAC gls
-      | Some items -> prepare_goal (last_item@items) gls in
-  let method_tac gls =
-    match cut.cut_using with
-        None ->
-	  Proofview.V82.of_tactic automation_tac gls
-      | Some tac ->
-	  Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
-    justification (tclTHEN items_tac method_tac) gls0
-
-let instr_cut mkstat _thus _then cut gls0 =
-  let info = get_its_info gls0 in
-  let stat = cut.cut_stat in
-  let (c_id,_) = match stat.st_label with
-      Anonymous ->
-	pf_get_new_id (Id.of_string "_fact") gls0,false
-    | Name id -> id,true in
-  let c_stat = mkstat info gls0 stat.st_it in
-  let thus_tac gls=
-    if _thus then
-      thus_tac (mkVar c_id) (EConstr.of_constr c_stat) [] gls
-    else tclIDTAC gls in
-    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
-      [tclTHEN tcl_erase_info (just_tac _then cut info);
-       thus_tac] gls0
-
-
-(* iterated equality *)
-let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
-
-let decompose_eq id gls =
-  let typ = pf_get_hyp_typ gls id in
-  let whd =  (special_whd gls typ) in
-    match kind_of_term whd with
-	App (f,args)->
-	  if Term.eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
-	  then (args.(0),
-		args.(1),
-		args.(2))
-	  else error "Previous step is not an equality."
-      | _ -> error "Previous step is not an equality."
-
-let instr_rew _thus rew_side cut gls0 =
-  let last_id =
-    try get_last (pf_env gls0)
-    with UserError _ -> error "No previous equality."
-  in
-  let typ,lhs,rhs = decompose_eq last_id gls0 in
-  let items_tac gls =
-    match cut.cut_by with
-	None -> tclIDTAC gls
-      | Some items -> prepare_goal items gls in
-  let method_tac gls =
-    match cut.cut_using with
-        None ->
-	  Proofview.V82.of_tactic automation_tac gls
-      | Some tac ->
-	  Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
-  let just_tac gls =
-    justification (tclTHEN items_tac method_tac) gls in
-  let (c_id,_) = match cut.cut_stat.st_label with
-      Anonymous ->
-	pf_get_new_id (Id.of_string "_eq") gls0,false
-    | Name id -> id,true in
-  let thus_tac new_eq gls=
-    if _thus then
-      thus_tac (mkVar c_id) (EConstr.of_constr new_eq) [] gls
-    else tclIDTAC gls in
-    match rew_side with
-	Lhs ->
-	  let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in
-	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
-	      [tclTHEN tcl_erase_info
-		 (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr lhs)))
-		    [just_tac;Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id))]);
-	       thus_tac new_eq] gls0
-      | Rhs ->
-	  let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
-	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
-	      [tclTHEN tcl_erase_info
-		 (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr rhs)))
-		    [Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id));just_tac]);
-	       thus_tac new_eq] gls0
-
-
-(* tactics for claim/focus *)
-
-let instr_claim _thus st gls0 =
-  let info = get_its_info gls0 in
-  let (id,_) = match st.st_label with
-      Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false
-    | Name id -> id,true in
-  let thus_tac gls=
-    if _thus then
-      thus_tac (mkVar id) (EConstr.of_constr st.st_it) [] gls
-    else tclIDTAC gls in
-  let ninfo1 = {pm_stack=
-      (if _thus then Focus_claim else Claim)::info.pm_stack} in
-    tclTHENS (Proofview.V82.of_tactic (assert_postpone id st.st_it))
-      [thus_tac;
-       tcl_change_info ninfo1] gls0
-
-(* tactics for assume *)
-
-let push_intro_tac coerce nam gls =
-      let (hid,_) =
-	match nam with
-	    Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false
-	  | Name id -> id,true in
-	tclTHENLIST
-	  [Proofview.V82.of_tactic (intro_mustbe_force hid);
-	   coerce hid]
-	  gls
-
-let assume_tac hyps gls =
-  List.fold_right
-    (fun (Hvar st | Hprop st) ->
-       tclTHEN
-	 (push_intro_tac
-	    (fun id ->
-	       Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) st.st_label))
-	 hyps tclIDTAC gls
-
-let assume_hyps_or_theses hyps gls =
-  List.fold_right
-    (function
-	 (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) ->
-	   tclTHEN
-	     (push_intro_tac
-		(fun id ->
-		   Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr c)))) nam)
-       | Hprop {st_label=nam;st_it=Thesis (tk)} ->
-	   tclTHEN
-	     (push_intro_tac
-		(fun id -> tclIDTAC) nam))
-    hyps tclIDTAC gls
-
-let assume_st hyps gls =
-  List.fold_right
-    (fun st ->
-       tclTHEN
-	 (push_intro_tac
-	    (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) st.st_label))
-	 hyps tclIDTAC gls
-
-let assume_st_letin hyps gls =
-  List.fold_right
-    (fun st ->
-       tclTHEN
-	 (push_intro_tac
-	    (fun id ->
-	       Proofview.V82.of_tactic (convert_hyp (LocalDef (id, EConstr.of_constr (fst st.st_it), EConstr.of_constr (snd st.st_it))))) st.st_label))
-	 hyps tclIDTAC gls
-
-(* suffices *)
-
-let rec metas_from n hyps =
-  match hyps with
-      _ :: q -> n :: metas_from (succ n) q
-    | [] -> []
-
-let rec build_product sigma args body =
-  match args with
-      (Hprop st| Hvar st )::rest ->
-	let pprod= lift 1 (build_product sigma rest body) in
-	let lbody =
-	  match st.st_label with
-	      Anonymous -> pprod
-	    | Name id -> subst_var id pprod in
-	  mkProd (st.st_label, st.st_it, lbody)
-    | [] -> body
-
-let rec build_applist prod = function
-    [] -> [],prod
-  | n::q ->
-      let (_,typ,_) = destProd prod in
-      let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
-	(n,typ)::ctx,head
-
-let instr_suffices _then cut gls0 =
-  let info = get_its_info gls0 in
-  let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
-  let ctx,hd = cut.cut_stat in
-  let c_stat = build_product (project gls0) ctx (mk_stat_or_thesis info gls0 hd) in
-  let metas = metas_from 1 ctx in
-  let c_ctx,c_head = build_applist c_stat metas in
-  let c_term = applist (mkVar c_id,List.map mkMeta metas) in
-  let thus_tac gls=
-    thus_tac c_term (EConstr.of_constr c_head) c_ctx gls in
-   tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
-     [tclTHENLIST
-	 [ assume_tac ctx;
-	   tcl_erase_info;
-	   just_tac _then cut info];
-      thus_tac] gls0
-
-(* tactics for consider/given *)
-
-let conjunction_arity id gls =
-  let typ = pf_get_hyp_typ gls id  in
-  let hd,params = decompose_app (special_whd gls typ) in
-  let env =pf_env gls in
-    match kind_of_term hd with
-	Ind (ind,u as indu) when is_good_inductive env ind ->
-	  let mib,oib=
-	    Inductive.lookup_mind_specif env ind in
-          let gentypes=
-            Inductive.arities_of_constructors indu (mib,oib) in
-	  let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in
-	  let apptype = Term.prod_applist gentypes.(0) params in
-	  let rc,_ = Reduction.dest_prod env apptype in
-	    List.length rc
-      | _ -> raise Not_found
-
-let rec intron_then n ids ltac gls =
-  if n<=0 then
-    ltac ids gls
-  else
-    let id = pf_get_new_id (Id.of_string "_tmp") gls in
-      tclTHEN
-	(Proofview.V82.of_tactic (intro_mustbe_force id))
-	(intron_then (pred n) (id::ids) ltac) gls
-
-
-let rec consider_match may_intro introduced available expected gls =
-  match available,expected with
-      [],[] ->
-	  tclIDTAC gls
-    | _,[] -> error "Last statements do not match a complete hypothesis."
-	(* should tell which ones *)
-    | [],hyps ->
-	if may_intro then
-	  begin
- 	    let id = pf_get_new_id (Id.of_string "_tmp") gls in
-	      tclIFTHENELSE
-		(Proofview.V82.of_tactic (intro_mustbe_force id))
-		(consider_match true [] [id] hyps)
-		(fun _ ->
-		   error "Not enough sub-hypotheses to match statements.")
-		gls
-          end
-	else
-	  error "Not enough sub-hypotheses to match statements."
-	    (* should tell which ones *)
-    | id::rest_ids,(Hvar st | Hprop st)::rest ->
-	tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it))))
-	  begin
-	    match st.st_label with
-		Anonymous ->
-		  consider_match may_intro ((id,false)::introduced) rest_ids rest
-	      | Name hid ->
-		  tclTHENLIST
-		    [Proofview.V82.of_tactic (rename_hyp [id,hid]);
-		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
-	  end
-	  begin
-	    (fun gls ->
-	       let nhyps =
-		 try conjunction_arity id gls with
-		     Not_found -> error "Matching hypothesis not found." in
-		 tclTHENLIST
-		   [Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id));
-		    intron_then nhyps []
-		      (fun l -> consider_match may_intro introduced
-			 (List.rev_append l rest_ids) expected)] gls)
-	  end
-	  gls
-
-let consider_tac c hyps gls =
-  let c = EConstr.of_constr c in
-  match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with
-      Var id ->
-	consider_match false [] [id] hyps gls
-    | _ ->
-	let id = pf_get_new_id (Id.of_string "_tmp") gls in
-	tclTHEN
-	  (Proofview.V82.of_tactic (pose_proof (Name id) c))
- 	  (consider_match false [] [id] hyps) gls
-
-
-let given_tac hyps gls =
-  consider_match true [] [] hyps gls
-
-(* tactics for take *)
-
-let rec take_tac wits gls =
-  match wits with
-      [] -> tclIDTAC gls
-    | wit::rest ->
-	let typ = pf_unsafe_type_of gls (EConstr.of_constr wit) in
-	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
-
-
-(* tactics for define *)
-
-let subst_term sigma c t =
-  EConstr.Unsafe.to_constr (subst_term sigma c t)
-
-let rec build_function sigma args body =
-  match args with
-      st::rest ->
-	let pfun= lift 1 (build_function sigma rest body) in
-	let id = match st.st_label with
-	    Anonymous -> assert false
-	  | Name id -> id in
-	  mkLambda (Name id, st.st_it, subst_term sigma (EConstr.mkVar id) (EConstr.of_constr pfun))
-    | [] -> body
-
-let define_tac id args body gls =
-  let t = build_function (project gls) args body in
-  let t = EConstr.of_constr t in
-    Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls
-
-(* tactics for reconsider *)
-
-let cast_tac id_or_thesis typ gls =
-  let typ = EConstr.of_constr typ in
-  match id_or_thesis with
-    | This id ->
-        Proofview.V82.of_tactic  (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
-    | Thesis (For _ ) ->
-	error "\"thesis for ...\" is not applicable here."
-    | Thesis Plain ->
-          Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls
-
-(* per cases *)
-
-let is_rec_pos (main_ind,wft) =
-  match main_ind with
-      None -> false
-    | Some index ->
-	match fst (Rtree.dest_node wft) with
-	    Mrec (_,i) when Int.equal i index -> true
-	  | _ -> false
-
-let rec constr_trees (main_ind,wft) ind =
-    match Rtree.dest_node wft with
-      Norec,_ ->
-	let itree =
-	  (snd (Global.lookup_inductive ind)).mind_recargs in
-	  constr_trees (None,itree) ind
-    | _,constrs -> main_ind,constrs
-
-let ind_args rp ind =
-    let main_ind,constrs = constr_trees rp ind in
-    let args ctree =
-      Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in
-      Array.map args constrs
-
-let init_tree ids ind rp nexti =
-  let indargs = ind_args rp ind in
-  let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in
-    Split_patt (ids,ind,Array.mapi do_i indargs)
-
-let map_tree_rp rp id_fun mapi = function
-    Split_patt (ids,ind,branches) ->
-  let indargs = ind_args rp ind in
-  let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in
-    Split_patt (id_fun ids,ind,Array.mapi do_i branches)
-  | _ -> failwith "map_tree_rp: not a splitting node"
-
-let map_tree id_fun mapi = function
-    Split_patt (ids,ind,branches) ->
-  let do_i i (recargs,bri) = recargs,mapi i bri in
-    Split_patt (id_fun ids,ind,Array.mapi do_i branches)
-  | _ -> failwith "map_tree: not a splitting node"
-
-
-let start_tree env ind rp =
-  init_tree Id.Set.empty ind rp (fun _ _ -> None)
-
-let build_per_info etype casee gls =
-  let concl=pf_concl gls in
-  let env=pf_env gls in
-  let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
-  let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in
-  let hd,args = decompose_app (special_whd gls ctyp) in
-  let (ind,u) =
-    try
-      destInd hd
-    with DestKO ->
-      error "Case analysis must be done on an inductive object." in
-  let mind,oind = Global.lookup_inductive ind in
-  let nparams,index =
-    match etype with
-	ET_Induction -> mind.mind_nparams_rec,Some (snd ind)
-      | _ -> mind.mind_nparams,None in
-  let params,real_args = List.chop nparams args in
-  let abstract_obj c body =
-    let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
-      lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
-  let pred= List.fold_right abstract_obj
-    real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
-  let ctyp = EConstr.Unsafe.to_constr ctyp in
-  let pred = EConstr.Unsafe.to_constr pred in
-    is_dep,
-  {per_casee=casee;
-   per_ctype=ctyp;
-   per_ind=ind;
-   per_pred=pred;
-   per_args=real_args;
-   per_params=params;
-   per_nparams=nparams;
-   per_wf=index,oind.mind_recargs}
-
-let per_tac etype casee gls=
-  let env=pf_env gls in
-  let info = get_its_info gls in
-    match casee with
-	Real c ->
-	  let is_dep,per_info = build_per_info etype c gls in
-	  let ek =
-	    if is_dep then
-	      EK_dep (start_tree env per_info.per_ind per_info.per_wf)
-	    else EK_unknown in
-	    tcl_change_info
-	      {pm_stack=
-		  Per(etype,per_info,ek,[])::info.pm_stack} gls
-      | Virtual cut ->
-	  assert (cut.cut_stat.st_label == Anonymous);
-	  let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in
-	  let c = mkVar id in
-	  let modified_cut =
-	    {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
-	    tclTHEN
-	      (instr_cut (fun _ _ c -> c) false false modified_cut)
-	      (fun gls0 ->
-		 let is_dep,per_info = build_per_info etype c gls0 in
-		   assert (not is_dep);
-		   tcl_change_info
-		     {pm_stack=
-			 Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
-	      gls
-
-(* suppose *)
-
-let register_nodep_subcase id= function
-    Per(et,pi,ek,clauses)::s ->
-      begin
-	match ek with
-	    EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
-	  | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
-	  | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"."
-      end
-  | _ -> anomaly (Pp.str "wrong stack state")
-
-let suppose_tac hyps gls0 =
-  let info = get_its_info gls0 in
-  let thesis = pf_concl gls0 in
-  let thesis = EConstr.Unsafe.to_constr thesis in
-  let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
-  let clause = build_product (project gls0) hyps thesis in
-  let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
-  let old_clauses,stack = register_nodep_subcase id info.pm_stack in
-  let ninfo2 = {pm_stack=stack} in
-    tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause))
-      [tclTHENLIST [tcl_change_info ninfo1;
-		    assume_tac hyps;
-		    clear old_clauses];
-       tcl_change_info ninfo2] gls0
-
-(* suppose it is ... *)
-
-(* pattern matching compiling *)
-
-let rec skip_args rest ids n =
-  if n <= 0 then
-    Close_patt rest
-  else
-    Skip_patt (ids,skip_args rest ids (pred n))
-
-let rec tree_of_pats ((id,_) as cpl) pats =
-  match pats with
-      [] -> End_patt cpl
-    | args::stack ->
-	match args with
-	    [] -> Close_patt (tree_of_pats cpl stack)
-	  | (patt,rp) :: rest_args ->
-	      match patt with
-		  PatVar (_,v) ->
-		    Skip_patt (Id.Set.singleton id,
-			       tree_of_pats cpl (rest_args::stack))
-		| PatCstr (_,(ind,cnum),args,nam) ->
-		    let nexti i ati =
-		      if Int.equal i (pred cnum) then
-			let nargs =
-			  List.map_i (fun j a -> (a,ati.(j))) 0 args in
-			  Some (Id.Set.singleton id,
-				tree_of_pats cpl (nargs::rest_args::stack))
-		      else None
-		      in init_tree Id.Set.empty ind rp nexti
-
-let rec add_branch ((id,_) as cpl) pats tree=
-  match pats with
-      [] ->
-	begin
-	  match tree with
-	      End_patt cpl0 -> End_patt cpl0
-		(* this ensures precedence for overlapping patterns *)
-	    | _ -> anomaly (Pp.str "tree is expected to end here")
-	end
-    | args::stack ->
-	match args with
-	    [] ->
-	      begin
-		match tree with
-		   Close_patt t ->
-		     Close_patt (add_branch cpl stack t)
-		  | _ -> anomaly (Pp.str "we should pop here")
-	      end
-	  | (patt,rp) :: rest_args ->
-	      match patt with
-		  PatVar (_,v) ->
-		    begin
-		      match tree with
-			  Skip_patt (ids,t) ->
-			    Skip_patt (Id.Set.add id ids,
-				       add_branch cpl (rest_args::stack) t)
-			| Split_patt (_,_,_) ->
-			    map_tree (Id.Set.add id)
-			      (fun i bri ->
-				 append_branch cpl 1 (rest_args::stack) bri)
-			      tree
-			| _ -> anomaly (Pp.str "No pop/stop expected here")
-		    end
-		| PatCstr (_,(ind,cnum),args,nam) ->
-		      match tree with
-			Skip_patt (ids,t) ->
-			  let nexti i ati =
-			    if Int.equal i (pred cnum) then
-			      let nargs =
-				List.map_i (fun j a -> (a,ati.(j))) 0 args in
-				Some (Id.Set.add id ids,
-				      add_branch cpl (nargs::rest_args::stack)
-					(skip_args t ids (Array.length ati)))
-			    else
-			      Some (ids,
-				    skip_args t ids (Array.length ati))
-			  in init_tree ids ind rp nexti
-		      | Split_patt (_,ind0,_) ->
-			  if (not (eq_ind ind ind0)) then error
-			    (* this can happen with coercions *)
-	                    "Case pattern belongs to wrong inductive type.";
-			  let mapi i ati bri =
-			    if Int.equal i (pred cnum) then
-			      let nargs =
-				List.map_i (fun j a -> (a,ati.(j))) 0 args in
-				append_branch cpl 0
-				  (nargs::rest_args::stack) bri
-			    else bri in
-			    map_tree_rp rp (fun ids -> ids) mapi tree
-		      | _ -> anomaly (Pp.str "No pop/stop expected here")
-and append_branch ((id,_) as cpl) depth pats = function
-    Some (ids,tree) ->
-      Some (Id.Set.add id ids,append_tree cpl depth pats tree)
-  | None ->
-      Some (Id.Set.singleton id,tree_of_pats cpl pats)
-and append_tree ((id,_) as cpl) depth pats tree =
-  if depth<=0 then add_branch cpl pats tree
-  else match tree with
-      Close_patt t ->
-	Close_patt (append_tree cpl (pred depth) pats t)
-    | Skip_patt (ids,t) ->
-	Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t)
-    | End_patt _ -> anomaly (Pp.str "Premature end of branch")
-    | Split_patt (_,_,_) ->
-	map_tree (Id.Set.add id)
-	  (fun i bri -> append_branch cpl (succ depth) pats bri) tree
-
-(* suppose it is *)
-
-let rec st_assoc id = function
-    [] -> raise Not_found
-  | st::_ when Name.equal st.st_label id  -> st.st_it
-  | _ :: rest -> st_assoc id rest
-
-let thesis_for obj typ per_info env=
-  let rc,hd1=decompose_prod typ in
-  let cind,all_args=decompose_app typ in
-  let ind,u = destInd cind in
-  let _ = if not (eq_ind ind per_info.per_ind) then
-    user_err ~hdr:"thesis_for"
-      ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
-	 str"cannot give an induction hypothesis (wrong inductive type).") in
-  let params,args = List.chop per_info.per_nparams all_args in
-  let _ = if not (List.for_all2 Term.eq_constr params per_info.per_params) then
-    user_err ~hdr:"thesis_for"
-      ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
-	 str "cannot give an induction hypothesis (wrong parameters).") in
-  let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
-    compose_prod rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2)))
-
-let rec build_product_dep pat_info per_info args body gls =
-  match args with
-      (Hprop {st_label=nam;st_it=This c}
-      | Hvar {st_label=nam;st_it=c})::rest ->
-	let pprod=
-	  lift 1 (build_product_dep pat_info per_info rest body gls) in
-	let lbody =
-	  match nam with
-	      Anonymous -> body
-	    | Name id -> subst_var id pprod in
-	  mkProd (nam,c,lbody)
-    | Hprop ({st_it=Thesis tk} as st)::rest ->
-	let pprod=
-	  lift 1 (build_product_dep pat_info per_info rest body gls) in
-	let lbody =
-	  match st.st_label with
-	      Anonymous -> body
-	    | Name id -> subst_var id pprod in
-	let ptyp =
-	  match tk with
-	      For id ->
-		let obj = mkVar id in
-		let typ =
-		  try st_assoc (Name id) pat_info.pat_vars
-		  with Not_found ->
-		    snd (st_assoc (Name id) pat_info.pat_aliases) in
-		  thesis_for obj typ per_info (pf_env gls)
-	    | Plain -> EConstr.Unsafe.to_constr (pf_concl gls) in
-	  mkProd (st.st_label,ptyp,lbody)
-    | [] -> body
-
-let build_dep_clause params pat_info per_info hyps gls =
-  let concl=
-    thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in
-  let open_clause =
-    build_product_dep pat_info per_info hyps concl gls in
-  let prod_one st body =
-    match st.st_label with
-	Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body)
-      | Name id -> mkNamedProd id st.st_it (lift 1 body) in
-  let let_one_in st body =
-    match st.st_label with
-	Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body)
-      | Name id ->
-	  mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in
-  let aliased_clause =
-    List.fold_right let_one_in pat_info.pat_aliases open_clause in
-    List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause
-
-let rec register_dep_subcase id env per_info pat = function
-    EK_nodep -> error  "Only \"suppose it is\" can be used here."
-  | EK_unknown ->
-      register_dep_subcase id env per_info pat
-	(EK_dep (start_tree env per_info.per_ind per_info.per_wf))
-  | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
-
-let case_tac params pat_info hyps gls0 =
-  let info = get_its_info gls0 in
-  let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
-  let et,per_info,ek,old_clauses,rest =
-    match info.pm_stack with
-	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest)
-      | _ -> anomaly (Pp.str "wrong place for cases") in
-  let clause = build_dep_clause params pat_info per_info hyps gls0 in
-  let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
-  let nek = 
-    register_dep_subcase (id,(List.length params,List.length hyps)) 
-      (pf_env gls0) per_info pat_info.pat_pat ek in  
-  let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
-    tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause))
-      [tclTHENLIST
-	 [tcl_change_info ninfo1;
-	  assume_st (params@pat_info.pat_vars);
-	  assume_st_letin pat_info.pat_aliases;
-	  assume_hyps_or_theses hyps;
-	  clear old_clauses];
-       tcl_change_info ninfo2] gls0
-
-(* end cases *)
-
-type ('a, 'b) instance_stack =
-    ('b * (('a option * constr list) list)) list
-
-let initial_instance_stack ids : (_, _) instance_stack =
-  List.map (fun id -> id,[None,[]]) ids
-
-let push_one_arg arg = function
-    [] -> anomaly (Pp.str "impossible")
-  | (head,args) :: ctx ->
-      ((head,(arg::args)) :: ctx)
-
-let push_arg arg stacks =
-  List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks
-
-
-let push_one_head c ids (id,stack) =
-  let head = if Id.Set.mem id ids then Some c else None in
-    id,(head,[]) :: stack
-
-let push_head c ids stacks =
-  List.map (push_one_head c ids) stacks
-
-let pop_one (id,stack) =
-  let nstack=
-    match stack with
-	[] -> anomaly (Pp.str "impossible")
-      | [c] as l -> l
-      | (Some head,args)::(head0,args0)::ctx ->
-	  let arg = applist (head,(List.rev args)) in
-	    (head0,(arg::args0))::ctx
-     | (None,args)::(head0,args0)::ctx ->
-	 (head0,(args@args0))::ctx
-  in id,nstack
-
-let pop_stacks stacks =
-  List.map pop_one stacks
-
-let hrec_for fix_id per_info gls obj_id =
-  let obj=mkVar obj_id in
-  let typ=pf_get_hyp_typ gls obj_id in
-  let typ = EConstr.Unsafe.to_constr typ in
-  let rc,hd1=decompose_prod typ in
-  let cind,all_args=decompose_app typ in
-  let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
-  let params,args= List.chop per_info.per_nparams all_args in
-  assert begin
-    try List.for_all2 Term.eq_constr params per_info.per_params with
-        Invalid_argument _ -> false end;
-  let hd2 = applist (mkVar fix_id,args@[obj]) in
-    EConstr.of_constr (compose_lam rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2))))
-
-let warn_missing_case =
-  CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
-    (fun () -> strbrk "missing case")
-
-let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
-  match tree, objs  with
-      Close_patt t,_ ->
-	let args0 = pop_stacks args in
-	  execute_cases fix_name per_info tacnext args0 objs nhrec t gls
-    | Skip_patt (_,t),skipped::next_objs ->
-	let args0 = push_arg skipped args in
-	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
-    | End_patt (id,(nparams,nhyps)),[] -> 
-	begin
-	  match Id.List.assoc id args with
-	      [None,br_args] -> 
-		let all_metas = 
-		  List.init (nparams + nhyps) (fun n -> mkMeta (succ n))  in
-		let param_metas,hyp_metas = List.chop nparams all_metas in
-		  tclTHEN
-		    (tclDO nhrec (Proofview.V82.of_tactic introf))
-		    (tacnext 
-		       (applist (mkVar id,
-				 List.append param_metas 
-				   (List.rev_append br_args hyp_metas)))) gls
-	    | _ -> anomaly (Pp.str "wrong stack size")
-	end
-    | Split_patt (ids,ind,br), casee::next_objs ->
-	let (mind,oind) as spec = Global.lookup_inductive ind in
-	let nparams = mind.mind_nparams in
-	let concl=pf_concl gls in
-	let env=pf_env gls in
-	let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
-	let hd,all_args = decompose_app (special_whd gls ctyp) in
-	let ind', u = destInd hd in
-	let _ = assert (eq_ind ind' ind) in (* just in case *)
-	let params,real_args = List.chop nparams all_args in
-	let abstract_obj c body =
-	  let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
-	    lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
-	let elim_pred = List.fold_right abstract_obj
-	  real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
-        let elim_pred = EConstr.Unsafe.to_constr elim_pred in
-	let case_info = Inductiveops.make_case_info env ind RegularStyle in
-	let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
-	let f_ids typ =
-	  let sign =
-	    (prod_assum (Term.prod_applist typ params)) in
-          let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
-	    find_intro_names sign gls in
-	let constr_args_ids = Array.map f_ids gen_arities in
-	let case_term =
-	  mkCase(case_info,elim_pred,casee,
-		 Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in
-	let branch_tac i (recargs,bro) gls0 =
-	  let args_ids = constr_args_ids.(i) in
-	  let rec aux n = function
-	      [] ->
-		assert (Int.equal n (Array.length recargs));
-		next_objs,[],nhrec
-	    | id :: q ->
-		let objs,recs,nrec = aux (succ n) q in
-		  if recargs.(n)
-		  then (mkVar id::objs),(id::recs),succ nrec
-		  else (mkVar id::objs),recs,nrec in
-	  let objs,recs,nhrec = aux 0 args_ids in
-	    tclTHENLIST
-	      [tclMAP (fun id -> Proofview.V82.of_tactic (intro_mustbe_force id)) args_ids;
-	       begin
-		 fun gls1 ->
-		   let hrecs =
-		     List.map
-		       (fun id ->
-			  hrec_for (out_name fix_name) per_info gls1 id)
-		       recs in
-		     Proofview.V82.of_tactic (generalize hrecs) gls1
-	       end;
-	       match bro with
-		   None ->
-                     warn_missing_case ();
-                     tacnext (mkMeta 1)
-		 | Some (sub_ids,tree) ->
-		     let br_args =
-		       List.filter
-			 (fun (id,_) -> Id.Set.mem id sub_ids) args in
-		     let construct =
-		       applist (mkConstruct(ind,succ i),params) in
-		     let p_args =
-		       push_head construct ids br_args in
-		       execute_cases fix_name per_info tacnext
-			 p_args objs nhrec tree] gls0 in
-	  tclTHENSV
-	    (refine (EConstr.of_constr case_term))
-	    (Array.mapi branch_tac br) gls
-    | Split_patt (_, _, _) , [] ->
-	anomaly ~label:"execute_cases " (Pp.str "Nothing to split")
-    | Skip_patt _ , [] ->
-	anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
-    | End_patt (_,_) , _ :: _  ->
-	anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
-
-let understand_my_constr env sigma c concl =
-  let env = env in
-  let c = EConstr.of_constr c in
-  let rawc = Detyping.detype false [] env Evd.empty c in
-  let rec frob = function
-    | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
-    | rc ->  map_glob_constr frob rc
-  in
-  Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
-
-let my_refine c gls =
-  let oc = { run = begin fun sigma ->
-    let sigma = Sigma.to_evar_map sigma in
-    let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
-    Sigma.Unsafe.of_pair (c, sigma)
-  end } in
-  Proofview.V82.of_tactic (Tactics.New.refine oc) gls
-
-(* end focus/claim *)
-
-let end_tac et2 gls =
-  let info = get_its_info gls in
-  let et1,pi,ek,clauses =
-    match info.pm_stack with
-	Suppose_case::_ ->
-	  anomaly (Pp.str "This case should already be trapped")
-      | Claim::_ ->
-	  error "\"end claim\" expected."
-      | Focus_claim::_ ->
-	  error "\"end focus\" expected."
-      | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses)
-      | [] ->
-	  anomaly (Pp.str "This case should already be trapped") in
-  let et = match et1, et2 with
-  | ET_Case_analysis, ET_Case_analysis -> et1
-  | ET_Induction, ET_Induction -> et1
-  | ET_Case_analysis, _ -> error "\"end cases\" expected."
-  | ET_Induction, _ -> error "\"end induction\" expected."
-  in
-    tclTHEN
-      tcl_erase_info
-      begin
-	match et,ek with
-	    _,EK_unknown ->
-	      tclSOLVE [Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr pi.per_casee))]
-	  | ET_Case_analysis,EK_nodep ->
-	      tclTHEN
-		(Proofview.V82.of_tactic (simplest_case (EConstr.of_constr pi.per_casee)))
-		(default_justification (List.map mkVar clauses))
-	  | ET_Induction,EK_nodep ->
-	      tclTHENLIST
-		[Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee])));
-		 Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
-		 default_justification (List.map mkVar clauses)]
-	  | ET_Case_analysis,EK_dep tree ->
-		 execute_cases Anonymous pi 
-		   (fun c -> tclTHENLIST 
-		      [my_refine c;
-		       clear clauses;
-		       justification (Proofview.V82.of_tactic assumption)])
-		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
-	  | ET_Induction,EK_dep tree ->
-	      let nargs = (List.length pi.per_args) in
-		tclTHEN (Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee]))))
-		  begin
-		    fun gls0 ->
-		      let fix_id =
-			pf_get_new_id (Id.of_string "_fix") gls0 in
-		      let c_id =
-			pf_get_new_id (Id.of_string "_main_arg") gls0 in
-			tclTHENLIST
-			  [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
-			   tclDO nargs (Proofview.V82.of_tactic introf);
-			   Proofview.V82.of_tactic (intro_mustbe_force c_id);
-			   execute_cases (Name fix_id) pi
-			     (fun c ->
-				tclTHENLIST
-				  [clear [fix_id];
-				   my_refine c;
-				   clear clauses;
-				   justification (Proofview.V82.of_tactic assumption)])
-			     (initial_instance_stack clauses)
-			     [mkVar c_id]  0 tree] gls0
-		  end
-      end gls
-
-(* escape *)
-
-let escape_tac gls =
-  (* spiwack: sets an empty info stack to avoid interferences.
-     We could erase the info altogether, but that doesn't play
-     well with the Decl_mode.focus (used in post_processing). *)
-  let info={pm_stack=[]} in
-  tcl_change_info info gls
-
-(* General instruction engine *)
-
-let rec do_proof_instr_gen _thus _then instr =
-  match instr with
-      Pthus i ->
-	assert (not _thus);
-	do_proof_instr_gen true _then i
-    | Pthen i ->
-	assert (not _then);
-	do_proof_instr_gen _thus true i
-    | Phence i ->
-	assert (not (_then || _thus));
-	do_proof_instr_gen true true i
-    | Pcut c ->
-	instr_cut mk_stat_or_thesis _thus _then c
-    | Psuffices c ->
-	instr_suffices _then c
-    | Prew (s,c) ->
-	assert (not _then);
-	instr_rew _thus s c
-    | Pconsider (c,hyps)    -> consider_tac c hyps
-    | Pgiven hyps            -> given_tac hyps
-    | Passume hyps           -> assume_tac hyps
-    | Plet hyps              -> assume_tac hyps
-    | Pclaim st              -> instr_claim false st
-    | Pfocus st              -> instr_claim true st
-    | Ptake witl             -> take_tac witl
-    | Pdefine (id,args,body) -> define_tac id args body
-    | Pcast (id,typ)         -> cast_tac id typ
-    | Pper (et,cs)           -> per_tac et cs
-    | Psuppose hyps      -> suppose_tac hyps
-    | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
-    | Pend (B_elim et) -> end_tac et
-    | Pend _ -> anomaly (Pp.str "Not applicable")
-    | Pescape -> escape_tac
-
-let eval_instr {instr=instr} =
-  do_proof_instr_gen false false instr
-
-let rec preprocess pts instr =
-  match instr with
-    Phence i |Pthus i | Pthen i -> preprocess pts i
-  | Psuffices _ | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _
-  | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _
-  | Pdefine (_,_,_) | Pper _ | Prew _ ->
-      check_not_per pts;
-      true
-  | Pescape ->
-      check_not_per pts;
-      true
-  | Pcase _ | Psuppose _ | Pend (B_elim _) ->
-      close_previous_case pts ;
-      true
-  | Pend bt ->
-      close_block bt pts ;
-      false
-
-let rec postprocess pts instr =
-  match instr with
-      Phence i | Pthus i | Pthen i -> postprocess pts i
-    | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
-    | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> ()
-    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ ->
-      Decl_mode.focus pts
-    | Pescape ->
-      Decl_mode.focus pts;
-      Proof_global.set_proof_mode "Classic"
-    | Pend (B_elim ET_Induction) ->
-  	begin
-	  let pfterm = List.hd (Proof.partial_proof pts) in
-	  let pfterm = EConstr.Unsafe.to_constr pfterm in
-	  let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in
-	  let env =  try
-		       Goal.V82.env sigma (List.hd gls)
-	             with Failure "hd" ->
-		       Global.env ()
-	  in
-	    try
-	      Inductiveops.control_only_guard env pfterm;
-	      goto_current_focus_or_top ()
- 	    with
-		Type_errors.TypeError(env,
-				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
-		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
-	end
-    | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
-    | Pend B_proof -> Proof_global.set_proof_mode "Classic"
-    | Pend _ -> ()
-
-let do_instr raw_instr pts =
-  let has_tactic = preprocess pts raw_instr.instr in
-  (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
-     current proof (and, actually so does [do_instr] later one, so
-     it's ok to do the same here. Ideally the proof should be properly
-     threaded through the commands here, but since the are interleaved
-     with actions on the proof mode, which is attached to the global
-     proof environment, it is not possible without heavy lifting. *)
-  let pts = Proof_global.give_me_the_proof () in
-  let pts =
-    if has_tactic then
-            let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
-      let gl = { it=List.hd gls ; sigma=sigma; } in
-      let env=  pf_env gl in
-      let ist = {ltacvars = Id.Set.empty; genv = env} in
-      let glob_instr = intern_proof_instr ist raw_instr in
-      let instr =
-	interp_proof_instr (get_its_info gl) env sigma glob_instr in
-      let (pts',_) = Proof.run_tactic (Global.env())
-        (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
-      pts'
-    else pts
-  in
-  Proof_global.simple_with_current_proof (fun _ _ -> pts);
-  postprocess pts raw_instr.instr
-
-let proof_instr raw_instr =
-  let p = Proof_global.give_me_the_proof () in
-  do_instr raw_instr p
-
-(*
-
-(* STUFF FOR ITERATED RELATIONS *)
-let decompose_bin_app t=
-  let hd,args = destApp
-
-let identify_transitivity_lemma c =
-  let varx,tx,c1 = destProd c in
-  let vary,ty,c2 = destProd (pop c1) in
-  let varz,tz,c3 = destProd (pop c2) in
-  let _,p1,c4 = destProd (pop c3) in
-  let _,lp2,lp3 = destProd (pop c4) in
-  let p2=pop lp2 in
-  let p3=pop lp3 in
-*)
-
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
deleted file mode 100644
index ba196ff01..000000000
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ /dev/null
@@ -1,108 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Tacmach
-open Decl_mode
-
-val go_to_proof_mode: unit -> unit
-val return_from_tactic_mode: unit -> unit
-
-val register_automation_tac: unit Proofview.tactic -> unit
-
-val automation_tac : unit Proofview.tactic
-
-val concl_refiner:
-  Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
-
-val do_instr: Decl_expr.raw_proof_instr -> Proof.proof -> unit
-val proof_instr: Decl_expr.raw_proof_instr -> unit
-
-val tcl_change_info : Decl_mode.pm_info -> tactic
-
-val execute_cases :
-    Name.t ->
-    Decl_mode.per_info ->
-    (Term.constr -> Proof_type.tactic) ->
-    (Id.Set.elt * (Term.constr option * Term.constr list) list) list ->
-    Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
-
-val tree_of_pats : 
-  Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
-  split_tree
-
-val add_branch : 
-  Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
-  split_tree -> split_tree
-
-val append_branch :
-  Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
-  (Id.Set.t * Decl_mode.split_tree) option ->
-  (Id.Set.t * Decl_mode.split_tree) option
-
-val append_tree :
-  Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
-  split_tree -> split_tree
-
-val build_dep_clause :   Term.types Decl_expr.statement list ->
-    Decl_expr.proof_pattern ->
-    Decl_mode.per_info ->
-    (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis)
-    Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
-
-val register_dep_subcase :    
-    Id.t * (int * int) ->
-    Environ.env ->
-    Decl_mode.per_info ->
-    Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
-
-val thesis_for :     Term.constr ->
-    Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr
-
-val close_previous_case : Proof.proof -> unit
-
-val pop_stacks :
-  (Id.t *
-     (Term.constr option * Term.constr list) list) list ->
-  (Id.t *
-     (Term.constr option * Term.constr list) list) list
-
-val push_head :   Term.constr ->
-  Id.Set.t ->
-  (Id.t *
-     (Term.constr option * Term.constr list) list) list ->
-  (Id.t *
-     (Term.constr option * Term.constr list) list) list
-
-val push_arg : Term.constr ->
-  (Id.t *
-     (Term.constr option * Term.constr list) list) list ->
-  (Id.t *
-     (Term.constr option * Term.constr list) list) list
-
-val hrec_for:
-    Id.t ->
-    Decl_mode.per_info -> Proof_type.goal Tacmach.sigma ->
-    Id.t -> EConstr.constr
-
-val consider_match :
-   bool ->
-    (Id.Set.elt*bool) list ->
-    Id.Set.elt list ->
-    (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
-    Proof_type.tactic
-
-val init_tree:
-    Id.Set.t ->
-    inductive ->
-    int option * Declarations.wf_paths ->
-    (int ->
-     (int option * Declarations.recarg Rtree.t) array ->
-     (Id.Set.t * Decl_mode.split_tree) option) ->
-    Decl_mode.split_tree
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
deleted file mode 100644
index a71d20f0d..000000000
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ /dev/null
@@ -1,387 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-DECLARE PLUGIN "decl_mode_plugin"
-
-open Ltac_plugin
-open Compat
-open Pp
-open Decl_expr
-open Names
-open Pcoq
-open Vernacexpr
-open Tok (* necessary for camlp4 *)
-
-open Pcoq.Constr
-open Pltac
-open Ppdecl_proof
-
-let pr_goal gs =
-  let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
-  let env = Goal.V82.env sigma g in
-  let concl = Goal.V82.concl sigma g in
-  let goal =
-    Printer.pr_context_of env sigma ++ cut () ++
-      str "============================" ++ cut ()  ++
-      str "thesis :=" ++ cut () ++
-      Printer.pr_goal_concl_style_env env sigma concl in
-  str "     *** Declarative Mode ***" ++ fnl () ++ fnl () ++
-    str "  " ++ v 0 goal
-
-let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
-  match gll with
-  | [goal] when pr_first ->
-      pr_goal { Evd.it = goal ; sigma = sigma }
-  | _ ->
-      (* spiwack: it's not very nice to have to call proof global
-         here, a more robust solution would be to add a hook for
-         [Printer.pr_open_subgoals] in proof modes, in order to
-         compute the end command. Yet a more robust solution would be
-         to have focuses give explanations of their unfocusing
-         behaviour. *)
-      let p = Proof_global.give_me_the_proof () in
-      let close_cmd = Decl_mode.get_end_command p in
-      str "Subproof completed, now type " ++ str close_cmd ++ str "."
-
-let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
-  Decl_interp.interp_proof_instr 
-    (Decl_mode.get_info sigma gl)
-    (Goal.V82.env sigma gl)
-    (sigma)
-
-let vernac_decl_proof () = 
-  let pf = Proof_global.give_me_the_proof () in
-  if Proof.is_done pf then 
-    CErrors.error "Nothing left to prove here."
-  else
-    begin
-      Decl_proof_instr.go_to_proof_mode () ;
-      Proof_global.set_proof_mode "Declarative"
-    end
-
-(* spiwack: some bureaucracy is not performed here *)
-let vernac_return () =
-  begin
-    Decl_proof_instr.return_from_tactic_mode () ;
-    Proof_global.set_proof_mode "Declarative"
-  end
-
-let vernac_proof_instr instr =
-  Decl_proof_instr.proof_instr instr
-
-(* Before we can write an new toplevel command (see below) 
-    which takes a [proof_instr] as argument, we need to declare
-    how to parse it, print it, globalise it and interprete it.
-    Normally we could do that easily through ARGUMENT EXTEND, 
-    but as the parsing is fairly complicated we will do it manually to
-    indirect through the [proof_instr] grammar entry. *)
-(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
-
-(* Only declared at raw level, because only used in vernac commands. *)
-let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
-  Genarg.make0 "proof_instr"
-
-(* We create a new parser entry [proof_mode]. The Declarative proof mode
-    will replace the normal parser entry for tactics with this one. *)
-let proof_mode : vernac_expr Gram.entry =
-  Gram.entry_create "vernac:proof_command"
-(* Auxiliary grammar entry. *)
-let proof_instr : raw_proof_instr Gram.entry =
-  Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
-
-let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
-  pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
-
-let classify_proof_instr = function
-  | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
-  | _ -> Vernac_classifier.classify_as_proofstep
-
-(* We use the VERNAC EXTEND facility with a custom non-terminal
-    to populate [proof_mode] with a new toplevel interpreter.
-    The "-" indicates that the rule does not start with a distinguished
-    string. *)
-VERNAC proof_mode EXTEND ProofInstr
-  [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ]
-END
-
-(* It is useful to use GEXTEND directly to call grammar entries that have been
-    defined previously VERNAC EXTEND. In this case we allow, in proof mode,
-    the use of commands like Check or Print. VERNAC EXTEND does quite a bit of
-    bureaucracy for us, but it is not needed in this sort of case, and it would require
-    to have an ARGUMENT EXTEND version of the "proof_mode" grammar entry. *)
-GEXTEND Gram
-  GLOBAL: proof_mode ;
-
-  proof_mode: LAST
-    [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ]
-  ;
-END  
-
-(* We register a new proof mode here *)
-
-let _ = 
-  Proof_global.register_proof_mode { Proof_global.
-				       name = "Declarative" ; (* name for identifying and printing *)
-				       (* function [set] goes from No Proof Mode to 
-					   Declarative Proof Mode performing side effects *)
-				       set = begin fun () ->
-					 (* We set the command non terminal to
-					     [proof_mode] (which we just defined). *)
-					 Pcoq.set_command_entry proof_mode ;
-					 (* We substitute the goal printer, by the one we built
-					     for the proof mode. *)
-					 Printer.set_printer_pr { Printer.default_printer_pr with
-								                Printer.pr_goal = pr_goal;
-                                                                                pr_subgoals = pr_subgoals; }
-				       end ;
-                                       (* function [reset] goes back to No Proof Mode from
-					   Declarative Proof Mode *)
-				       reset = begin fun () ->
-					 (* We restore the command non terminal to
-					      [noedit_mode]. *)
-					 Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
-					 (* We restore the goal printer to default *)
-					 Printer.set_printer_pr Printer.default_printer_pr
-				       end
-				   }
-
-VERNAC COMMAND EXTEND DeclProof
-[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
-END
-VERNAC COMMAND EXTEND  DeclReturn
-[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ]
-END
-
-let none_is_empty = function
-    None -> []
-  | Some l -> l
-
-GEXTEND Gram
-GLOBAL: proof_instr;
-  thesis :
-    [[ "thesis" -> Plain 
-     | "thesis"; "for"; i=ident -> (For i)
-     ]];
-  statement :
-    [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
-     | i=ident -> {st_label=Anonymous;
-		   st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
-     | c=constr -> {st_label=Anonymous;st_it=c}
-     ]];
-  constr_or_thesis :
-     [[ t=thesis -> Thesis t ] |
-      [ c=constr -> This c
-      ]];
-  statement_or_thesis : 
-    [
-      [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] 
-    |
-      [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
-      | i=ident -> {st_label=Anonymous;
-		    st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
-      | c=constr -> {st_label=Anonymous;st_it=This c}
-      ]
-    ];
-  justification_items : 
-    [[ -> Some [] 
-     | "by"; l=LIST1 constr SEP "," -> Some l
-     | "by"; "*"                    -> None ]]
-  ;
-  justification_method : 
-    [[ -> None 
-     | "using";  tac = tactic -> Some tac ]]
-  ;
-  simple_cut_or_thesis :
-    [[ ls = statement_or_thesis;
-       j = justification_items;
-       taco = justification_method 	
-	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
-  ;
-  simple_cut :
-    [[ ls = statement;
-       j = justification_items;
-       taco = justification_method 	
-	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
-  ;
-  elim_type:
-    [[ IDENT "induction" -> ET_Induction
-     | IDENT "cases" -> ET_Case_analysis ]]
-  ;
-  block_type :
-    [[ IDENT "claim" -> B_claim
-     | IDENT "focus" -> B_focus
-     | IDENT "proof" -> B_proof
-     | et=elim_type -> B_elim et ]]
-  ;    
-  elim_obj:
-    [[ IDENT "on"; c=constr -> Real c
-     | IDENT "of"; c=simple_cut -> Virtual c ]]
-  ;  
-  elim_step:
-    [[ IDENT "consider" ; 
-       h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
-     | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)
-     | IDENT "suffices"; ls=suff_clause;
-       j = justification_items;
-       taco = justification_method 	
-	-> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] 
-  ;
-  rew_step :
-    [[ "~=" ;         c=simple_cut -> (Rhs,c)       
-     | "=~" ;         c=simple_cut -> (Lhs,c)]]
-  ;
-  cut_step:
-    [[ "then"; tt=elim_step -> Pthen tt
-     | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c)
-     | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) 
-     | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c)
-     | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c)
-     | tt=elim_step -> tt
-     | tt=rew_step -> let s,c=tt in Prew (s,c); 
-     | IDENT "have"; c=simple_cut_or_thesis -> Pcut c;
-     | IDENT "claim"; c=statement -> Pclaim c;
-     | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c;    
-     | "end"; bt = block_type -> Pend bt;
-     | IDENT "escape" -> Pescape ]]
-  ;
-  (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*)
-  loc_id: 
-    [[ id=ident -> fun x -> (!@loc,(id,x)) ]];
-  hyp:
-    [[ id=loc_id -> id None ;
-     | id=loc_id ; ":" ; c=constr -> id (Some c)]]
-  ;
-  consider_vars:
-    [[ name=hyp -> [Hvar name]
-     | name=hyp; ","; v=consider_vars -> (Hvar name) :: v
-     | name=hyp; 
-       IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h
-     ]]
-  ;
-  consider_hyps:  
-    [[ st=statement; IDENT "and"; h=consider_hyps  -> Hprop st::h
-     | st=statement; IDENT "and"; 
-       IDENT "consider" ; v=consider_vars  -> Hprop st::v
-     | st=statement -> [Hprop st]
-     ]]
-  ;  
-  assume_vars:
-    [[ name=hyp -> [Hvar name]
-     | name=hyp; ","; v=assume_vars -> (Hvar name) :: v
-     | name=hyp; 
-       IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h
-     ]]
-  ;
-  assume_hyps:  
-    [[ st=statement; IDENT "and"; h=assume_hyps  -> Hprop st::h
-     | st=statement; IDENT "and"; 
-       IDENT "we"; IDENT "have" ; v=assume_vars  -> Hprop st::v
-     | st=statement -> [Hprop st]
-     ]]
-  ;
-  assume_clause:
-    [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v
-    |  h=assume_hyps -> h ]]
-  ; 
-  suff_vars:
-    [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
-      [Hvar name],c
-     | name=hyp; ","; v=suff_vars -> 
-	 let (q,c) = v in ((Hvar name) :: q),c
-     | name=hyp; 
-       IDENT "such"; IDENT "that"; h=suff_hyps -> 
-	 let (q,c) = h in ((Hvar name) :: q),c
-     ]];
-  suff_hyps:  
-    [[ st=statement; IDENT "and"; h=suff_hyps  ->	 
-	 let (q,c) = h in (Hprop st::q),c
-     | st=statement; IDENT "and"; 
-       IDENT "to" ; IDENT "have" ; v=suff_vars -> 
-	 let (q,c) = v in (Hprop st::q),c
-     | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> 
-	 [Hprop st],c
-     ]]
-  ;
-  suff_clause:
-    [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v
-    |  h=suff_hyps -> h ]]
-  ; 
-  let_vars:
-    [[ name=hyp -> [Hvar name]
-     | name=hyp; ","; v=let_vars -> (Hvar name) :: v
-     | name=hyp; IDENT "be"; 
-       IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h
-     ]]
-  ;
-  let_hyps:  
-    [[ st=statement; IDENT "and"; h=let_hyps  -> Hprop st::h
-    |  st=statement; IDENT "and"; "let"; v=let_vars  -> Hprop st::v
-    |  st=statement -> [Hprop st]
-    ]];
-  given_vars:
-    [[ name=hyp -> [Hvar name]
-     | name=hyp; ","; v=given_vars -> (Hvar name) :: v
-     | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h
-     ]]
-  ;
-  given_hyps:  
-    [[ st=statement; IDENT "and"; h=given_hyps  -> Hprop st::h
-    |  st=statement; IDENT "and"; IDENT "given"; v=given_vars  -> Hprop st::v
-    |  st=statement -> [Hprop st]
-    ]];
-  suppose_vars:
-    [[name=hyp -> [Hvar name] 
-     |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v
-     |name=hyp; OPT[IDENT "be"]; 
-      IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h
-     ]]
-  ;
-  suppose_hyps:  
-    [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h
-     | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have";
-          v=suppose_vars -> Hprop st::v
-     | st=statement_or_thesis -> [Hprop st]
-     ]]
-  ;
-  suppose_clause:
-    [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v;
-     |  h=suppose_hyps -> h ]]
-  ;
-  intro_step:
-    [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
-     | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
-       po=OPT[ "with"; p=LIST1 hyp SEP ","-> p  ] ; 
-       ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> 
-	 Pcase (none_is_empty po,c,none_is_empty ho)
-     | "let" ; v=let_vars -> Plet v	 
-     | IDENT "take"; witnesses = LIST1 constr SEP ","  -> Ptake witnesses
-     | IDENT "assume"; h=assume_clause -> Passume h
-     | IDENT "given"; h=given_vars -> Pgiven h
-     | IDENT "define"; id=ident; args=LIST0 hyp; 
-       "as"; body=constr -> Pdefine(id,args,body)
-     | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ)
-     | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ)
-     ]]
-  ;
-  emphasis : 
-    [[ -> 0
-     | "*" -> 1
-     | "**" -> 2
-     | "***" -> 3
-     ]]
-  ;
-  bare_proof_instr:
-    [[ c = cut_step -> c ;
-     | i = intro_step -> i ]]
-  ;
-  proof_instr :
-    [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]]
-  ;
-END;;
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
deleted file mode 100644
index 92045e775..000000000
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ /dev/null
@@ -1,218 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Pp
-open Decl_expr
-open Names
-open Nameops
-
-let pr_label = function
-    Anonymous -> mt ()
-  | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
-
-let pr_justification_items pr_constr = function
-    Some [] -> mt ()
-  | Some (_::_ as l) ->
-      spc () ++ str "by" ++ spc () ++
-	prlist_with_sep (fun () -> str ",") pr_constr l
-  | None -> spc () ++ str "by *"
-
-let pr_justification_method pr_tac = function
-    None -> mt ()
-  | Some tac ->
-      spc () ++ str "using" ++ spc () ++ pr_tac tac
-
-let pr_statement pr_constr st =
-  pr_label st.st_label ++ pr_constr st.st_it
-
-let pr_or_thesis pr_this = function
-    Thesis Plain -> str "thesis"
-  | Thesis (For id) ->
-      str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
-  | This c -> pr_this c
-
-let pr_cut pr_constr pr_tac pr_it c =
-  hov 1 (pr_it c.cut_stat) ++
-    pr_justification_items pr_constr c.cut_by ++
-    pr_justification_method pr_tac c.cut_using
-
-let type_or_thesis = function
-    Thesis _ -> Term.mkProp
-  | This c -> c
-
-let _I x = x
-
-let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps =
-  let pr_sep = if sep then str "and" ++ spc () else mt () in
-    match hyps with
-	(Hvar _ ::_) as rest ->
-	  spc () ++ pr_sep ++ str _have ++
-	    pr_vars pr_var pr_constr gtyp false _be _have rest
-      | Hprop st :: rest ->
-	  begin
-	(* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) 
-	      spc() ++ pr_sep ++ pr_statement pr_constr st ++
-		pr_hyps pr_var pr_constr gtyp true _be _have rest
-	  end
-      | [] -> mt ()
-
-and pr_vars pr_var pr_constr gtyp sep _be _have vars =
-  match vars with
-    Hvar st :: rest ->
-      begin
-	(* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) 
-	let pr_sep = if sep then pr_comma () else mt () in
-		spc() ++ pr_sep ++
-		  pr_var st ++
-		  pr_vars pr_var pr_constr gtyp true _be _have rest
-      end
-   | (Hprop _ :: _) as rest ->
-      let _st =  if _be then
-	str "be such that"
-      else
-	str "such that" in
-	spc() ++ _st ++  pr_hyps pr_var pr_constr gtyp false _be _have rest
-  | [] -> mt ()
-
-let pr_suffices_clause pr_var pr_constr (hyps,c) =
-    pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++
-       str "to show" ++ spc () ++ pr_or_thesis pr_constr c
-
-let pr_elim_type = function
-    ET_Case_analysis -> str "cases"
-  | ET_Induction -> str "induction"
-
-let pr_block_type = function
-    B_elim et -> pr_elim_type et
-  | B_proof -> str "proof"
-  | B_claim -> str "claim"
-  | B_focus -> str "focus"
-
-let pr_casee pr_constr pr_tac =function
-    Real c -> str "on" ++ spc () ++ pr_constr c
-  | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut
-
-let pr_side = function
-    Lhs -> str "=~"
-  | Rhs -> str "~="
-
-let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function
-  | Pescape -> str "escape"
-  | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac  true _thus i
-  | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac  _then true i
-  | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i
-  | Pcut c ->
-      begin
-	match _then,_thus with
-	    false,false -> str "have" ++ spc () ++
-	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
-	  | false,true  -> str "thus" ++ spc () ++
-	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
-	  | true,false  -> str "then" ++ spc () ++
-	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
-	  | true,true   -> str "hence" ++ spc () ++
-	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
-      end
-  | Psuffices c ->
-      str "suffices" ++  pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c
-  | Prew (sid,c) ->
-      (if _thus then str "thus" else str "    ") ++ spc () ++
-	pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c
-  | Passume hyps ->
-      str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps
-  | Plet hyps ->
-      str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps
-  | Pclaim st ->
-      str "claim" ++ spc () ++ pr_statement pr_constr st
-  | Pfocus st ->
-      str "focus on" ++ spc () ++ pr_statement pr_constr st
-  | Pconsider (id,hyps) ->
-      str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps
-      ++ spc () ++ str "from " ++ pr_constr id
-  | Pgiven hyps ->
-      str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps
-  | Ptake witl ->
-      str "take" ++ spc () ++
-	prlist_with_sep pr_comma pr_constr witl
-  | Pdefine (id,args,body) ->
-      str "define" ++ spc () ++ pr_id id ++ spc () ++
-	prlist_with_sep spc
-	(fun st -> str "(" ++
-	   pr_var st ++ str ")") args ++ spc () ++
-	str "as" ++ (pr_constr body)
-  | Pcast (id,typ) ->
-      str "reconsider" ++ spc () ++
-	pr_or_thesis pr_id id ++ spc () ++
-	str "as" ++ spc () ++ (pr_constr typ)
-  | Psuppose hyps ->
-      str "suppose" ++
-	pr_hyps pr_var pr_constr _I false false "we have" hyps 
-  | Pcase (params,pat,hyps) ->
-      str "suppose it is" ++ spc () ++ pr_pat pat ++
-	(if params = [] then mt () else
-	   (spc () ++ str "with" ++ spc () ++
-	      prlist_with_sep spc
-	      (fun st -> str "(" ++
-		 pr_var st ++ str ")") params ++ spc ()))
-      ++
-	(if hyps = [] then mt () else
-	   (spc () ++ str "and" ++
-	      pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis
-	      false false "we have" hyps)) 
-  | Pper (et,c) -> 
-      str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
-	pr_casee pr_constr pr_tac c  
-  | Pend blk -> str "end" ++ spc () ++ pr_block_type blk
-
-let pr_emph = function
-    0 -> str "    "
-  | 1 -> str "*   "
-  | 2 -> str "**  "
-  | 3 -> str "*** "
-  | _ -> anomaly (Pp.str "unknown emphasis")
-
-let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr =
-  pr_emph instr.emph ++ spc () ++
-    pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr
-
-
-let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) =
-   pr_gen_proof_instr
-     (fun (_,(id,otyp)) -> 
-       match otyp with
-	 None -> pr_id id
-       | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")"
-     )
-     pconstr2
-     Ppconstr.pr_cases_pattern_expr
-     (ptac Pptactic.ltop)
-     instr
-
-let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
-    pr_gen_proof_instr
-      (fun (_,(id,otyp)) -> 
-	match otyp with
-	  None -> pr_id id
-	| Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")")
-     pconstr2
-     Ppconstr.pr_cases_pattern_expr
-     (ptac Pptactic.ltop)
-     instr
-
-let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
-  let pconstr1 c = pconstr1 (EConstr.of_constr c) in
-  let pconstr2 c = pconstr2 (EConstr.of_constr c) in
-  pr_gen_proof_instr
-    (fun st -> pr_statement pconstr1 st)
-    pconstr2
-    (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr)
-    (ptac Pptactic.ltop)
-    instr
-
diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
deleted file mode 100644
index 678fc0768..000000000
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-
-open Decl_expr
-open Pptactic
-
-val pr_gen_proof_instr : 
-  ('var -> Pp.std_ppcmds) ->
-  ('constr -> Pp.std_ppcmds) ->
-  ('pat -> Pp.std_ppcmds) ->
-  ('tac -> Pp.std_ppcmds) ->  
-  ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
-
-val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
-val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
-val pr_proof_instr : proof_instr extra_genarg_printer
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index e28d6aa62..3c0319319 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -159,21 +159,3 @@ END
 
 open Proofview.Notations
 open Cc_plugin
-open Decl_mode_plugin
-
-let default_declarative_automation =
-  Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
-  Tacticals.New.tclORELSE
-    (Tacticals.New.tclORELSE (Auto.h_trivial [] None)
-    (Cctac.congruence_tac !congruence_depth []))
-    (Proofview.V82.tactic (gen_ground_tac true
-       (Some (Tacticals.New.tclTHEN
-		(snd (default_solver ()))
-		(Cctac.congruence_tac !congruence_depth [])))
-       [] []))
-
-
-
-let () =
-  Decl_proof_instr.register_automation_tac default_declarative_automation
-
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1ec52718a..38fdfb759 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
@@ -348,10 +348,10 @@ END
 open EConstr
 open Vars
 
-let constr_flags = {
+let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
@@ -360,7 +360,7 @@ let refine_tac ist simple with_classes c =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags =
-      { constr_flags with Pretyping.use_typeclasses = with_classes } in
+      { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma ->
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index e9a6e9e04..dfa8331ff 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -46,7 +46,7 @@ let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 928646bcb..50f43931e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   Proofview.NonLogical.run (db_constr (curr_debug ist) env evd c);
   (evd,c)
 
-let constr_flags = {
+let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  interp_gen kind ist false constr_flags env sigma c
+  interp_gen kind ist false (constr_flags ()) env sigma c
 
 let interp_constr = interp_constr_gen WithoutTypeConstraint
 
 let interp_type = interp_constr_gen IsType
 
-let open_constr_use_classes_flags = {
+let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
-let open_constr_no_classes_flags = {
+let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
@@ -679,11 +679,11 @@ let pure_open_constr_flags = {
   expand_evars = false }
 
 (* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
   let flags =
-    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
-    else open_constr_use_classes_flags in
-  interp_gen expected_type ist false flags
+    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
+    else open_constr_use_classes_flags () in
+  interp_gen expected_type ist false flags env sigma c
 
 let interp_pure_open_constr ist =
   interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
@@ -1789,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             (TacLetTac(na,c,clp,b,eqpat))
 	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
                (let_pat_tac b (interp_name ist env sigma na)
-                  ((sigma,sigma'),c) clp eqpat) sigma')
+                  (sigma,c) clp eqpat) sigma')
       end }
 
   (* Derived basic tactics *)