Final part of moving Program code inside the main code. Adapted add_definition/fixpoint and parsing of the "Program" prefix.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7

30 files changed, 4 insertions, 3512 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 449dcd20eb..31814b141e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -361,12 +361,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
-	let ce,imps =
-	  Command.interp_definition bl None body (Some ret_type)
-	in
-	Command.declare_definition
-	  fname (Decl_kinds.Global,Decl_kinds.Definition)
-	  ce imps (fun _ _ -> ())
+	Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
+	  bl None body (Some ret_type) (fun _ _ -> ())
     | _ ->
 	Command.do_fixpoint fixpoint_exprl
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index f6500f74de..bb59a5c9cc 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -55,7 +55,7 @@ val jmeq_refl : unit -> Term.constr
 val new_save_named : bool -> unit
 
 val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  Tacexpr.declaration_hook -> unit
+  unit Tacexpr.declaration_hook -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
@@ -63,7 +63,7 @@ val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_k
 val get_proof_clean : bool ->
   Names.identifier *
     (Entries.definition_entry * Decl_kinds.goal_kind *
-       Tacexpr.declaration_hook)
+      unit Tacexpr.declaration_hook)
 
 
 
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
deleted file mode 100644
index 0bde8dca9c..0000000000
--- a/plugins/subtac/eterm.ml
+++ /dev/null
@@ -1,260 +0,0 @@
-(**
-   - Get types of existentials ;
-   - Flatten dependency tree (prefix order) ;
-   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
-   - Apply term prefixed by quantification on "existentials".
-*)
-
-open Term
-open Sign
-open Names
-open Evd
-open List
-open Pp
-open Errors
-open Util
-open Subtac_utils
-open Proof_type
-
-let trace s =
-  if !Flags.debug then (msgnl s; msgerr s)
-  else ()
-
-let succfix (depth, fixrels) =
-  (succ depth, List.map succ fixrels)
-
-type oblinfo =
-  { ev_name: int * identifier;
-    ev_hyps: named_context;
-    ev_status: obligation_definition_status;
-    ev_chop: int option;
-    ev_src: hole_kind located;
-    ev_typ: types;
-    ev_tac: tactic option;
-    ev_deps: Intset.t }
-
-(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
-open Store.Field
-let evar_tactic = Store.field ()
-
-(** Substitute evar references in t using De Bruijn indices,
-  where n binders were passed through. *)
-
-let subst_evar_constr evs n idf t = 
-  let seen = ref Intset.empty in
-  let transparent = ref Idset.empty in
-  let evar_info id = List.assoc id evs in
-  let rec substrec (depth, fixrels) c = match kind_of_term c with
-    | Evar (k, args) ->
-	let { ev_name = (id, idstr) ;
-	      ev_hyps = hyps ; ev_chop = chop } =
-	  try evar_info k
-	  with Not_found ->
-	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
-	in
-        seen := Intset.add id !seen;
-	  (* Evar arguments are created in inverse order,
-	     and we must not apply to defined ones (i.e. LetIn's)
-	  *)
-	let args =
-	  let n = match chop with None -> 0 | Some c -> c in
-	  let (l, r) = list_chop n (List.rev (Array.to_list args)) in
-	    List.rev r
-	in
-	let args =
-	  let rec aux hyps args acc =
-	     match hyps, args with
-		 ((_, None, _) :: tlh), (c :: tla) ->
-		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
-	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
-		   aux tlh tla acc
-	       | [], [] -> acc
-	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
-	  in aux hyps args []
-	in
-	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
-	    transparent := Idset.add idstr !transparent;
-	  mkApp (idf idstr, Array.of_list args)
-    | Fix _ ->
-	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
-    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
-  in
-  let t' = substrec (0, []) t in
-    t', !seen, !transparent
-
-
-(** Substitute variable references in t using De Bruijn indices,
-  where n binders were passed through. *)
-let subst_vars acc n t =
-  let var_index id = Util.list_index id acc in
-  let rec substrec depth c = match kind_of_term c with
-    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
-    | _ -> map_constr_with_binders succ substrec depth c
-  in
-    substrec 0 t
-
-(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
-    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
-    Changes evars and hypothesis references to variable references.
-*)
-let etype_of_evar evs hyps concl =
-  let rec aux acc n = function
-      (id, copt, t) :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar t in
-	let t'' = subst_vars acc 0 t' in
-	let rest, s', trans' = aux (id :: acc) (succ n) tl in
-	let s' = Intset.union s s' in
-	let trans' = Idset.union trans trans' in
-	  (match copt with
-	      Some c -> 
-		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
-		let c' = subst_vars acc 0 c' in
-		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
-		Intset.union s'' s',
-		Idset.union trans'' trans'
-	    | None ->
-		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
-    | [] ->
-	let t', s, trans = subst_evar_constr evs n mkVar concl in
-	  subst_vars acc 0 t', s, trans
-  in aux [] 0 (rev hyps)
-
-
-open Tacticals
-
-let trunc_named_context n ctx =
-  let len = List.length ctx in
-    list_firstn (len - n) ctx
-
-let rec chop_product n t =
-  if n = 0 then Some t
-  else
-    match kind_of_term t with
-      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
-      | _ -> None
-
-let evars_of_evar_info evi =
-  Intset.union (Evarutil.evars_of_term evi.evar_concl)
-    (Intset.union
-	(match evi.evar_body with
-	| Evar_empty -> Intset.empty
-	| Evar_defined b -> Evarutil.evars_of_term b)
-	(Evarutil.evars_of_named_context (evar_filtered_context evi)))
-
-let evar_dependencies evm oev =
-  let one_step deps =
-    Intset.fold (fun ev s ->
-      let evi = Evd.find evm ev in
-      let deps' = evars_of_evar_info evi in
-	if Intset.mem oev deps' then
-	  raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev))
-	else Intset.union deps' s)
-      deps deps
-  in
-  let rec aux deps =
-    let deps' = one_step deps in
-      if Intset.equal deps deps' then deps
-      else aux deps'
-  in aux (Intset.singleton oev)
-      
-let move_after (id, ev, deps as obl) l = 
-  let rec aux restdeps = function
-    | (id', _, _) as obl' :: tl -> 
-	let restdeps' = Intset.remove id' restdeps in
-	  if Intset.is_empty restdeps' then
-	    obl' :: obl :: tl
-	  else obl' :: aux restdeps' tl
-    | [] -> [obl]
-  in aux (Intset.remove id deps) l
-    
-let sort_dependencies evl =
-  let rec aux l found list =
-    match l with
-    | (id, ev, deps) as obl :: tl ->
-	let found' = Intset.union found (Intset.singleton id) in
-	  if Intset.subset deps found' then
-	    aux tl found' (obl :: list)
-	  else aux (move_after obl tl) found list
-    | [] -> List.rev list
-  in aux evl Intset.empty []
-
-let map_evar_body f = function
-  | Evar_empty -> Evar_empty
-  | Evar_defined c -> Evar_defined (f c)
-
-open Environ
-      
-let map_evar_info f evi =
-  { evi with evar_hyps = val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps));
-    evar_concl = f evi.evar_concl;
-    evar_body = map_evar_body f evi.evar_body }
-    
-let eterm_obligations env name isevars evm fs ?status t ty = 
-  (* 'Serialize' the evars *)
-  let nc = Environ.named_context env in
-  let nc_len = Sign.named_context_length nc in
-  let evl = List.rev (to_list evm) in
-  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
-  let sevl = sort_dependencies evl in
-  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
-  let evn =
-    let i = ref (-1) in
-      List.rev_map (fun (id, ev) -> incr i;
-		      (id, (!i, id_of_string
-			      (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
-		       ev)) evl
-  in
-  let evts =
-    (* Remove existential variables in types and build the corresponding products *)
-    fold_right
-      (fun (id, (n, nstr), ev) l ->
-	 let hyps = Evd.evar_filtered_context ev in
-	 let hyps = trunc_named_context nc_len hyps in
-	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
-	 let evtyp, hyps, chop =
-	   match chop_product fs evtyp with
-	   | Some t -> t, trunc_named_context fs hyps, fs
-	   | None -> evtyp, hyps, 0
-	 in
-	 let loc, k = evar_source id isevars in
-	 let status = match k with QuestionMark o -> Some o | _ -> status in
-	 let status, chop = match status with
-	   | Some (Define true as stat) ->
-	       if chop <> fs then Define false, None
-	       else stat, Some chop
-	   | Some s -> s, None
-	   | None -> Define true, None
-	 in
-	 let tac = match evar_tactic.get ev.evar_extra with
-	   | Some t ->
-	       if Dyn.tag t = "tactic" then
-		 Some (Tacinterp.interp 
-			  (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
-	       else None
-	   | None -> None
-	 in
-	 let info = { ev_name = (n, nstr);
-		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
-		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
-	 in (id, info) :: l)
-      evn []
-  in
-  let t', _, transparent = (* Substitute evar refs in the term by variables *)
-    subst_evar_constr evts 0 mkVar t 
-  in
-  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
-  let evars = 
-    List.map (fun (ev, info) ->
-      let { ev_name = (_, name); ev_status = status;
-	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
-      in
-      let status = match status with
-	| Define true when Idset.mem name transparent -> Define false
-	| _ -> status
-      in name, typ, src, status, deps, tac) evts
-  in
-  let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
-  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
-    Array.of_list (List.rev evars), (evnames, evmap), t', ty
-
-let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
deleted file mode 100644
index 4812fe0a6b..0000000000
--- a/plugins/subtac/eterm.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Environ
-open Tacmach
-open Term
-open Evd
-open Names
-open Pp
-open Util
-open Tacinterp
-
-val mkMetas : int -> constr list
-
-val evar_dependencies : evar_map -> int -> Intset.t
-val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
-
-(* env, id, evars, number of function prototypes to try to clear from
-   evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int ->
-  ?status:obligation_definition_status -> constr -> types -> 
-  (identifier * types * hole_kind located * obligation_definition_status * Intset.t * 
-      tactic option) array
-    (* Existential key, obl. name, type as product, location of the original evar, associated tactic,
-       status and dependencies as indexes into the array *)
-  * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * constr * types
-    (* Translations from existential identifiers to obligation identifiers 
-       and for terms with existentials to closed terms, given a 
-       translation from obligation identifiers to constrs, new term, new type *)
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
deleted file mode 100644
index 27de89f673..0000000000
--- a/plugins/subtac/g_subtac.ml4
+++ /dev/null
@@ -1,210 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(*
-  Syntax for the subtac terms and types.
-  Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-
-
-open Flags
-open Errors
-open Pp
-open Names
-open Nameops
-open Vernacentries
-open Reduction
-open Term
-open Libnames
-open Topconstr
-
-(* We define new entries for programs, with the use of this module
- * Subtac. These entries are named Subtac.<foo>
- *)
-
-module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
-module Tactic = Pcoq.Tactic
-
-module SubtacGram =
-struct
-  let gec s = Gram.entry_create ("Subtac."^s)
-		(* types *)
-  let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc"
-
-  let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac"
-end
-
-open Glob_term
-open SubtacGram
-open Util
-open Tok
-open Pcoq
-open Prim
-open Constr
-let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
-
-let enforce_locality arg =
-  let flag = !Vernacexpr.locality_flag in
-  match flag with
-  | None -> (* no locality flag set for now *)
-    Vernacexpr.locality_flag := arg
-  | Some _ -> (* a locality flag has been set, we cannot redefine it *)
-    begin match arg with
-    | None -> ()
-    | Some _ -> error "A locality flag has already been set."
-    end
-
-GEXTEND Gram
-  GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac;
-
-  (* FIXME : Program should be handled at a higher level in rule hierarchy. *)
-  subtac_locality:
-    [ [ IDENT "Local" -> enforce_locality (Some (loc, true))
-      | IDENT "Global" -> enforce_locality (Some (loc, false))
-      | -> enforce_locality None ] ]
-  ;
-
-  subtac_gallina_loc:
-    [ [ subtac_locality; g = Vernac.gallina -> loc, g
-    | subtac_locality; g = Vernac.gallina_ext -> loc, g ] ]
-    ;
-
-  subtac_withtac:
-    [ [ "with"; t = Tactic.tactic -> Some t
-      | -> None ] ]
-  ;
-
-  Constr.closed_binder:
-    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
-	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [LocalRawAssum ([id], default_binder_kind, typ)]
-    ] ];
-
-  END
-
-type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type
-
-let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
-  (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype),
-  (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
-  Genarg.create_arg "subtac_gallina_loc"
-
-type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
-
-let (wit_subtac_withtac : Genarg.tlevel withtac_argtype),
-  (globwit_subtac_withtac : Genarg.glevel withtac_argtype),
-  (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) =
-  Genarg.create_arg "subtac_withtac"
-
-VERNAC COMMAND EXTEND Subtac
-[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
-  END
-
-let try_catch_exn f e =
-  try f e
-  with exn -> errorlabstrm "Program" (Errors.print exn)
-
-let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
-let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
-let try_solve_obligation e = try_catch_exn Subtac_obligations.try_solve_obligation e
-let try_solve_obligations e = try_catch_exn Subtac_obligations.try_solve_obligations e
-let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligations e
-let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e
-
-VERNAC COMMAND EXTEND Subtac_Obligations
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) subtac_withtac(tac) ] -> 
-    [ subtac_obligation (num, Some name, Some t) tac ]
-| [ "Obligation" integer(num) "of" ident(name) subtac_withtac(tac) ] -> 
-    [ subtac_obligation (num, Some name, None) tac ]
-| [ "Obligation" integer(num) ":" lconstr(t) subtac_withtac(tac) ] -> 
-    [ subtac_obligation (num, None, Some t) tac ]
-| [ "Obligation" integer(num) subtac_withtac(tac) ] -> 
-    [ subtac_obligation (num, None, None) tac ]
-| [ "Next" "Obligation" "of" ident(name) subtac_withtac(tac) ] -> 
-    [ next_obligation (Some name) tac ]
-| [ "Next" "Obligation" subtac_withtac(tac) ] -> [ next_obligation None tac ]
-END
-
-VERNAC COMMAND EXTEND Subtac_Solve_Obligation
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] ->
-    [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] ->
-    [ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
-      END
-
-VERNAC COMMAND EXTEND Subtac_Solve_Obligations
-| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] ->
-    [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligations" "using" tactic(t) ] ->
-    [ try_solve_obligations None (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligations" ] ->
-    [ try_solve_obligations None None ]
-      END
-
-VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
-| [ "Solve" "All" "Obligations" "using" tactic(t) ] ->
-    [ solve_all_obligations (Some (Tacinterp.interp t)) ]
-| [ "Solve" "All" "Obligations" ] ->
-    [ solve_all_obligations None ]
-      END
-
-VERNAC COMMAND EXTEND Subtac_Admit_Obligations
-| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
-| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
-    END
-
-VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
-    Subtac_obligations.set_default_tactic 
-      (Vernacexpr.use_section_locality ())
-      (Tacinterp.glob_tactic t) ]
-END
-
-open Pp
-
-VERNAC COMMAND EXTEND Subtac_Show_Solver
-| [ "Show" "Obligation" "Tactic" ] -> [
-    msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ]
-END
-
-VERNAC COMMAND EXTEND Subtac_Show_Obligations
-| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
-| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
-END
-
-VERNAC COMMAND EXTEND Subtac_Show_Preterm
-| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ]
-| [ "Preterm" ] -> [ Subtac_obligations.show_term None ]
-END
-
-open Pp
-
-(* Declare a printer for the content of [Program] *)
-let () =
-  let printer _ _ _ expr = Ppvernac.pr_vernac_body (snd expr) in
-  (* should not happen *)
-  let dummy _ _ _ expr = assert false in
-  Pptactic.declare_extra_genarg_pprule
-    (rawwit_subtac_gallina_loc, printer)
-    (globwit_subtac_gallina_loc, dummy)
-    (wit_subtac_gallina_loc, dummy)
-
-(* Declare a printer for the content of Program tactics *)
-let () =
-  let printer _ _ _ = function
-  | None -> mt ()
-  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac
-  in
-  (* should not happen *)
-  let dummy _ _ _ expr = assert false in
-  Pptactic.declare_extra_genarg_pprule
-    (rawwit_subtac_withtac, printer)
-    (globwit_subtac_withtac, dummy)
-    (wit_subtac_withtac, dummy)
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
deleted file mode 100644
index ffcd40f94b..0000000000
--- a/plugins/subtac/subtac.ml
+++ /dev/null
@@ -1,229 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Compat
-open Global
-open Pp
-open Errors
-open Util
-open Names
-open Sign
-open Evd
-open Term
-open Termops
-open Namegen
-open Reductionops
-open Environ
-open Type_errors
-open Typeops
-open Libnames
-open Classops
-open List
-open Recordops
-open Evarutil
-open Pretype_errors
-open Glob_term
-open Evarconv
-open Pattern
-open Vernacexpr
-
-open Subtac_coercion
-open Subtac_utils
-open Coqlib
-open Printer
-open Subtac_errors
-open Eterm
-
-let require_library dirpath =
-  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
-    Library.require_library [qualid] None
-
-open Pp
-open Ppconstr
-open Decl_kinds
-open Tacinterp
-open Tacexpr
-
-let solve_tccs_in_type env id isevars evm c typ =
-  if not (Evd.is_empty evm) then
-    let stmt_id = Nameops.add_suffix id "_stmt" in
-    let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
-      match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
-      | Subtac_obligations.Defined cst -> constant_value (Global.env()) 
-	  (match cst with ConstRef kn -> kn | _ -> assert false)
-      | _ ->
-	  errorlabstrm "start_proof"
-	    (str "The statement obligations could not be resolved automatically, " ++ spc () ++
-		str "write a statement definition first.")
-  else
-    let _ = Typeops.infer_type env c in c
-
-
-let start_proof_com env isevars sopt kind (bl,t) hook =
-  let id = match sopt with
-    | Some (loc,id) ->
-        (* We check existence here: it's a bit late at Qed time *)
-        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
-          user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
-        id
-    | None ->
-	next_global_ident_away (id_of_string "Unnamed_thm")
- 	  (Pfedit.get_all_proof_names ())
-  in
-  let evm, c, typ, imps =
-    Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None
-  in
-  let c = solve_tccs_in_type env id isevars evm c typ in
-    Lemmas.start_proof id kind c (fun loc gr ->
-      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
-      hook loc gr)
-
-let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
-
-let start_proof_and_print env isevars idopt k t hook =
-  start_proof_com env isevars idopt k t hook;
-  print_subgoals ()
-
-let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
-
-let assumption_message id =
-  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
-
-let declare_assumptions env isevars idl is_coe k bl c nl =
-  if not (Pfedit.refining ()) then
-    let id = snd (List.hd idl) in
-    let evm, c, typ, imps =
-      Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
-    in
-    let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_assumption is_coe k c imps false nl) idl
-  else
-    errorlabstrm "Command.Assumption"
-	(str "Cannot declare an assumption while in proof editing mode.")
-
-let dump_constraint ty ((loc, n), _, _) =
-  match n with
-    | Name id -> Dumpglob.dump_definition (loc, id) false ty
-    | Anonymous -> ()
-
-let dump_variable lid = ()
-
-let vernac_assumption env isevars kind l nl =
-  let global = fst kind = Global in
-    List.iter (fun (is_coe,(idl,c)) ->
-      if Dumpglob.dump () then
-	List.iter (fun lid ->
-	  if global then Dumpglob.dump_definition lid (not global) "ax"
-	  else dump_variable lid) idl;
-      declare_assumptions env isevars idl is_coe kind [] c nl) l
-
-let check_fresh (loc,id) =
-  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
-    user_err_loc (loc,"",pr_id id ++ str " already exists")
-
-let subtac (loc, command) =
-  check_required_library ["Coq";"Init";"Datatypes"];
-  check_required_library ["Coq";"Init";"Specif"];
-  let env = Global.env () in
-  let isevars = ref (create_evar_defs Evd.empty) in
-  try
-  match command with
-  | VernacDefinition (defkind, (_, id as lid), expr, hook) ->
-      check_fresh lid;
-      Dumpglob.dump_definition lid false "def";
-      (match expr with
-      | ProveBody (bl, t) ->
-	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
-	    (fun _ _ -> ())
-      | DefineBody (bl, _, c, tycon) ->
-	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
-
-  | VernacFixpoint l ->
-      List.iter (fun ((lid, _, _, _, _), _) ->
-	check_fresh lid;
-	Dumpglob.dump_definition lid false "fix") l;
-      let _ = trace (str "Building fixpoint") in
-	ignore(Subtac_command.build_recursive l)
-
-  | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
-      if guard <> None then 
-        error "Do not support building theorems as a fixpoint.";
-      Dumpglob.dump_definition id false "prf";
-      if not(Pfedit.refining ()) then
-	if lettop then
-	  errorlabstrm "Subtac_command.StartProof"
-	    (str "Let declarations can only be used in proof editing mode");
-      if Lib.is_modtype () then
-	errorlabstrm "Subtac_command.StartProof"
-	  (str "Proof editing mode not supported in module types");
-      check_fresh id;
-      start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
-
-  | VernacAssumption (stre,nl,l) ->
-      vernac_assumption env isevars stre l nl
-
-  | VernacInstance (abst, glob, sup, is, props, pri) ->
-      dump_constraint "inst" is;
-      if abst then
-	error "Declare Instance not supported here.";
-      ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
-
-  | VernacCoFixpoint l ->
-      if Dumpglob.dump () then
-	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
-      ignore(Subtac_command.build_corecursive l)
-
-  | _ -> user_err_loc (loc,"", str ("Invalid Program command"))
-  with
-  | Typing_error e ->
-      msg_warning (str "Type error in Program tactic:");
-      let cmds =
-	(match e with
-	| NonFunctionalApp (loc, x, mux, e) ->
-	    str "non functional application of term " ++
-	      e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
-	| NonSigma (loc, t) ->
-	    str "Term is not of Sigma type: " ++ t
-	| NonConvertible (loc, x, y) ->
-	    str "Unconvertible terms:" ++ spc () ++
-	      x ++ spc () ++ str "and" ++ spc () ++ y
-	| IllSorted (loc, t) ->
-	    str "Term is ill-sorted:" ++ spc () ++ t
-	)
-      in msg_warning cmds
-
-  | Subtyping_error e ->
-      msg_warning (str "(Program tactic) Subtyping error:");
-      let cmds =
-	match e with
-	| UncoercibleInferType (loc, x, y) ->
-	    str "Uncoercible terms:" ++ spc ()
-	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
-	| UncoercibleInferTerm (loc, x, y, tx, ty) ->
-	    str "Uncoercible terms:" ++ spc ()
-	    ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
-	    ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
-	| UncoercibleRewrite (x, y) ->
-	    str "Uncoercible terms:" ++ spc ()
-	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
-      in msg_warning cmds
-
-  | Cases.PatternMatchingError (env, exn) as e -> raise e
-
-  | Type_errors.TypeError (env, exn) as e -> raise e
-
-  | Pretype_errors.PretypeError (env, _, exn) as e -> raise e
-
-  | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
-     Loc.Exc_located (loc, e') as e) -> raise e
-
-  | e -> 
-      (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
-      raise e
-
-let subtac c = Program.with_program subtac c
diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli
deleted file mode 100644
index 32d4840912..0000000000
--- a/plugins/subtac/subtac.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-val require_library : string -> unit
-val subtac : Pp.loc * Vernacexpr.vernac_expr -> unit
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
deleted file mode 100644
index 75d0f3429e..0000000000
--- a/plugins/subtac/subtac_classes.ml
+++ /dev/null
@@ -1,190 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pretyping
-open Evd
-open Environ
-open Term
-open Glob_term
-open Topconstr
-open Names
-open Libnames
-open Pp
-open Vernacexpr
-open Constrintern
-open Subtac_command
-open Typeclasses
-open Typeclasses_errors
-open Decl_kinds
-open Entries
-open Errors
-open Util
-
-let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c =
-  understand_tcc_evars evdref env kind
-    (intern_gen (kind=IsType) ~impls !evdref env c)
-
-let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ =
-  interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
-
-let interp_context_evars evdref env params =
-  let impls_env, bl = Constrintern.interp_context_gen
-    (fun env t -> understand_tcc_evars evdref env IsType t)
-    (understand_judgment_tcc evdref) !evdref env params in bl
-
-let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c =
-  let c = intern_gen true ~impls !evdref env c in
-  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
-    understand_tcc_evars ~fail_evar:false evdref env IsType c, imps
-
-let type_ctx_instance evars env ctx inst subst =
-  let rec aux (subst, instctx) l = function
-    (na, b, t) :: ctx ->
-      let t' = substl subst t in
-      let c', l =
-	match b with
-	| None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l
-	| Some b -> substl subst b, l
-      in
-       evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
-       let d = na, Some c', t' in
-	aux (c' :: subst, d :: instctx) l ctx
-    | [] -> subst
-  in aux (subst, []) inst (List.rev ctx)
-
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
-  let env = Global.env() in
-  let evars = ref Evd.empty in
-  let tclass, _ =
-    match bk with
-    | Implicit ->
-	Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *)
-	  ~allow_partial:false (fun avoid (clname, (id, _, t)) ->
-	    match clname with
-	    | Some (cl, b) ->
-		let t =
-		  if b then
-		    let _k = class_info cl in
-		      CHole (Pp.dummy_loc, Some Evd.InternalHole)
-		  else CHole (Pp.dummy_loc, None)
-		in t, avoid
-	    | None -> failwith ("new instance: under-applied typeclass"))
-	  cl
-      | Explicit -> cl, Idset.empty
-  in
-  let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
-  let k, cty, ctx', ctx, len, imps, subst =
-    let (env', ctx), imps = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
-    let len = List.length ctx in
-    let imps = imps @ Impargs.lift_implicits len imps' in
-    let ctx', c = decompose_prod_assum c' in
-    let ctx'' = ctx' @ ctx in
-    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
-    let _, args = 
-      List.fold_right (fun (na, b, t) (args, args') ->
-	match b with
-	| None -> (List.tl args, List.hd args :: args')
-	| Some b -> (args, substl args' b :: args'))
-	(snd cl.cl_context) (args, [])
-    in
-      cl, c', ctx', ctx, len, imps, args
-  in
-  let id =
-    match snd instid with
-    | Name id ->
-	let sp = Lib.make_path id in
-	  if Nametab.exists_cci sp then
-	    errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
-	  id
-    | Anonymous ->
-	let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
-	  Namegen.next_global_ident_away i (Termops.ids_of_context env)
-  in
-  evars := Typeclasses.mark_resolvables (Evarutil.nf_evar_map !evars);
-  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
-  let ctx = Evarutil.nf_rel_context_evar !evars ctx 
-  and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in
-  let env' = push_rel_context ctx env in
-  let sigma =  !evars in
-  let subst = List.map (Evarutil.nf_evar sigma) subst in
-  let props =
-    match props with
-    | Some (CRecord (loc, _, fs)) ->
-	if List.length fs > List.length k.cl_props then
-	  Classes.mismatched_props env' (List.map snd fs) k.cl_props;
-	Inl fs
-    | Some p -> Inr p
-    | None -> Inl []
-  in
-  let subst =
-    match props with
-    | Inr term ->
-	let c = interp_casted_constr_evars evars env' term cty in
-	  Inr c
-    | Inl props ->
-	let get_id =
-	  function
-	    | Ident id' -> id'
-	    | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled")
-	in
-	let props, rest =
-	  List.fold_left
-	    (fun (props, rest) (id,b,_) ->
-	      if b = None then
-		try
-		  let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
-		  let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
-		  let (loc, mid) = get_id loc_mid in
-		    List.iter 
-		      (fun (n, _, x) -> 
-			 if n = Name mid then
-			   Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
-		      k.cl_projs;
-		    c :: props, rest'
-		with Not_found ->
-		  (CHole (Pp.dummy_loc, None) :: props), rest
-	      else props, rest)
-	    ([], props) k.cl_props
-	in
-	  if rest <> [] then
-	    unbound_method env' k.cl_impl (get_id (fst (List.hd rest)))
-	  else
-	    Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
-  in	  
-  evars := Evarutil.nf_evar_map !evars;
-  evars := Typeclasses.mark_resolvables !evars;
-  evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
-  let term, termtype =
-    match subst with
-    | Inl subst ->
-	let subst = List.fold_left2
-	  (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
-	  [] subst (k.cl_props @ snd k.cl_context)
-	in
-	let app, ty_constr = instance_constructor k subst in
-	let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
-	  term, termtype
-    | Inr def ->
-	let termtype = it_mkProd_or_LetIn cty ctx in
-	let term = Termops.it_mkLambda_or_LetIn def ctx in
-	  term, termtype
-  in
-  let termtype = Evarutil.nf_evar !evars termtype in
-  let term = Evarutil.nf_evar !evars term in
-  evars := undefined_evars !evars;
-  Evarutil.check_evars env Evd.empty !evars termtype;
-  let hook vis gr =
-    let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-      Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-      Typeclasses.declare_instance pri (not global) (ConstRef cst)
-  in
-  let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
-  let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
-    id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
deleted file mode 100644
index 5b8636a126..0000000000
--- a/plugins/subtac/subtac_classes.mli
+++ /dev/null
@@ -1,40 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i*)
-open Names
-open Decl_kinds
-open Term
-open Sign
-open Evd
-open Environ
-open Nametab
-open Mod_subst
-open Topconstr
-open Errors
-open Util
-open Typeclasses
-open Implicit_quantifiers
-open Classes
-(*i*)
-
-val type_ctx_instance :     Evd.evar_map ref ->
-  Environ.env ->
-    ('a * Term.constr option * Term.constr) list ->
-    Topconstr.constr_expr list ->
-    Term.constr list ->
-    Term.constr list
-
-val new_instance :
-  ?global:bool ->
-  local_binder list ->
-  typeclass_constraint ->
-  constr_expr option ->
-  ?generalize:bool ->
-  int option ->
-  identifier * Subtac_obligations.progress
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
deleted file mode 100644
index 33560995db..0000000000
--- a/plugins/subtac/subtac_command.ml
+++ /dev/null
@@ -1,474 +0,0 @@
-open Closure
-open RedFlags
-open Declarations
-open Entries
-open Libobject
-open Pattern
-open Matching
-open Pp
-open Glob_term
-open Sign
-open Tacred
-open Errors
-open Util
-open Names
-open Nameops
-open Libnames
-open Nametab
-open Pfedit
-open Proof_type
-open Refiner
-open Tacmach
-open Tactic_debug
-open Topconstr
-open Term
-open Tacexpr
-open Safe_typing
-open Typing
-open Hiddentac
-open Genarg
-open Decl_kinds
-open Mod_subst
-open Printer
-open Inductiveops
-open Syntax_def
-open Environ
-open Tactics
-open Tacticals
-open Tacinterp
-open Vernacexpr
-open Notation
-open Evd
-open Evarutil
-
-open Subtac_utils
-open Pretyping
-open Subtac_obligations
-
-(*********************************************************************)
-(* Functions to parse and interpret constructions *)
-
-let evar_nf isevars c =
-  Evarutil.nf_evar !isevars c
-
-let interp_gen kind isevars env
-               ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
-               c =
-  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
-  let c' = understand_tcc_evars isevars env kind c' in
-    evar_nf isevars c'
-
-let interp_constr isevars env c =
-  interp_gen (OfType None) isevars env c
-
-let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c =
-  interp_gen IsType isevars env ~impls c
-
-let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
-  interp_gen (OfType (Some typ)) isevars env ~impls c
-
-let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
-  interp_gen (OfType (Some typ)) isevars env ~impls c
-
-let interp_open_constr isevars env c =
-    msgnl (str "Pretyping " ++ my_print_constr_expr c);
-  let c = Constrintern.intern_constr ( !isevars) env c in
-  let c' = understand_tcc_evars isevars env (OfType None) c in
-    evar_nf isevars c'
-
-let interp_constr_judgment isevars env c =
-  let j =
-    understand_judgment_tcc isevars env
-      (Constrintern.intern_constr ( !isevars) env c)
-  in
-    { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
-
-let locate_if_isevar loc na = function
-  | GHole _ ->
-      (try match na with
-	| Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
-	| Anonymous -> raise Not_found
-      with Not_found -> GHole (loc, Evd.BinderType na))
-  | x -> x
-
-let interp_binder sigma env na t =
-  let t = Constrintern.intern_gen true ( !sigma) env t in
-    understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
-
-let interp_context_evars evdref env params =
-  let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in
-  let (env, par, _, impls) =
-    List.fold_left
-      (fun (env,params,n,impls) (na, k, b, t) ->
-	match b with
-	    None ->
-	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-	      let t = understand_tcc_evars evdref env IsType t' in
-	      let d = (na,None,t) in
-	      let impls =
-		if k = Implicit then
-		  let na = match na with Name n -> Some n | Anonymous -> None in
-		    (ExplByPos (n, na), (true, true, true)) :: impls
-		else impls
-	      in
-		(push_rel d env, d::params, succ n, impls)
-	  | Some b ->
-	      let c = understand_judgment_tcc evdref env b in
-	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env,d::params, succ n, impls))
-      (env,[],1,[]) (List.rev bl)
-  in (env, par), impls
-
-
-open Coqlib
-
-let sigT = Lazy.lazy_from_fun build_sigma_type
-
-let rec telescope = function
-  | [] -> assert false
-  | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
-  | (n, None, t) :: tl ->
-      let ty, tys, (k, constr) =
-	List.fold_left
-	  (fun (ty, tys, (k, constr)) (n, b, t) ->
-	    let pred = mkLambda (n, t, ty) in
-	    let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
-	    let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
-	      (sigty, pred :: tys, (succ k, intro)))
-	  (t, [], (2, mkRel 1)) tl
-      in
-      let (last, subst) = List.fold_right2
-	(fun pred (n, b, t) (prev, subst) ->
-	  let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
-	  let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
-	    (lift 1 proj2, (n, Some proj1, t) :: subst))
-	(List.rev tys) tl (mkRel 1, [])
-      in ty, ((n, Some last, t) :: subst), constr
-
-  | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
-      ty, ((n, Some b, t) :: subst), lift 1 term
-
-let nf_evar_context isevars ctx =
-  List.map (fun (n, b, t) ->
-    (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
-
-let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
-  Coqlib.check_required_library ["Coq";"Program";"Wf"];
-  let sigma = Evd.empty in
-  let isevars = ref (Evd.create_evar_defs sigma) in
-  let env = Global.env() in
-  let _pr c = my_print_constr env c in
-  let _prr = Printer.pr_rel_context env in
-  let _prn = Printer.pr_named_context env in
-  let _pr_rel env = Printer.pr_rel_context env in
-  let (env', binders_rel), impls = interp_context_evars isevars env bl in
-  let len = List.length binders_rel in
-  let top_env = push_rel_context binders_rel env in
-  let top_arity = interp_type_evars isevars top_env arityc in
-  let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
-  let argtyp, letbinders, make = telescope binders_rel in
-  let argname = id_of_string "recarg" in
-  let arg = (Name argname, None, argtyp) in
-  let binders = letbinders @ [arg] in
-  let binders_env = push_rel_context binders_rel env in
-  let rel = interp_constr isevars env r in
-  let relty = type_of env !isevars rel in
-  let relargty =
-    let error () =
-      user_err_loc (constr_loc r,
-		   "Subtac_command.build_wellfounded",
-		   my_print_constr env rel ++ str " is not an homogeneous binary relation.")
-    in
-      try
-	let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
-	  match ctx, kind_of_term ar with
-	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
-	      when Reductionops.is_conv env !isevars t u -> t
-	  | _, _ -> error ()
-      with _ -> error ()
-  in
-  let measure = interp_casted_constr isevars binders_env measure relargty in
-  let wf_rel, wf_rel_fun, measure_fn =
-    let measure_body, measure =
-      it_mkLambda_or_LetIn measure letbinders,
-      it_mkLambda_or_LetIn measure binders
-    in
-    let comb = constr_of_global (delayed_force measure_on_R_ref) in
-    let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
-    let wf_rel_fun x y =
-      mkApp (rel, [| subst1 x measure_body;
- 		     subst1 y measure_body |])
-    in wf_rel, wf_rel_fun, measure
-  in
-  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
-  let argid' = id_of_string (string_of_id argname ^ "'") in
-  let wfarg len = (Name argid', None,
-  		  mkSubset (Name argid') argtyp
-		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
-  in
-  let intern_bl = wfarg 1 :: [arg] in
-  let _intern_env = push_rel_context intern_bl env in
-  let proj = (delayed_force sig_).Coqlib.proj1 in
-  let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
-  let projection = (* in wfarg :: arg :: before *)
-    mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
-  in
-  let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
-  let intern_arity = substl [projection] top_arity_let in
-  (* substitute the projection of wfarg for something,
-     now intern_arity is in wfarg :: arg *)
-  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
-  let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
-  let curry_fun =
-    let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
-    let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
-    let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
-    let rcurry = mkApp (rel, [| measure; lift len measure |]) in
-    let lam = (Name (id_of_string "recproof"), None, rcurry) in
-    let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
-    let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
-      (Name recname, Some body, ty)
-  in
-  let fun_bl = intern_fun_binder :: [arg] in
-  let lift_lets = Termops.lift_rel_context 1 letbinders in
-  let intern_body =
-    let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
-    let (r, l, impls, scopes) =
-      Constrintern.compute_internalization_data env
-	Constrintern.Recursive full_arity impls 
-    in
-    let newimpls = Idmap.singleton recname
-      (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))],
-       scopes @ [None]) in
-      interp_casted_constr isevars ~impls:newimpls
-	(push_rel_context ctx env) body (lift 1 top_arity)
-  in
-  let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
-  let prop = mkLambda (Name argname, argtyp, top_arity_let) in
-  let def =
-    mkApp (constr_of_global (delayed_force fix_sub_ref),
-	  [| argtyp ; wf_rel ;
-	     make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
-	     prop ; intern_body_lam |])
-  in
-  let _ = isevars := Evarutil.nf_evar_map !isevars in
-  let binders_rel = nf_evar_context !isevars binders_rel in
-  let binders = nf_evar_context !isevars binders in
-  let top_arity = Evarutil.nf_evar !isevars top_arity in
-  let hook, recname, typ = 
-    if List.length binders_rel > 1 then
-      let name = add_suffix recname "_func" in
-      let hook l gr = 
-	let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
-	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let ce =
-          { const_entry_body = Evarutil.nf_evar !isevars body;
-            const_entry_secctx = None;
-	    const_entry_type = Some ty;
-	    const_entry_opaque = false }
-	in 
-	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
-	let gr = ConstRef c in
-	  if Impargs.is_implicit_args () || impls <> [] then
-	    Impargs.declare_manual_implicits false gr [impls]
-      in
-      let typ = it_mkProd_or_LetIn top_arity binders in
-	hook, name, typ
-    else 
-      let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook l gr = 
-	if Impargs.is_implicit_args () || impls <> [] then
-	  Impargs.declare_manual_implicits false gr [impls]
-      in hook, recname, typ
-  in
-  let fullcoqc = Evarutil.nf_evar !isevars def in
-  let fullctyp = Evarutil.nf_evar !isevars typ in
-  let evm = evars_of_term !isevars Evd.empty fullctyp in
-  let evm = evars_of_term !isevars evm fullcoqc in
-  let evm = non_instanciated_map env isevars evm in
-  let evars, _, evars_def, evars_typ = 
-    Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp 
-  in
-    Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook
-
-let interp_fix_context evdref env fix =
-  interp_context_evars evdref env fix.Command.fix_binders
-
-let interp_fix_ccl evdref (env,_) fix =
-  interp_type_evars evdref env fix.Command.fix_type
-
-let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
-  let env = push_rel_context ctx env_rec in
-  let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in
-  Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body
-
-let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
-
-let prepare_recursive_declaration fixnames fixtypes fixdefs =
-  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
-  let names = List.map (fun id -> Name id) fixnames in
-  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
-
-let rel_index n ctx =
-  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
-
-let rec unfold f b =
-  match f b with
-    | Some (x, b') -> x :: unfold f b'
-    | None -> []
-
-let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
-  match n with
-  | Some (loc, n) -> [rel_index n fixctx]
-  | None ->
-      (* If recursive argument was not given by user, we try all args.
-	 An earlier approach was to look only for inductive arguments,
-	 but doing it properly involves delta-reduction, and it finally
-         doesn't seem to worth the effort (except for huge mutual
-	 fixpoints ?) *)
-      let len = List.length fixctx in
-	unfold (function x when x = len -> None
-	  | n -> Some (n, succ n)) 0
-
-let push_named_context = List.fold_right push_named
-
-let check_evars env initial_sigma evd c =
-  let sigma =  evd in
-  let c = nf_evar sigma c in
-  let rec proc_rec c =
-    match kind_of_term c with
-      | Evar (evk,args) ->
-          assert (Evd.mem sigma evk);
-	  if not (Evd.mem initial_sigma evk) then
-            let (loc,k) = evar_source evk evd in
-	      (match k with
-	      | QuestionMark _
-	      | ImplicitArg (_, _, false) -> ()
-	      | _ ->
-		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
-		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
-      | _ -> iter_constr proc_rec c
-  in proc_rec c
-
-let out_def = function
-  | Some def -> def
-  | None -> error "Program Fixpoint needs defined bodies."
-
-let interp_recursive fixkind l =
-  let env = Global.env() in
-  let fixl, ntnl = List.split l in
-  let kind = fixkind <> IsCoFixpoint in
-  let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
-
-  (* Interp arities allowing for unresolved types *)
-  let evdref = ref Evd.empty in
-  let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
-  let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
-  let fixtypes = List.map2 build_fix_type fixctxs fixccls in
-  let rec_sign =
-    List.fold_left2 (fun env' id t ->
-      let sort = Retyping.get_type_of env !evdref t in
-      let fixprot =
-	try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
-	with e -> t
-      in
-	(id,None,fixprot) :: env')
-      [] fixnames fixtypes
-  in
-  let env_rec = push_named_context rec_sign env in
-
-  (* Get interpretation metadatas *)
-  let impls = Constrintern.compute_internalization_env env
-    Constrintern.Recursive fixnames fixtypes fiximps
-  in
-  let notations = List.flatten ntnl in
-
-  (* Interp bodies with rollback because temp use of notations/implicit *)
-  let fixdefs =
-    States.with_state_protection (fun () ->
-      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
-      list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
-      () in
-
-  let fixdefs = List.map out_def fixdefs in
-
-  (* Instantiate evars and check all are resolved *)
-  let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
-  let evd = Typeclasses.resolve_typeclasses
-    ~onlyargs:true ~split:true ~fail:false env_rec evd
-  in
-  let evd = Evarutil.nf_evar_map evd in
-  let fixdefs = List.map (nf_evar evd) fixdefs in
-  let fixtypes = List.map (nf_evar evd) fixtypes in
-  let rec_sign = nf_named_context_evar evd rec_sign in
-
-  let recdefs = List.length rec_sign in
-  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
-  List.iter (check_evars env Evd.empty evd) fixtypes;
-  Command.check_mutuality env kind (List.combine fixnames fixdefs);
-
-  (* Russell-specific code *)
-
-  (* Get the interesting evars, those that were not instanciated *)
-  let isevars = Evd.undefined_evars evd in
-  let evm =  isevars in
-  (* Solve remaining evars *)
-  let rec collect_evars id def typ imps =
-      (* Generalize by the recursive prototypes  *)
-    let def =
-      Termops.it_mkNamedLambda_or_LetIn def rec_sign
-    and typ =
-      Termops.it_mkNamedProd_or_LetIn typ rec_sign
-    in
-    let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
-    let evm' = Subtac_utils.evars_of_term evm evm' typ in
-    let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
-      (id, def, typ, imps, evars)
-  in
-  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
-    (match fixkind with
-      | IsFixpoint wfl ->
-	  let possible_indexes =
-	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
-	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
-	    Array.of_list fixtypes,
-	    Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
-	  in
-	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
-	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
-      | IsCoFixpoint -> ());
-    Subtac_obligations.add_mutual_definitions defs notations fixkind
-
-let out_n = function
-    Some n -> n
-  | None -> raise Not_found
-
-let build_recursive l =
-  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
-    match g, l with
-	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
-	  ignore(build_wellfounded (id, n, bl, typ, out_def def) r
-		    (match n with Some n -> mkIdentC (snd n) | None ->
-		      errorlabstrm "Subtac_command.build_recursive"
-			(str "Recursive argument required for well-founded fixpoints"))
-		    ntn)
-
-      | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
-	  ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
-		    m ntn)
-
-      | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
-	  let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
-	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
-	      Command.fix_body = def; Command.fix_type = typ},ntn)) l
-	  in interp_recursive (IsFixpoint g) fixl
-      | _, _ ->
-	  errorlabstrm "Subtac_command.build_recursive"
-	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
-
-let build_corecursive l =
-  let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
-    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
-      Command.fix_body = def; Command.fix_type = typ},ntn))
-    l in
-  interp_recursive IsCoFixpoint fixl
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
deleted file mode 100644
index 72549a011e..0000000000
--- a/plugins/subtac/subtac_command.mli
+++ /dev/null
@@ -1,60 +0,0 @@
-open Pretyping
-open Evd
-open Environ
-open Term
-open Topconstr
-open Names
-open Libnames
-open Pp
-open Vernacexpr
-open Constrintern
-
-val interp_gen :
-  typing_constraint ->
-  evar_map ref ->
-  env ->
-  ?impls:internalization_env ->
-  ?allow_patvar:bool ->
-  ?ltacvars:ltac_sign ->
-  constr_expr -> constr
-val interp_constr :
-  evar_map ref ->
-  env -> constr_expr -> constr
-val interp_type_evars :
-  evar_map ref ->
-  env ->
-  ?impls:internalization_env ->
-  constr_expr -> constr
-val interp_casted_constr_evars :
-  evar_map ref ->
-  env ->
-  ?impls:internalization_env ->
-  constr_expr -> types -> constr
-val interp_open_constr :
-  evar_map ref -> env -> constr_expr -> constr
-val interp_constr_judgment :
-  evar_map ref ->
-  env ->
-  constr_expr -> unsafe_judgment
-val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
-
-val interp_binder :     Evd.evar_map ref ->
-    Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
-
-
-val telescope :
-  (Names.name * Term.types option * Term.types) list ->
-  Term.types * (Names.name * Term.types option * Term.types) list *
-    Term.constr
-
-val build_wellfounded :
-           Names.identifier * 'a * Topconstr.local_binder list *
-           Topconstr.constr_expr * Topconstr.constr_expr ->
-           Topconstr.constr_expr ->
-           Topconstr.constr_expr -> 'b -> Subtac_obligations.progress
-
-val build_recursive :
-  (fixpoint_expr * decl_notation list) list -> unit
-
-val build_corecursive :
-  (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml
deleted file mode 100644
index f07bbeb436..0000000000
--- a/plugins/subtac/subtac_errors.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-open Errors
-open Util
-open Pp
-open Printer
-
-type term_pp = Pp.std_ppcmds
-
-type subtyping_error =
-  | UncoercibleInferType of loc * term_pp * term_pp
-  | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp
-  | UncoercibleRewrite of term_pp * term_pp
-
-type typing_error =
-  | NonFunctionalApp of loc * term_pp * term_pp * term_pp
-  | NonConvertible of loc * term_pp * term_pp
-  | NonSigma of loc * term_pp
-  | IllSorted of loc * term_pp
-
-exception Subtyping_error of subtyping_error
-exception Typing_error of typing_error
-
-exception Debug_msg of string
-
-let typing_error e = raise (Typing_error e)
-let subtyping_error e = raise (Subtyping_error e)
diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli
deleted file mode 100644
index c65203075a..0000000000
--- a/plugins/subtac/subtac_errors.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-type term_pp = Pp.std_ppcmds
-type subtyping_error =
-    UncoercibleInferType of Pp.loc * term_pp * term_pp
-  | UncoercibleInferTerm of Pp.loc * term_pp * term_pp * term_pp * term_pp
-  | UncoercibleRewrite of term_pp * term_pp
-type typing_error =
-    NonFunctionalApp of Pp.loc * term_pp * term_pp * term_pp
-  | NonConvertible of Pp.loc * term_pp * term_pp
-  | NonSigma of Pp.loc * term_pp
-  | IllSorted of Pp.loc * term_pp
-exception Subtyping_error of subtyping_error
-exception Typing_error of typing_error
-exception Debug_msg of string
-val typing_error : typing_error -> 'a
-val subtyping_error : subtyping_error -> 'a
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
deleted file mode 100644
index 527c5e0847..0000000000
--- a/plugins/subtac/subtac_obligations.ml
+++ /dev/null
@@ -1,694 +0,0 @@
-open Printf
-open Pp
-open Subtac_utils
-open Command
-open Environ
-
-open Term
-open Names
-open Libnames
-open Summary
-open Libobject
-open Entries
-open Decl_kinds
-open Errors
-open Util
-open Evd
-open Declare
-open Proof_type
-open Compat
-
-let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
-let pperror cmd = Errors.errorlabstrm "Program" cmd
-let error s = pperror (str s)
-
-let reduce c =
-  Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c
-
-exception NoObligations of identifier option
-
-let explain_no_obligations = function
-    Some ident -> str "No obligations for program " ++ str (string_of_id ident)
-  | None -> str "No obligations remaining"
-
-type obligation_info = (Names.identifier * Term.types * hole_kind located *
-			  obligation_definition_status * Intset.t * tactic option) array
-
-type obligation =
-  { obl_name : identifier;
-    obl_type : types;
-    obl_location : hole_kind located;
-    obl_body : constr option;
-    obl_status : obligation_definition_status;
-    obl_deps : Intset.t;
-    obl_tac : tactic option;
-  }
-
-type obligations = (obligation array * int)
-
-type fixpoint_kind =
-  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
-  | IsCoFixpoint
-
-type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
-
-type program_info = {
-  prg_name: identifier;
-  prg_body: constr;
-  prg_type: constr;
-  prg_obligations: obligations;
-  prg_deps : identifier list;
-  prg_fixkind : fixpoint_kind option ;
-  prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
-  prg_notations : notations ;
-  prg_kind : definition_kind;
-  prg_reduce : constr -> constr;
-  prg_hook : Tacexpr.declaration_hook;
-}
-
-let assumption_message id =
-  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
-
-let (set_default_tactic, get_default_tactic, print_default_tactic) = 
-  Tactic_option.declare_tactic_option "Program tactic"
-
-(* true = All transparent, false = Opaque if possible *)
-let proofs_transparency = ref true
-
-let set_proofs_transparency = (:=) proofs_transparency
-let get_proofs_transparency () = !proofs_transparency
-
-open Goptions
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "transparency of Program obligations";
-      optkey   = ["Transparent";"Obligations"];
-      optread  = get_proofs_transparency;
-      optwrite = set_proofs_transparency; }
-
-(* true = hide obligations *)
-let hide_obligations = ref false
-
-let set_hide_obligations = (:=) hide_obligations
-let get_hide_obligations () = !hide_obligations
-
-open Goptions
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "Hidding of Program obligations";
-      optkey   = ["Hide";"Obligations"];
-      optread  = get_hide_obligations;
-      optwrite = set_hide_obligations; }
-
-let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-
-let get_obligation_body expand obl =
-  let c = Option.get obl.obl_body in
-    if expand && obl.obl_status = Expand then
-      match kind_of_term c with
-      | Const c -> constant_value (Global.env ()) c
-      | _ -> c
-    else c
-
-let obl_substitution expand obls deps =
-  Intset.fold
-    (fun x acc ->
-       let xobl = obls.(x) in
-       let oblb =
-	 try get_obligation_body expand xobl
-	 with _ -> assert(false)
-       in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
-    deps []
-
-let subst_deps expand obls deps t =
-  let subst = obl_substitution expand obls deps in
-    Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
-
-let rec prod_app t n =
-  match kind_of_term (strip_outer_cast t) with
-    | Prod (_,_,b) -> subst1 n b
-    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
-    | _ ->
-	errorlabstrm "prod_app"
-	  (str"Needed a product, but didn't find one" ++ fnl ())
-
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
-  let rec aux c = 
-    let f, l = decompose_app c in
-      if isVar f then
-	try
-	  let c' = List.map (map_constr aux) l in
-	  let (t, b) = List.assoc (destVar f) subst in
-	    mkApp (delayed_force hide_obligation, 
-		   [| prod_applist t c'; applistc b c' |])
-	with Not_found -> map_constr aux c
-      else map_constr aux c
-  in map_constr aux
-       
-let subst_prog expand obls ints prg =
-  let subst = obl_substitution expand obls ints in
-    if get_hide_obligations () then
-      (replace_appvars subst prg.prg_body,
-       replace_appvars subst (Termops.refresh_universes prg.prg_type))
-    else 
-      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
-	(Term.replace_vars subst' prg.prg_body,
-	 Term.replace_vars subst' (Termops.refresh_universes prg.prg_type))
-
-let subst_deps_obl obls obl =
-  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
-    { obl with obl_type = t' }
-
-module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
-
-let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
-
-let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-
-let map_cardinal m =
-  let i = ref 0 in
-    ProgMap.iter (fun _ _ -> incr i) m;
-    !i
-
-exception Found of program_info
-
-let map_first m =
-  try
-    ProgMap.iter (fun _ v -> raise (Found v)) m;
-    assert(false)
-  with Found x -> x
-
-let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
-
-let freeze () = !from_prg
-let unfreeze v = from_prg := v
-let init () = from_prg := ProgMap.empty
-
-(** Beware: if this code is dynamically loaded via dynlink after the start
-    of Coq, then this [init] function will not be run by [Lib.init ()].
-    Luckily, here we can launch [init] at load-time. *)
-
-let _ = init ()
-
-let _ =
-  Summary.declare_summary "program-tcc-table"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
-
-let progmap_union = ProgMap.fold ProgMap.add
-
-let close sec =
-  if not (ProgMap.is_empty !from_prg) then
-    let keys = map_keys !from_prg in
-      errorlabstrm "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
-			      prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
-			      (str (if List.length keys = 1 then " has " else "have ") ++
-			       str "unsolved obligations"))
-
-let input : program_info ProgMap.t -> obj =
-  declare_object
-    { (default_object "Program state") with
-      cache_function = (fun (na, pi) -> from_prg := pi);
-      load_function = (fun _ (_, pi) -> from_prg := pi);
-      discharge_function = (fun _ -> close "section"; None);
-      classify_function = (fun _ -> close "module"; Dispose) }
-    
-open Evd
-
-let progmap_remove prg =
-  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
-  
-let progmap_add n prg =
-  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
-
-let progmap_replace prg' = 
-  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
-
-let rec intset_to = function
-    -1 -> Intset.empty
-  | n -> Intset.add n (intset_to (pred n))
-
-let subst_body expand prg =
-  let obls, _ = prg.prg_obligations in
-  let ints = intset_to (pred (Array.length obls)) in
-    subst_prog expand obls ints prg
-
-let declare_definition prg =
-  let body, typ = subst_body true prg in
-  let (local, kind) = prg.prg_kind in
-  let ce =
-    { const_entry_body = body;
-      const_entry_secctx = None;
-      const_entry_type = Some typ;
-      const_entry_opaque = false }
-  in
-    (Command.get_declare_definition_hook ()) ce;
-    match local with
-    | Local when Lib.sections_are_opened () ->
-        let c =
-          SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
-        let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in
-          print_message (Subtac_utils.definition_message prg.prg_name);
-          if Pfedit.refining () then
-            Flags.if_verbose msg_warning
-	      (str"Local definition " ++ Nameops.pr_id prg.prg_name ++
-		  str" is not visible from current goals");
-	  progmap_remove prg; 
-          VarRef prg.prg_name
-    | (Global|Local) ->
-	let c =
-	  Declare.declare_constant
-	    prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind))
-	in
-	let gr = ConstRef c in
-	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
-	    Impargs.declare_manual_implicits false gr [prg.prg_implicits];
-	  print_message (Subtac_utils.definition_message prg.prg_name);
-	  progmap_remove prg; 
-	  prg.prg_hook local gr;
-	  gr
-
-open Pp
-open Ppconstr
-
-let rec lam_index n t acc =
-  match kind_of_term t with
-    | Lambda (na, _, b) ->
-	if na = Name n then acc
-	else lam_index n b (succ acc)
-    | _ -> raise Not_found
-
-let compute_possible_guardness_evidences (n,_) fixbody fixtype =
-  match n with
-  | Some (loc, n) -> [lam_index n fixbody 0]
-  | None ->
-      (* If recursive argument was not given by user, we try all args.
-	 An earlier approach was to look only for inductive arguments,
-	 but doing it properly involves delta-reduction, and it finally
-         doesn't seem to worth the effort (except for huge mutual
-	 fixpoints ?) *)
-      let m = Term.nb_prod fixtype in
-      let ctx = fst (decompose_prod_n_assum m fixtype) in
-	list_map_i (fun i _ -> i) 0 ctx
-
-let declare_mutual_definition l =
-  let len = List.length l in
-  let first = List.hd l in
-  let fixdefs, fixtypes, fiximps =
-    list_split3
-      (List.map (fun x -> 
-	let subs, typ = (subst_body true x) in
-	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
-	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
-	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
-  in
-(*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixkind = Option.get first.prg_fixkind in
-  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
-  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let (local,kind) = first.prg_kind in
-  let fixnames = first.prg_deps in
-  let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
-  let indexes, fixdecls =
-    match fixkind with
-      | IsFixpoint wfl ->
-	  let possible_indexes =
-	    list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
-	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
-	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
-      | IsCoFixpoint ->
-	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
-  in
-  (* Declare the recursive definitions *)
-  let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in
-    (* Declare notations *)
-    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
-    Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
-    let gr = List.hd kns in
-    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      first.prg_hook local gr;
-      List.iter progmap_remove l; kn
-      
-let declare_obligation prg obl body =
-  let body = prg.prg_reduce body in
-  let ty = prg.prg_reduce obl.obl_type in
-  match obl.obl_status with
-  | Expand -> { obl with obl_body = Some body }
-  | Define opaque ->
-      let opaque = if get_proofs_transparency () then false else opaque in
-      let ce = 
-	{ const_entry_body = body;
-          const_entry_secctx = None;
-	  const_entry_type = Some ty;
-	  const_entry_opaque = opaque }
-      in
-      let constant = Declare.declare_constant obl.obl_name
-	(DefinitionEntry ce,IsProof Property)
-      in
-	if not opaque then
-	  Auto.add_hints false [string_of_id prg.prg_name]
-	    (Auto.HintsUnfoldEntry [EvalConstRef constant]);
-	print_message (Subtac_utils.definition_message obl.obl_name);
-	{ obl with obl_body = Some (mkConst constant) }
-
-let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
-  let obls', b = 
-    match b with
-    | None ->
-	assert(obls = [||]);
-	let n = Nameops.add_suffix n "_obligation" in
-	  [| { obl_name = n; obl_body = None;
-	       obl_location = dummy_loc, InternalHole; obl_type = t;
-	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
-	mkVar n
-    | Some b ->
-	Array.mapi
-	  (fun i (n, t, l, o, d, tac) ->
-            { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = reduce t; obl_status = o;
-	      obl_deps = d; obl_tac = tac })
-	  obls, b
-  in
-    { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls');
-      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
-      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; }
-
-let get_prog name =
-  let prg_infos = !from_prg in
-    match name with
-	Some n ->
-	  (try ProgMap.find n prg_infos
-	   with Not_found -> raise (NoObligations (Some n)))
-      | None ->
-	  (let n = map_cardinal prg_infos in
-	     match n with
-		 0 -> raise (NoObligations None)
-	       | 1 -> map_first prg_infos
-	       | _ -> error "More than one program with unsolved obligations")
-
-let get_prog_err n =
-  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
-
-let obligations_solved prg = (snd prg.prg_obligations) = 0
-
-let all_programs () =
-  ProgMap.fold (fun k p l -> p :: l) !from_prg []
-
-type progress =
-    | Remain of int
-    | Dependent
-    | Defined of global_reference
-
-let obligations_message rem =
-  if rem > 0 then
-    if rem = 1 then
-      Flags.if_verbose msgnl (int rem ++ str " obligation remaining")
-    else
-      Flags.if_verbose msgnl (int rem ++ str " obligations remaining")
-  else
-    Flags.if_verbose msgnl (str "No more obligations remaining")
-
-let update_obls prg obls rem =
-  let prg' = { prg with prg_obligations = (obls, rem) } in
-    progmap_replace prg';
-    obligations_message rem;
-    if rem > 0 then Remain rem
-    else (
-      match prg'.prg_deps with
-      | [] ->
-	  let kn = declare_definition prg' in
-	    progmap_remove prg';
-	    Defined kn
-      | l ->
-	  let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
-	    if List.for_all (fun x -> obligations_solved x) progs then
-	      let kn = declare_mutual_definition progs in
-		Defined (ConstRef kn)
-	    else Dependent)
-
-let is_defined obls x = obls.(x).obl_body <> None
-
-let deps_remaining obls deps =
-  Intset.fold
-    (fun x acc ->
-      if is_defined obls x then acc
-      else x :: acc)
-    deps []
-
-let dependencies obls n =
-  let res = ref Intset.empty in
-    Array.iteri
-      (fun i obl ->
-	if i <> n && Intset.mem n obl.obl_deps then
-	  res := Intset.add i !res)
-      obls;
-    !res
-
-let kind_of_opacity o =
-  match o with
-  | Define false | Expand -> Subtac_utils.goal_kind
-  | _ -> Subtac_utils.goal_proof_kind
-
-let not_transp_msg =
-  str "Obligation should be transparent but was declared opaque." ++ spc () ++
-    str"Use 'Defined' instead."
-
-let warn_not_transp () = ppwarn not_transp_msg
-let error_not_transp () = pperror not_transp_msg
-
-let rec solve_obligation prg num tac =
-  let user_num = succ num in
-  let obls, rem = prg.prg_obligations in
-  let obl = obls.(num) in
-    if obl.obl_body <> None then
-      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
-    else
-      match deps_remaining obls obl.obl_deps with
-      | [] ->
-	  let obl = subst_deps_obl obls obl in
-	    Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
-	      (fun strength gr ->
-		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
-		let obl =
-		  let transparent = evaluable_constant cst (Global.env ()) in
-		  let body =
-		    match obl.obl_status with
-		    | Expand ->
-			if not transparent then error_not_transp ()
-			else constant_value (Global.env ()) cst
-		    | Define opaque ->
-			if not opaque && not transparent then error_not_transp ()
-			else Libnames.constr_of_global gr
-		  in
-		    if transparent then
-		      Auto.add_hints true [string_of_id prg.prg_name]
-			(Auto.HintsUnfoldEntry [EvalConstRef cst]);
-		    { obl with obl_body = Some body }
-		in
-		let obls = Array.copy obls in
-		let _ = obls.(num) <- obl in
-		let res = try update_obls prg obls (pred rem)
-		  with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
-		in
-		  match res with
-		  | Remain n when n > 0 ->
-		      let deps = dependencies obls num in
-			if deps <> Intset.empty then
-			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
-		  | _ -> ());
-	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
-	    Pfedit.by (snd (get_default_tactic ()));
-	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac;
-	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
-      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-		       ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
-
-and subtac_obligation (user_num, name, typ) tac =
-  let num = pred user_num in
-  let prg = get_prog_err name in
-  let obls, rem = prg.prg_obligations in
-    if num < Array.length obls then
-      let obl = obls.(num) in
-	match obl.obl_body with
-	    None -> solve_obligation prg num tac
-	  | Some r -> error "Obligation already solved"
-    else error (sprintf "Unknown obligation number %i" (succ num))
-
-
-and solve_obligation_by_tac prg obls i tac =
-  let obl = obls.(i) in
-    match obl.obl_body with
-    | Some _ -> false
-    | None ->
-	try
-	  if deps_remaining obls obl.obl_deps = [] then
-	    let obl = subst_deps_obl obls obl in
-	    let tac =
-	      match tac with
-	      | Some t -> t
-	      | None ->
-		  match obl.obl_tac with
-		  | Some t -> t
-		  | None -> snd (get_default_tactic ())
-	    in
-	    let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
-	      obls.(i) <- declare_obligation prg obl t;
-	      true
-	  else false
-	with
-	| Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	| Loc.Exc_located(_, Refiner.FailError (_, s))
-	| Refiner.FailError (_, s) ->
-	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-	| Errors.Anomaly _ as e -> raise e
-	| e -> false
-
-and solve_prg_obligations prg ?oblset tac =
-  let obls, rem = prg.prg_obligations in
-  let rem = ref rem in
-  let obls' = Array.copy obls in
-  let p = match oblset with
-    | None -> (fun _ -> true)
-    | Some s -> (fun i -> Intset.mem i s)
-  in
-  let _ =
-    Array.iteri (fun i x ->
-		 if p i && solve_obligation_by_tac prg obls' i tac then
-		   decr rem)
-      obls'
-  in
-    update_obls prg obls' !rem
-
-and solve_obligations n tac =
-  let prg = get_prog_err n in
-    solve_prg_obligations prg tac
-
-and solve_all_obligations tac =
-  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
-
-and try_solve_obligation n prg tac =
-  let prg = get_prog prg in
-  let obls, rem = prg.prg_obligations in
-  let obls' = Array.copy obls in
-    if solve_obligation_by_tac prg obls' n tac then
-      ignore(update_obls prg obls' (pred rem));
-
-and try_solve_obligations n tac =
-  try ignore (solve_obligations n tac) with NoObligations _ -> ()
-
-and auto_solve_obligations n ?oblset tac : progress =
-  Flags.if_verbose msgnl (str "Solving obligations automatically...");
-  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
-
-open Pp
-let show_obligations_of_prg ?(msg=true) prg =
-  let n = prg.prg_name in
-  let obls, rem = prg.prg_obligations in
-  let showed = ref 5 in
-    if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
-    Array.iteri (fun i x ->
-		   match x.obl_body with
-		   | None ->
-		       if !showed > 0 then (
-			 decr showed;
-			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
-				   str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
-				   hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
-		   | Some _ -> ())
-      obls
-
-let show_obligations ?(msg=true) n =
-  let progs = match n with
-    | None -> all_programs ()
-    | Some n ->
-	try [ProgMap.find n !from_prg]
-	with Not_found -> raise (NoObligations (Some n))
-  in List.iter (show_obligations_of_prg ~msg) progs
-
-let show_term n =
-  let prg = get_prog_err n in
-  let n = prg.prg_name in
-    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
-	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
-	    ++ my_print_constr (Global.env ()) prg.prg_body)
-
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
-  Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
-  let obls,_ = prg.prg_obligations in
-  if Array.length obls = 0 then (
-    Flags.if_verbose ppnl (str ".");
-    let cst = declare_definition prg in
-      Defined cst)
-  else (
-    let len = Array.length obls in
-    let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
-      progmap_add n prg;
-      let res = auto_solve_obligations (Some n) tactic in
-	match res with
-	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
-	| _ -> res)
-
-let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
-    ?(hook=fun _ _ -> ()) notations fixkind =
-  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
-    List.iter
-    (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info n (Some b) t deps (Some fixkind) 
-       notations obls imps kind reduce hook 
-     in progmap_add n prg) l;
-    let _defined =
-      List.fold_left (fun finished x ->
-	if finished then finished
-	else
-	  let res = auto_solve_obligations (Some x) tactic in
-	    match res with
-	    | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
-	    | _ -> false)
-	false deps
-    in ()
-
-let admit_obligations n =
-  let prg = get_prog_err n in
-  let obls, rem = prg.prg_obligations in
-    Array.iteri 
-      (fun i x ->
-	match x.obl_body with
-	| None ->
-            let x = subst_deps_obl obls x in
-	    let kn = Declare.declare_constant x.obl_name 
-              (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
-	    in
-	      assumption_message x.obl_name;
-	      obls.(i) <- { x with obl_body = Some (mkConst kn) }
-	| Some _ -> ())
-      obls;
-    ignore(update_obls prg obls 0)
-
-exception Found of int
-
-let array_find f arr =
-  try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
-    raise Not_found
-  with Found i -> i
-
-let next_obligation n tac =
-  let prg = get_prog_err n in
-  let obls, rem = prg.prg_obligations in
-  let i =
-    try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
-    with Not_found -> anomaly "Could not find a solvable obligation."
-  in solve_obligation prg i tac
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
deleted file mode 100644
index 284e975dbd..0000000000
--- a/plugins/subtac/subtac_obligations.mli
+++ /dev/null
@@ -1,73 +0,0 @@
-open Names
-open Pp
-open Util
-open Libnames
-open Evd
-open Proof_type
-open Vernacexpr
-
-type obligation_info =
-  (identifier * Term.types * hole_kind located *
-      obligation_definition_status * Intset.t * tactic option) array
-    (* ident, type, location, (opaque or transparent, expand or define),
-       dependencies, tactic to solve it *)
-
-type progress = (* Resolution status of a program *)
-  | Remain of int  (* n obligations remaining *)
-  | Dependent (* Dependent on other definitions *)
-  | Defined of global_reference (* Defined as id *)
-      
-val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val get_default_tactic : unit -> locality_flag * Proof_type.tactic
-val print_default_tactic : unit -> Pp.std_ppcmds
-
-val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
-val get_proofs_transparency : unit -> bool
-
-val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> 
-  ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
-  ?kind:Decl_kinds.definition_kind ->
-  ?tactic:Proof_type.tactic ->
-  ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
-
-type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
-
-type fixpoint_kind =
-  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
-  | IsCoFixpoint
-
-val add_mutual_definitions :
-  (Names.identifier * Term.constr * Term.types *
-      (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
-  ?tactic:Proof_type.tactic ->
-  ?kind:Decl_kinds.definition_kind ->
-  ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:Tacexpr.declaration_hook ->
-  notations ->
-  fixpoint_kind -> unit
-
-val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option ->
-  Tacexpr.raw_tactic_expr option -> unit
-
-val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit
-
-val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
-(* Number of remaining obligations to be solved for this program *)
-
-val solve_all_obligations : Proof_type.tactic option -> unit
-
-val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit
-
-val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit
-
-val show_obligations : ?msg:bool -> Names.identifier option -> unit
-
-val show_term : Names.identifier option -> unit
-
-val admit_obligations : Names.identifier option -> unit
-
-exception NoObligations of Names.identifier option
-
-val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds
-
diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
deleted file mode 100644
index c932a71716..0000000000
--- a/plugins/subtac/subtac_plugin.mllib
+++ /dev/null
@@ -1,10 +0,0 @@
-Subtac_utils
-Eterm
-Subtac_errors
-Subtac_obligations
-Subtac_pretyping
-Subtac_command
-Subtac_classes
-Subtac
-G_subtac
-Subtac_plugin_mod
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
deleted file mode 100644
index f64c1ae2f2..0000000000
--- a/plugins/subtac/subtac_pretyping.ml
+++ /dev/null
@@ -1,137 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Global
-open Pp
-open Errors
-open Util
-open Names
-open Sign
-open Evd
-open Term
-open Termops
-open Reductionops
-open Environ
-open Type_errors
-open Typeops
-open Libnames
-open Classops
-open List
-open Recordops
-open Evarutil
-open Pretype_errors
-open Glob_term
-open Evarconv
-open Pattern
-
-open Subtac_coercion
-open Subtac_utils
-open Coqlib
-open Printer
-open Subtac_errors
-open Eterm
-
-open Pretyping
-
-let _ = Pretyping.allow_anonymous_refs := true
-
-type recursion_info = {
-  arg_name: name;
-  arg_type: types; (* A *)
-  args_after : rel_context;
-  wf_relation: constr; (* R : A -> A -> Prop *)
-  wf_proof: constr; (* : well_founded R *)
-  f_type: types; (* f: A -> Set *)
-  f_fulltype: types; (* Type with argument and wf proof product first *)
-}
-
-let my_print_rec_info env t =
-  str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
-  str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
-  str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
-  str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
-  str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
-  str "Full type: " ++ my_print_constr env t.f_fulltype
-(*   trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *)
-(* 	   str " and tycon "++ my_print_tycon env tycon ++ *)
-(* 	   str " in environment: " ++ my_print_env env); *)
-
-let interp env isevars c tycon =
-  let j = pretype tycon env isevars ([],[]) c in
-  let _ = isevars := Evarutil.nf_evar_map !isevars in
-  let evd = consider_remaining_unif_problems env !isevars in
-(*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
-  let evm =  unevd' in
-    isevars := unevd';
-    nf_evar evm j.uj_val, nf_evar evm j.uj_type
-
-let find_with_index x l =
-  let rec aux i = function
-      (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-open Vernacexpr
-
-let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr = 
-  Constrintern.intern_constr evd env
-let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = 
-  Constrintern.intern_type evd env
-
-let env_with_binders env isevars l =
-  let rec aux ((env, rels) as acc) = function
-      Topconstr.LocalRawDef ((loc, name), def) :: tl ->
-	let rawdef = coqintern_constr !isevars env def in
-	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
-	let reldecl = (name, Some coqdef, deftyp) in
-	  aux  (push_rel reldecl env, reldecl :: rels) tl
-    | Topconstr.LocalRawAssum (bl, k, typ) :: tl ->
-	let rawtyp = coqintern_type !isevars env typ in
-	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
-	let acc =
-	  List.fold_left (fun (env, rels) (loc, name) ->
-			    let reldecl = (name, None, coqtyp) in
-			      (push_rel reldecl env,
-			       reldecl :: rels))
-	    (env, rels) bl
-	in aux acc tl
-    | [] -> acc
-  in aux (env, []) l
-
-let subtac_process ?(is_type=false) env isevars id bl c tycon =
-  let c = Topconstr.abstract_constr_expr c bl in
-  let tycon, imps =
-    match tycon with
-	None -> empty_tycon, None
-      | Some t ->
-	  let t = Topconstr.prod_constr_expr t bl in
-	  let t = coqintern_type !isevars env t in
-	  let imps = Implicit_quantifiers.implicits_of_glob_constr t in
-	  let coqt, ttyp = interp env isevars t empty_tycon in
-	    mk_tycon coqt, Some imps
-  in
-  let c = coqintern_constr !isevars env c in
-  let imps = match imps with 
-    | Some i -> i
-    | None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c
-  in
-  let coqc, ctyp = interp env isevars c tycon in
-  let evm = non_instanciated_map env isevars !isevars in
-  let ty = nf_evar !isevars (match tycon with Some c -> c | _ -> ctyp) in
-    evm, coqc, ty, imps
-
-open Subtac_obligations
-
-let subtac_proof kind hook env isevars id bl c tycon =
-  let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
-  let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
-  let evm' = Subtac_utils.evars_of_term evm evm' coqt in
-  let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
-    add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
deleted file mode 100644
index e999f1710c..0000000000
--- a/plugins/subtac/subtac_pretyping.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-open Term
-open Environ
-open Names
-open Sign
-open Evd
-open Global
-open Topconstr
-open Implicit_quantifiers
-open Impargs
-
-val interp :
-    Environ.env ->
-    Evd.evar_map ref ->
-    Glob_term.glob_constr ->
-    Evarutil.type_constraint -> Term.constr * Term.constr
-
-val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
-  constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
-
-val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_map ref -> identifier -> local_binder list ->
-  constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
deleted file mode 100644
index 8f56bf52c0..0000000000
--- a/plugins/subtac/subtac_utils.ml
+++ /dev/null
@@ -1,479 +0,0 @@
-(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
-
-open Evd
-open Libnames
-open Coqlib
-open Term
-open Names
-open Errors
-open Pp
-open Util
-
-let ($) f x = f x
-
-(****************************************************************************)
-(* Library linking *)
-
-let contrib_name = "Program"
-let subtac_dir = [contrib_name]
-let fixsub_module = subtac_dir @ ["Wf"]
-let utils_module = subtac_dir @ ["Utils"]
-let tactics_module = subtac_dir @ ["Tactics"]
-let init_constant dir s () = gen_constant contrib_name dir s
-let init_reference dir s () = gen_reference contrib_name dir s
-
-let safe_init_constant md name () =
-  check_required_library ("Coq"::md);
-  init_constant md name ()
-let fix_proto = safe_init_constant tactics_module "fix_proto"
-let hide_obligation = safe_init_constant tactics_module "obligation"
-
-let ex_pi1 = init_constant utils_module "ex_pi1"
-let ex_pi2 = init_constant utils_module "ex_pi2"
-
-let make_ref l s = init_reference l s
-let fix_sub_ref = make_ref fixsub_module "Fix_sub"
-let measure_on_R_ref = make_ref fixsub_module "MR"
-let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
-let acc_ref = make_ref  ["Init";"Wf"] "Acc"
-let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
-let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
-let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
-
-let make_ref s = Qualid (dummy_loc, qualid_of_string s)
-let lt_ref = make_ref "Init.Peano.lt"
-let sig_ref = make_ref "Init.Specif.sig"
-let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
-let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
-
-let build_sig () =
-  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" ();
-    proj2 = init_constant ["Init"; "Specif"] "proj2_sig" ();
-    elim = init_constant ["Init"; "Specif"] "sig_rec" ();
-    intro = init_constant ["Init"; "Specif"] "exist" ();
-    typ = init_constant ["Init"; "Specif"] "sig" () }
-
-let sig_ = build_sig
-
-let fix_proto = safe_init_constant tactics_module "fix_proto"
-let hide_obligation = safe_init_constant tactics_module "obligation"
-
-let eq_ind = init_constant ["Init"; "Logic"] "eq"
-let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
-let eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
-let eq_refl = init_constant ["Init"; "Logic"] "refl_equal"
-let eq_ind_ref = init_reference ["Init"; "Logic"] "eq"
-let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal"
-
-let not_ref = init_constant ["Init"; "Logic"] "not"
-
-let and_typ = Coqlib.build_coq_and
-
-let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep"
-let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec"
-let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
-let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"
-
-let jmeq_ind =
-  safe_init_constant ["Logic";"JMeq"] "JMeq"
-
-let jmeq_rec =
-  init_constant ["Logic";"JMeq"] "JMeq_rec"
-
-let jmeq_refl =
-  init_constant ["Logic";"JMeq"] "JMeq_refl"
-
-let ex_ind = init_constant ["Init"; "Logic"] "ex"
-let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
-
-let proj1 = init_constant ["Init"; "Logic"] "proj1"
-let proj2 = init_constant ["Init"; "Logic"] "proj2"
-
-let existS = build_sigma_type
-
-let prod = build_prod
-
-
-(* orders *)
-let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let fix = init_constant ["Init"; "Wf"] "Fix"
-let acc = init_constant ["Init"; "Wf"] "Acc"
-let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv"
-
-let extconstr = Constrextern.extern_constr true (Global.env ())
-let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
-
-open Pp
-
-let my_print_constr = Termops.print_constr_env
-let my_print_constr_expr = Ppconstr.pr_constr_expr
-let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
-let my_print_context = Termops.print_rel_context
-let my_print_named_context = Termops.print_named_context
-let my_print_env = Termops.print_env
-let my_print_glob_constr = Printer.pr_glob_constr_env
-let my_print_evardefs = Evd.pr_evar_map None
-
-let my_print_tycon = Evarutil.pr_tycon
-
-let debug_level = 2
-
-let debug_on = true
-
-let debug n s =
-  if debug_on then
-    if !Flags.debug && n >= debug_level then
-      msgnl s
-    else ()
-  else ()
-
-let debug_msg n s =
-  if debug_on then
-    if !Flags.debug  && n >= debug_level then s
-    else mt ()
-  else mt ()
-
-let trace s =
-  if debug_on then
-    if !Flags.debug  && debug_level > 0 then msgnl s
-    else ()
-  else ()
-
-let rec pp_list f = function
-    [] -> mt()
-  | x :: y -> f x ++ spc () ++ pp_list f y
-
-let wf_relations = Hashtbl.create 10
-
-let std_relations () =
-  let add k v = Hashtbl.add wf_relations k v in
-    add (init_constant ["Init"; "Peano"] "lt" ())
-      (init_constant ["Arith"; "Wf_nat"] "lt_wf")
-
-let std_relations = Lazy.lazy_from_fun std_relations
-
-type binders = Topconstr.local_binder list
-
-let app_opt c e =
-  match c with
-      Some constr -> constr e
-    | None -> e
-
-let print_args env args =
-  Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
-
-let make_existential loc ?(opaque = Define true) env isevars c =
-  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
-  let (key, args) = destEvar evar in
-    (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
-		  print_args env args ++ str " for type: "++
-		  my_print_constr env c) with _ -> ());
-    evar
-
-let make_existential_expr loc env c =
-  let key = Evarutil.new_untyped_evar () in
-  let evar = Topconstr.CEvar (loc, key, None) in
-    debug 2 (str "Constructed evar " ++ int key);
-    evar
-
-let string_of_hole_kind = function
-  | ImplicitArg _ -> "ImplicitArg"
-  | BinderType _ -> "BinderType"
-  | QuestionMark _ -> "QuestionMark"
-  | CasesType -> "CasesType"
-  | InternalHole -> "InternalHole"
-  | TomatchTypeParameter _ -> "TomatchTypeParameter"
-  | GoalEvar -> "GoalEvar"
-  | ImpossibleCase -> "ImpossibleCase"
-  | MatchingVar _ -> "MatchingVar"
-
-let evars_of_term evc init c =
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
-    | Evar (n, _) -> assert(false)
-    | _ -> fold_constr evrec acc c
-  in
-    evrec init c
-
-let non_instanciated_map env evd evm =
-  List.fold_left
-    (fun evm (key, evi) ->
-       let (loc,k) = evar_source key !evd in
-	 debug 2 (str "evar " ++ int key ++ str " has kind " ++
-		    str (string_of_hole_kind k));
-	 match k with
-	 | QuestionMark _ -> Evd.add evm key evi
-	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
-	 | _ ->
-	     debug 2 (str " and is an implicit");
-	     Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
-    Evd.empty (Evarutil.non_instantiated evm)
-
-let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
-
-let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
-let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
-
-let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
-let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
-
-open Tactics
-open Tacticals
-
-let filter_map f l =
-  let rec aux acc = function
-      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
-		     | None -> aux acc tl)
-    | [] -> List.rev acc
-  in aux [] l
-
-let build_dependent_sum l =
-  let rec aux names conttac conttype = function
-      (n, t) :: ((_ :: _) as tl) ->
-	let hyptype = substl names t in
-	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
-	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
-	   with _ -> ());
-	let tac = assert_tac (Name n) hyptype in
-	let conttac =
-	  (fun cont ->
-	     conttac
-	     (tclTHENS tac
-		([intros;
-		  (tclTHENSEQ
-		     [constructor_tac false (Some 1) 1
-			(Glob_term.ImplicitBindings [mkVar n]);
-		      cont]);
-		 ])))
-	in
-	let conttype =
-	  (fun typ ->
-	     let tex = mkLambda (Name n, t, typ) in
-	       conttype
-		 (mkApp (ex_ind (), [| t; tex |])))
-	in
-	  aux (mkVar n :: names) conttac conttype tl
-    | (n, t) :: [] ->
-	(conttac intros, conttype t)
-    | [] -> raise (Invalid_argument "build_dependent_sum")
-  in aux [] identity identity (List.rev l)
-
-open Proof_type
-open Tacexpr
-
-let mkProj1 a b c =
-  mkApp (delayed_force proj1, [| a; b; c |])
-
-let mkProj2 a b c =
-  mkApp (delayed_force proj2, [| a; b; c |])
-
-let mk_ex_pi1 a b c =
-  mkApp (delayed_force ex_pi1, [| a; b; c |])
-
-let mk_ex_pi2 a b c =
-  mkApp (delayed_force ex_pi2, [| a; b; c |])
-
-let mkSubset name typ prop =
-  mkApp ((delayed_force sig_).typ,
-	 [| typ; mkLambda (name, typ, prop) |])
-
-let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |])
-
-let unsafe_fold_right f = function
-    hd :: tl -> List.fold_right f tl hd
-  | [] -> raise (Invalid_argument "unsafe_fold_right")
-
-let mk_conj l =
-  let conj_typ = delayed_force and_typ in
-    unsafe_fold_right
-      (fun c conj ->
-	 mkApp (conj_typ, [| c ; conj |]))
-      l
-
-let mk_not c =
-  let notc = delayed_force not_ref in
-    mkApp (notc, [| c |])
-
-let and_tac l hook =
-  let andc = Coqlib.build_coq_and () in
-  let rec aux ((accid, goal, tac, extract) as acc) = function
-    | [] -> (* Singleton *) acc
-
-    | (id, x, elgoal, eltac) :: tl ->
-	let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
-	let proj = fun c -> mkProj2 goal elgoal c in
-	let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
-	  aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
-	       (id, x, elgoal, proj) :: extract) tl
-
-  in
-  let and_proof_id, and_goal, and_tac, and_extract =
-    match l with
-      | [] -> raise (Invalid_argument "and_tac: empty list of goals")
-      | (hdid, x, hdg, hdt) :: tl ->
-	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
-  in
-  let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
-    Lemmas.start_proof and_proofid goal_kind and_goal
-      (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
-    trace (str "Started and proof");
-    Pfedit.by and_tac;
-    trace (str "Applied and tac")
-
-
-let destruct_ex ext ex =
-  let rec aux c acc =
-    match kind_of_term c with
-	App (f, args) ->
-	  (match kind_of_term f with
-	       Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
-		 let (dom, rng) =
-		   try (args.(0), args.(1))
-		   with _ -> assert(false)
-		 in
-		 let pi1 = (mk_ex_pi1 dom rng acc) in
-		 let rng_body =
-		   match kind_of_term rng with
-		       Lambda (_, _, t) -> subst1 pi1 t
-		     | t -> rng
-		 in
-		   pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
-	     | _ -> [acc])
-      | _ -> [acc]
-  in aux ex ext
-
-open Glob_term
-
-let id_of_name = function
-    Name n -> n
-  | Anonymous -> raise (Invalid_argument "id_of_name")
-
-let definition_message id =
-  Nameops.pr_id id ++ str " is defined"
-
-let recursive_message v =
-  match Array.length v with
-    | 0 -> error "no recursive definition"
-    | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined")
-    | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++
-		    spc () ++ str "are recursively defined")
-
-let print_message m =
-  Flags.if_verbose ppnl m
-
-(* Solve an obligation using tactics, return the corresponding proof term *)
-let solve_by_tac evi t =
-  let id = id_of_string "H" in
-  try
-    Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
-    (fun _ _ -> ());
-    Pfedit.by (tclCOMPLETE t);
-    let _,(const,_,_,_) = Pfedit.cook_proof ignore in
-      Pfedit.delete_current_proof (); 
-      Inductiveops.control_only_guard (Global.env ())
-	const.Entries.const_entry_body;
-      const.Entries.const_entry_body
-  with e ->
-    Pfedit.delete_current_proof();
-    raise e
-
-(* let apply_tac t goal = t goal *)
-
-(* let solve_by_tac evi t = *)
-(*   let ev = 1 in *)
-(*   let evm = Evd.add Evd.empty ev evi in *)
-(*   let goal = {it = evi; sigma = evm } in *)
-(*   let (res, valid) = apply_tac t goal in *)
-(*     if res.it = [] then *)
-(*       let prooftree = valid [] in *)
-(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
-(* 	if obls = [] then proofterm *)
-(* 	else raise Exit *)
-(*     else raise Exit *)
-
-let rec string_of_list sep f = function
-    [] -> ""
-  | x :: [] -> f x
-  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
-
-let string_of_intset d =
-  string_of_list "," string_of_int (Intset.elements d)
-
-(**********************************************************)
-(* Pretty-printing *)
-open Printer
-open Ppconstr
-open Nameops
-open Evd
-
-let pr_meta_map evd =
-  let ml = meta_list evd in
-  let pr_name = function
-      Name id -> str"[" ++ pr_id id ++ str"]"
-    | _ -> mt() in
-  let pr_meta_binding = function
-    | (mv,Cltyp (na,b)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " : " ++
-           Termops.print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,b,_)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " := " ++
-             Termops.print_constr (fst b).rebus ++ fnl ())
-  in
-  prlist pr_meta_binding ml
-
-let pr_idl idl = pr_sequence pr_id idl
-
-let pr_evar_info evi =
-  let phyps =
-    (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
-    Printer.pr_named_context (Global.env()) (evar_context evi)
-  in
-  let pty = Termops.print_constr evi.evar_concl in
-  let pb =
-    match evi.evar_body with
-      | Evar_empty -> mt ()
-      | Evar_defined c -> spc() ++ str"=> "  ++ Termops.print_constr c
-  in
-  hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
-
-let pr_evar_map sigma =
-  h 0
-    (prlist_with_sep fnl
-      (fun (ev,evi) ->
-        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
-      (to_list sigma))
-
-let pr_constraints pbs =
-  h 0
-    (prlist_with_sep fnl (fun (pbty,t1,t2) ->
-      Termops.print_constr t1 ++ spc() ++
-      str (match pbty with
-	| Reduction.CONV -> "=="
-	| Reduction.CUMUL -> "<=") ++
-      spc() ++ Termops.print_constr t2) pbs)
-
-let pr_evar_map evd =
-  let pp_evm =
-    let evars =  evd in
-    if evars = empty then mt() else
-      str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
-  let pp_met =
-    if meta_list evd = [] then mt() else
-      str"METAS:"++brk(0,1)++pr_meta_map evd in
-  v 0 (pp_evm ++ pp_met)
-
-let contrib_tactics_path =
-  make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
-
-let tactics_tac s =
-  lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
-
-let tactics_call tac args =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
deleted file mode 100644
index 5cbb307db3..0000000000
--- a/plugins/subtac/subtac_utils.mli
+++ /dev/null
@@ -1,130 +0,0 @@
-open Term
-open Libnames
-open Coqlib
-open Environ
-open Pp
-open Evd
-open Decl_kinds
-open Topconstr
-open Glob_term
-open Errors
-open Util
-open Evarutil
-open Names
-open Sign
-
-val ($) : ('a -> 'b) -> 'a -> 'b
-val contrib_name : string
-val subtac_dir : string list
-val fixsub_module : string list
-val init_constant : string list -> string -> constr delayed
-val init_reference : string list -> string -> global_reference delayed
-val well_founded_ref : global_reference delayed
-val acc_ref : global_reference delayed
-val acc_inv_ref : global_reference delayed
-val fix_sub_ref : global_reference delayed
-val measure_on_R_ref : global_reference delayed
-val fix_measure_sub_ref : global_reference delayed
-val refl_ref : global_reference delayed
-val lt_ref : reference
-val sig_ref : reference
-val proj1_sig_ref : reference
-val proj2_sig_ref : reference
-val build_sig : unit -> coq_sigma_data
-val sig_ : coq_sigma_data delayed
-
-val fix_proto : constr delayed
-
-val hide_obligation : constr delayed
-
-val eq_ind : constr delayed
-val eq_rec : constr delayed
-val eq_rect : constr delayed
-val eq_refl : constr delayed
-
-val not_ref : constr delayed
-val and_typ : constr delayed
-
-val eqdep_ind : constr delayed
-val eqdep_rec : constr delayed
-
-val jmeq_ind : constr delayed
-val jmeq_rec : constr delayed
-val jmeq_refl : constr delayed
-
-val existS : coq_sigma_data delayed
-val prod : coq_sigma_data delayed
-
-val well_founded : constr delayed
-val fix : constr delayed
-val acc : constr delayed
-val acc_inv : constr delayed
-val extconstr : constr -> constr_expr
-val extsort : sorts -> constr_expr
-
-val my_print_constr : env -> constr -> std_ppcmds
-val my_print_constr_expr : constr_expr -> std_ppcmds
-val my_print_evardefs : evar_map -> std_ppcmds
-val my_print_context : env -> std_ppcmds
-val my_print_rel_context : env -> rel_context -> std_ppcmds
-val my_print_named_context : env -> std_ppcmds
-val my_print_env : env -> std_ppcmds
-val my_print_glob_constr : env -> glob_constr -> std_ppcmds
-val my_print_tycon : env -> type_constraint -> std_ppcmds
-
-
-val debug : int -> std_ppcmds -> unit
-val debug_msg : int -> std_ppcmds -> std_ppcmds
-val trace : std_ppcmds -> unit
-val wf_relations : (constr, constr delayed) Hashtbl.t
-
-type binders = local_binder list
-val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> ?opaque:obligation_definition_status ->
-  env -> evar_map ref -> types -> constr
-val make_existential_expr : loc -> 'a -> 'b -> constr_expr
-val string_of_hole_kind : hole_kind -> string
-val evars_of_term : evar_map -> evar_map -> constr -> evar_map
-val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map
-val global_kind : logical_kind
-val goal_kind : locality * goal_object_kind
-val global_proof_kind : logical_kind
-val goal_proof_kind : locality * goal_object_kind
-val global_fix_kind : logical_kind
-val goal_fix_kind : locality * goal_object_kind
-
-val mkSubset : name -> constr -> constr -> constr
-val mkProj1 : constr -> constr -> constr -> constr
-val mkProj1 : constr -> constr -> constr -> constr
-val mk_ex_pi1 : constr -> constr -> constr -> constr
-val mk_ex_pi1 : constr -> constr -> constr -> constr
-val mk_eq : types -> constr -> constr -> types
-val mk_eq_refl : types -> constr -> constr
-val mk_JMeq : types -> constr-> types -> constr -> types
-val mk_JMeq_refl : types -> constr -> constr
-val mk_conj : types list -> types
-val mk_not : types -> types
-
-val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
-val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
-  ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
-
-val destruct_ex : constr -> constr -> constr list
-
-val id_of_name : name -> identifier
-
-val definition_message : identifier -> std_ppcmds
-val recursive_message : constant array -> std_ppcmds
-
-val print_message : std_ppcmds -> unit
-
-val solve_by_tac : evar_info -> Tacmach.tactic -> constr
-
-val string_of_list : string -> ('a -> string) -> 'a list -> string
-val string_of_intset : Intset.t -> string
-
-val pr_evar_map : evar_map -> Pp.std_ppcmds
-
-val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
-
-val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
deleted file mode 100644
index e3dbd127f9..0000000000
--- a/plugins/subtac/test/ListDep.v
+++ /dev/null
@@ -1,49 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import List.
-Require Import Coq.Program.Program.
-
-Set Implicit Arguments.
-
-Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
-
-Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
-Proof.
-  intros.
-  inversion H.
-  split.
-  intros.
-  apply H0.
-  auto with datatypes.
-  auto with arith.
-Qed.
-
-Section Map_DependentRecursor.
-  Variable U V : Set.
-  Variable l : list U.
-  Variable f : { x : U | In x l } -> V.
-
-  Obligations Tactic := unfold sub_list in * ;
-    program_simpl ; intuition.
-
-  Program Fixpoint map_rec ( l' : list U | sub_list l' l )
-    { measure length l' } : { r : list V | length r = length l' } :=
-    match l' with
-      | nil => nil
-      | cons x tl => let tl' := map_rec tl in
-	f x :: tl'
-    end.
-
-  Next Obligation.
-    destruct_call map_rec.
-    simpl in *.
-    subst l'.
-    simpl ; auto with arith.
-  Qed.
-
-  Program Definition map : list V := map_rec l.
-
-End Map_DependentRecursor.
-
-Extraction map.
-Extraction map_rec.
-
diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
deleted file mode 100644
index 2cea0841de..0000000000
--- a/plugins/subtac/test/ListsTest.v
+++ /dev/null
@@ -1,99 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.Program.Program.
-Require Import List.
-
-Set Implicit Arguments.
-
-Section Accessors.
-  Variable A : Set.
-
-  Program Definition myhd : forall (l : list A | length l <> 0), A :=
-    fun l =>
-      match l with
-        | nil => !
-        | hd :: tl => hd
-      end.
-
-  Program Definition mytail (l : list A | length l <> 0) : list A :=
-    match l with
-      | nil => !
-      | hd :: tl => tl
-    end.
-End Accessors.
-
-Program Definition test_hd : nat := myhd (cons 1 nil).
-
-(*Eval compute in test_hd*)
-(*Program Definition test_tail : list A := mytail nil.*)
-
-Section app.
-  Variable A : Set.
-
-  Program Fixpoint app (l : list A) (l' : list A) { struct l } :
-    { r : list A | length r = length l + length l' } :=
-    match l with
-      | nil => l'
-      | hd :: tl => hd :: (tl ++ l')
-    end
-    where "x ++ y" := (app x y).
-
-  Next Obligation.
-    intros.
-    destruct_call app ; program_simpl.
-  Defined.
-
-  Program Lemma app_id_l : forall l : list A, l = nil ++ l.
-  Proof.
-    simpl ; auto.
-  Qed.
-
-  Program Lemma app_id_r : forall l : list A, l = l ++ nil.
-  Proof.
-    induction l ; simpl in * ; auto.
-    rewrite <- IHl ; auto.
-  Qed.
-
-End app.
-
-Extraction app.
-
-Section Nth.
-
-  Variable A : Set.
-
-  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
-    match n, l with
-      | 0, hd :: _ => hd
-      | S n', _ :: tl => nth tl n'
-      | _, nil => !
-    end.
-
-  Next Obligation.
-  Proof.
-    simpl in *. auto with arith.
-  Defined.
-
-  Next Obligation.
-  Proof.
-    inversion H.
-  Qed.
-
-  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
-    match l, n with
-      | hd :: _, 0 => hd
-      | _ :: tl, S n' => nth' tl n'
-      | nil, _ => !
-    end.
-  Next Obligation.
-  Proof.
-    simpl in *. auto with arith.
-  Defined.
-
-  Next Obligation.
-  Proof.
-    intros.
-    inversion H.
-  Defined.
-
-End Nth.
-
diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
deleted file mode 100644
index 01e2d75f33..0000000000
--- a/plugins/subtac/test/Mutind.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Require Import List.
-
-Program Fixpoint f a : { x : nat | x > 0 } :=
-  match a with
-  | 0 => 1
-  | S a' => g a a'
-  end
-with g a b : { x : nat | x > 0 } :=
-  match b with
-  | 0 => 1
-  | S b' => f b'
-  end.
-
-Check f.
-Check g.
-
-
-
-
-
diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
deleted file mode 100644
index 7e0755d571..0000000000
--- a/plugins/subtac/test/Test1.v
+++ /dev/null
@@ -1,16 +0,0 @@
-Program Definition test (a b : nat) : { x : nat | x = a + b } :=
-  ((a + b) : { x : nat | x = a + b }).
-Proof.
-intros.
-reflexivity.
-Qed.
-
-Print test.
-
-Require Import List.
-
-Program hd_opt (l : list nat) : { x : nat | x <> 0 } :=
-  match l with
-    nil => 1
-    | a :: l => a
-  end.
diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
deleted file mode 100644
index 97c3d9414d..0000000000
--- a/plugins/subtac/test/euclid.v
+++ /dev/null
@@ -1,24 +0,0 @@
-Require Import Coq.Program.Program.
-Require Import Coq.Arith.Compare_dec.
-Notation "( x & y )" := (existS _ x y) : core_scope.
-
-Require Import Omega.
-
-Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a}  :
-  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
-  if le_lt_dec b a then let (q', r) := euclid (a - b) b in
-  (S q' & r)
-  else (O & a).
-
-Next Obligation.
-  assert(b * S q' = b * q' + b) by auto with arith ; omega.
-Defined.
-
-Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
-
-Eval lazy beta zeta delta iota in test_euclid.
-
-Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } :=
-  (a & S a).
-
-Check testsig.
diff --git a/plugins/subtac/test/id.v b/plugins/subtac/test/id.v
deleted file mode 100644
index 9ae1108817..0000000000
--- a/plugins/subtac/test/id.v
+++ /dev/null
@@ -1,46 +0,0 @@
-Require Coq.Arith.Arith.
-
-Require Import Coq.subtac.Utils.
-Program Fixpoint id (n : nat) : { x : nat | x = n } :=
-  match n with
-  | O => O
-  | S p => S (id p)
-  end.
-intros ; auto.
-
-pose (subset_simpl (id p)).
-simpl in e.
-unfold p0.
-rewrite e.
-auto.
-Defined.
-
-Check id.
-Print id.
-Extraction id.
-
-Axiom le_gt_dec : forall n m, { n <= m } + { n > m }.
-Require Import Omega.
-
-Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } :=
-  if le_gt_dec n 0 then 0
-  else S (id_if (pred n)).
-intros.
-auto with arith.
-intros.
-pose (subset_simpl (id_if (pred n))).
-simpl in e.
-rewrite e.
-induction n ; auto with arith.
-Defined.
-
-Print id_if_instance.
-Extraction id_if_instance.
-
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
-
-Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} :=
-  (a & a).
-intros.
-auto.
-Qed.
diff --git a/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v
deleted file mode 100644
index 4f938f4f87..0000000000
--- a/plugins/subtac/test/measure.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
-Unset Printing All.
-Require Import Coq.Arith.Compare_dec.
-
-Require Import Coq.Program.Program.
-
-Fixpoint size (a : nat) : nat :=
-  match a with
-  0 => 1
-  | S n => S (size n)
-  end.
-
-Program Fixpoint test_measure (a : nat) {measure size a}  : nat :=
-  match a with
-  | S (S n) => S (test_measure n)
-  | 0 | S 0 => a
-  end.
-
-Check test_measure.
-Print test_measure.
\ No newline at end of file
diff --git a/plugins/subtac/test/rec.v b/plugins/subtac/test/rec.v
deleted file mode 100644
index aaefd8cc5f..0000000000
--- a/plugins/subtac/test/rec.v
+++ /dev/null
@@ -1,65 +0,0 @@
-Require Import Coq.Arith.Arith.
-Require Import Lt.
-Require Import Omega.
-
-Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }.
-(*Proof.
-  intros.
-  elim (le_lt_dec y x) ; intros ; auto with arith.
-Defined.
-*)
-Require Import Coq.subtac.FixSub.
-Require Import Wf_nat.
-
-Lemma preda_lt_a : forall a, 0 < a -> pred a < a.
-auto with arith.
-Qed.
-
-Program Fixpoint id_struct (a : nat) : nat :=
-  match a with
-  0 => 0
-  | S n => S (id_struct n)
-  end.
-
-Check struct_rec.
-
-  if (lt_ge_dec O a)
-  then S (wfrec (pred a))
-  else O.
-
-Program Fixpoint wfrec (a : nat) { wf a lt } : nat :=
-  if (lt_ge_dec O a)
-  then S (wfrec (pred a))
-  else O.
-intros.
-apply preda_lt_a ; auto.
-
-Defined.
-
-Extraction wfrec.
-Extraction Inline proj1_sig.
-Extract Inductive bool => "bool" [ "true" "false" ].
-Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extract Inlined Constant lt_ge_dec => "<".
-
-Extraction wfrec.
-Extraction Inline lt_ge_dec le_lt_dec.
-Extraction wfrec.
-
-
-Program Fixpoint structrec (a : nat) { wf a lt } : nat :=
-  match a with
-   S n => S (structrec n)
-   | 0 => 0
-   end.
-intros.
-unfold n0.
-omega.
-Defined.
-
-Print structrec.
-Extraction structrec.
-Extraction structrec.
-
-Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a).
-Print structrec_fun.
diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v
deleted file mode 100644
index 90ae8bae84..0000000000
--- a/plugins/subtac/test/take.v
+++ /dev/null
@@ -1,34 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import JMeq.
-Require Import List.
-Require Import Program.
-
-Set Implicit Arguments.
-Obligations Tactic := idtac.
-
-Print cons.
-
-Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
-  match n with
-  | 0 => nil
-  | S p =>
-    match l with
-    | cons hd tl => let rest := take tl p in cons hd rest
-    | nil => !
-    end
-  end.
-
-Require Import Omega.
-Solve All Obligations.
-Next Obligation.
-  destruct_call take ; program_simpl.
-Defined.
-
-Next Obligation.
-  intros.
-  inversion H.
-Defined.
-
-
-
-
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v
deleted file mode 100644
index 5ccc154afd..0000000000
--- a/plugins/subtac/test/wf.v
+++ /dev/null
@@ -1,48 +0,0 @@
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
-Unset Printing All.
-Require Import Coq.Arith.Compare_dec.
-
-Require Import Coq.subtac.Utils.
-
-Ltac one_simpl_hyp :=
- match goal with
- | [H : (`exist _ _ _) = _ |- _] => simpl in H
- | [H : _ = (`exist _ _ _) |- _] => simpl in H
- | [H : (`exist _ _ _) < _ |- _] => simpl in H
- | [H : _ < (`exist _ _ _) |- _] => simpl in H
- | [H : (`exist _ _ _) <= _ |- _] => simpl in H
- | [H : _ <= (`exist _ _ _) |- _] => simpl in H
- | [H : (`exist _ _ _) > _ |- _] => simpl in H
- | [H : _ > (`exist _ _ _) |- _] => simpl in H
- | [H : (`exist _ _ _) >= _ |- _] => simpl in H
- | [H : _ >= (`exist _ _ _) |- _] => simpl in H
- end.
-
-Ltac one_simpl_subtac :=
-  destruct_exists ;
-  repeat one_simpl_hyp ; simpl.
-
-Ltac simpl_subtac :=  do 3 one_simpl_subtac ; simpl.
-
-Require Import Omega.
-Require Import Wf_nat.
-
-Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
-  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
-  if le_lt_dec b a then let (q', r) := euclid (a - b) b in
-  (S q' & r)
-  else (O & a).
-destruct b ; simpl_subtac.
-omega.
-simpl_subtac.
-assert(x0 * S q' = x0 + x0 * q').
-rewrite <- mult_n_Sm.
-omega.
-rewrite H2 ; omega.
-simpl_subtac.
-split ; auto with arith.
-omega.
-apply lt_wf.
-Defined.
-
-Check euclid_evars_proof.
\ No newline at end of file