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

49 files changed, 683 insertions, 2902 deletions

diff --git a/Makefile.build b/Makefile.build
index 04c01973e..d63558c2b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -451,7 +451,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 ###########################################################################
 
 .PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction
-.PHONY: field fourier funind cc subtac rtauto btauto pluginsopt
+.PHONY: field fourier funind cc rtauto btauto pluginsopt
 
 plugins: $(PLUGINSVO)
 omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
@@ -466,7 +466,6 @@ field: $(FIELDVO) $(FIELDCMA)
 fourier: $(FOURIERVO) $(FOURIERCMA)
 funind: $(FUNINDCMA) $(FUNINDVO)
 cc: $(CCVO) $(CCCMA)
-subtac: $(SUBTACCMA)
 rtauto: $(RTAUTOVO) $(RTAUTOCMA)
 btauto: $(BTAUTOVO) $(BTAUTOCMA)
 
diff --git a/Makefile.common b/Makefile.common
index 88f035ac4..5f32ee13f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -81,7 +81,7 @@ SRCDIRS:=\
   $(addprefix plugins/, \
     omega	romega 		micromega 	quote		ring	dp \
     setoid_ring xml 		extraction 	fourier \
-    cc 		funind 		firstorder 	field 		subtac \
+    cc 		funind 		firstorder 	field \
     rtauto 	nsatz           syntax          decl_mode	btauto)
 
 # Order is relevent here because kernel and checker contain files
@@ -184,7 +184,6 @@ EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
 FUNINDCMA:=plugins/funind/recdef_plugin.cma
 FOCMA:=plugins/firstorder/ground_plugin.cma
 CCCMA:=plugins/cc/cc_plugin.cma
-SUBTACCMA:=plugins/subtac/subtac_plugin.cma
 BTAUTOCMA:=plugins/btauto/btauto_plugin.cma
 RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
 NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
@@ -199,13 +198,13 @@ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
         $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
         $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
-        $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
+        $(CCCMA)  $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
         $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
 
 ifneq ($(HASNATDYNLINK),false)
  STATICPLUGINS:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
-	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA)
+	$(XMLCMA) $(FUNINDCMA) $(NATSYNTAXCMA)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  PLUGINS:=$(PLUGINSCMA)
  PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index c38d4186f..15babb2ab 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -100,6 +100,7 @@ let map_named_val f (ctxt,ctxtv) =
 let empty_named_context = empty_named_context
 
 let push_named = push_named
+let push_named_context = List.fold_right push_named
 let push_named_context_val = push_named_context_val
 
 let val_of_named_context ctxt =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 42100e4eb..70369ae4c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -81,6 +81,7 @@ val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
 val push_named : named_declaration -> env -> env
+val push_named_context : named_context -> env -> env
 val push_named_context_val  :
     named_declaration -> named_context_val -> named_context_val
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a52903df0..9b66cacb1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -80,7 +80,9 @@ GEXTEND Gram
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ g = gallina; "." -> g
+    [ [ IDENT "Program"; g = gallina; "." -> program_flag := true; g
+      | IDENT "Program"; g = gallina_ext; "." -> program_flag := true; g
+      | g = gallina; "." -> g
       | g = gallina_ext; "." -> g
       | c = command; "." -> c
       | c = syntax; "." -> c
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 449dcd20e..31814b141 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 f6500f74d..bb59a5c9c 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 0bde8dca9..000000000
--- 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 4812fe0a6..000000000
--- 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 27de89f67..000000000
--- 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 ffcd40f94..000000000
--- 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 32d484091..000000000
--- 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 75d0f3429..000000000
--- 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 5b8636a12..000000000
--- 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 33560995d..000000000
--- 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 72549a011..000000000
--- 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 f07bbeb43..000000000
--- 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 c65203075..000000000
--- 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_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
deleted file mode 100644
index c932a7171..000000000
--- 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 f64c1ae2f..000000000
--- 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 e999f1710..000000000
--- 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 8f56bf52c..000000000
--- 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 5cbb307db..000000000
--- 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 e3dbd127f..000000000
--- 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 2cea0841d..000000000
--- 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 01e2d75f3..000000000
--- 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 7e0755d57..000000000
--- 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 97c3d9414..000000000
--- 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 9ae110881..000000000
--- 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 4f938f4f8..000000000
--- 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 aaefd8cc5..000000000
--- 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 90ae8bae8..000000000
--- 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 5ccc154af..000000000
--- 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
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 9c600b01e..9f44d4fef 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -141,5 +141,5 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
 
   Next Obligation. destruct y ; intuition eauto. Defined.
 
-  Solve Obligations using unfold equiv, complement in * ; 
+  Solve Obligations with unfold equiv, complement in * ; 
     program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d9e9fe257..afdfb4cec 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -105,13 +105,15 @@ Section Respecting.
   (** Here we build an equivalence instance for functions which relates respectful ones only,
      we do not export it. *)
 
-  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type :=
+  Definition respecting `(eqa : Equivalence A (R : relation A), 
+                          eqb : Equivalence B (R' : relation B)) : Type :=
     { morph : A -> B | respectful R R' morph morph }.
 
   Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
-    Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+    Equivalence (fun (f g : respecting eqa eqb) => 
+                   forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
-  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
+  Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8e491b1b8..e0d7a3d7a 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -224,7 +224,7 @@ Hint Extern 4 (subrelation (inverse _) _) =>
   class_apply @subrelation_symmetric : typeclass_instances.
 
 (** The complement of a relation conserves its proper elements. *)
-
+Set Printing All.
 Program Definition complement_proper
   `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
   Proper (RA ==> RA ==> iff) (complement R) := _.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 6708220ea..a090d2007 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B))
       else in_right
     else in_right.
 
-  Solve Obligations using unfold complement ; program_simpl.
+  Solve Obligations with unfold complement ; program_simpl.
 
 (** Objects of function spaces with countable domains like bool
   have decidable equality. *)
@@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A))
       else in_right
     else in_right.
 
-  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+  Solve Obligations with try red ; unfold equiv, complement ; program_simpl.
 
   Next Obligation.
   Proof.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 2e2eb166d..6d0315b82 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
 
-  Global Program Instance eqk_equiv : Equivalence eq_key.
-  Global Program Instance eqke_equiv : Equivalence eq_key_elt.
-  Global Program Instance ltk_strorder : StrictOrder lt_key.
+  Global Instance eqk_equiv : Equivalence eq_key := _.
+  Global Instance eqke_equiv : Equivalence eq_key_elt := _.
+  Global Instance ltk_strorder : StrictOrder lt_key := _.
 
   Lemma mem_find :
     forall m x, mem x m = match find x m with None => false | _ => true end.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e929c561c..4b3c1b4fb 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -21,7 +21,6 @@ Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
 Declare ML Module "dp_plugin".
 Declare ML Module "recdef_plugin".
-Declare ML Module "subtac_plugin".
 Declare ML Module "xml_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_admitted" "_subproof" "Private_".
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index ca4002d7f..dda0ed68d 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -79,14 +79,14 @@ Qed.
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
    in tactics. *)
 
-Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
+Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
   fn (exist _ x eq_refl).
 
 (* This is what we want to be able to do: replace the originaly matched object by a new,
    propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
 
-Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B)
-  (y : A | y = x),
+Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
+  (y : {y:A | y = x}),
   match_eq A B x fn = fn y.
 Proof.
   intros.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index a823aedd3..ee0a7451b 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -35,11 +35,11 @@ Section Well_founded.
   Hypothesis
     F_ext :
     forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
-      (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g.
+      (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
 
   Lemma Fix_F_eq :
     forall (x:A) (r:Acc R x),
-      F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
+      F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
   Proof.
     destruct r using Acc_inv_dep; auto.
   Qed.
@@ -50,7 +50,7 @@ Section Well_founded.
     rewrite (proof_irrelevance (Acc R x) r s) ; auto.
   Qed.
 
-  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)).
+  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)).
   Proof.
     intro x; unfold Fix_sub in |- *.
     rewrite <- (Fix_F_eq ).
@@ -62,7 +62,7 @@ Section Well_founded.
     forall x : A,
       Fix_sub x =
       let f_sub := F_sub in
-        f_sub x (fun (y : A | R y x) => Fix_sub (`y)).
+        f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)).
     exact Fix_eq.
   Qed.
 
@@ -231,10 +231,10 @@ Module WfExtensionality.
   Program Lemma fix_sub_eq_ext :
     forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
       (P : A -> Type)
-      (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
-          F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y).
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y).
   Proof.
     intros ; apply Fix_eq ; auto.
     intros.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2f1b7138b..ceaab3d0f 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -172,7 +172,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   let env' = push_rel_context ctx env in
   evars := Evarutil.nf_evar_map !evars;
   evars := mark_resolvables !evars;
-  evars := resolve_typeclasses env !evars;
+  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
     if abstract then
@@ -190,52 +190,58 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
             (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None global imps ?hook (ConstRef cst); id
       end
-    else
-      begin
-	let props =
-	  match props with
-	  | Some (CRecord (loc, _, fs)) ->
-	      if List.length fs > List.length k.cl_props then
-		mismatched_props env' (List.map snd fs) k.cl_props;
-	      Some (Inl fs)
-	  | Some t -> Some (Inr t)
-	  | None -> None
-	in
-	let subst =
-	  match props with
-	  | None -> if k.cl_props = [] then Some (Inl subst) else None
-	  | Some (Inr term) ->
-	      let c = interp_casted_constr_evars evars env' term cty in
-		Some (Inr (c, subst))
-	  | Some (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
-		  Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst))
-	in	  
+    else (
+      let props =
+	match props with
+	| Some (CRecord (loc, _, fs)) ->
+	    if List.length fs > List.length k.cl_props then
+	      mismatched_props env' (List.map snd fs) k.cl_props;
+	    Some (Inl fs)
+	| Some t -> Some (Inr t)
+	| None -> 
+	    if Flags.is_program_mode () then Some (Inl [])
+	    else None
+      in
+      let subst =
+	match props with
+	| None -> if k.cl_props = [] then Some (Inl subst) else None
+	| Some (Inr term) ->
+	    let c = interp_casted_constr_evars evars env' term cty in
+	      Some (Inr (c, subst))
+	| Some (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
+		Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') 
+			     k.cl_props props subst))
+      in	  
 	evars := Evarutil.nf_evar_map !evars;
 	let term, termtype =
 	  match subst with
@@ -258,23 +264,42 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	let termtype = Evarutil.nf_evar !evars termtype in
 	let term = Option.map (Evarutil.nf_evar !evars) term in
 	let evm = undefined_evars !evars in
-	Evarutil.check_evars env Evd.empty !evars termtype;
+	  Evarutil.check_evars env Evd.empty !evars termtype;
 	  if Evd.is_empty evm && term <> None then
 	    declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
 	  else begin
 	    evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	      Flags.silently (fun () ->
-		Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook);
-		if term <> None then 
-		  Pfedit.by (!refine_ref (evm, Option.get term))
-		else if Flags.is_auto_intros () then
-		  Pfedit.by (Refiner.tclDO len Tactics.intro);
-		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
-	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
-	      id
-	  end
-      end
+	      if Flags.is_program_mode () then
+		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 obls, constr, typ =
+		  match term with 
+		  | Some t -> 
+		      let obls, _, constr, typ = 
+			Obligations.eterm_obligations env id !evars evm 0 t termtype
+		      in obls, Some constr, typ
+		  | None -> [||], None, termtype
+		in
+		  ignore (Obligations.add_definition id ?term:constr
+			    typ ~kind:(Global,Instance) ~hook obls);
+		  id
+	      else
+		(Flags.silently 
+		   (fun () ->
+		      Lemmas.start_proof id kind termtype
+			(fun _ -> instance_hook k pri global imps ?hook);
+		      if term <> None then 
+			Pfedit.by (!refine_ref (evm, Option.get term))
+		      else if Flags.is_auto_intros () then
+			Pfedit.by (Refiner.tclDO len Tactics.intro);
+		      (match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+		 Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
+		 id)
+	  end)
 	
 let named_of_rel_context l =
   let acc, ctx =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 82ec85b7a..0b4e9daa1 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -75,7 +75,6 @@ let interp_definition bl red_option c ctypopt =
       None ->
 	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
-	check_evars env Evd.empty !evdref body;
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
           const_entry_secctx = None;
@@ -86,15 +85,19 @@ let interp_definition bl red_option c ctypopt =
 	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
-	check_evars env Evd.empty !evdref body;
-	check_evars env Evd.empty !evdref typ;
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
           const_entry_secctx = None;
 	  const_entry_type = Some typ;
           const_entry_opaque = false }
   in
-  red_constant_entry (rel_context_length ctx) ce red_option, imps
+  red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
+
+let check_definition (ce, evd, imps) =
+  let env = Global.env () in
+    check_evars env Evd.empty evd ce.const_entry_body;
+    Option.iter (check_evars env Evd.empty evd) ce.const_entry_type;
+    ce
 
 let declare_global_definition ident ce local k imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in
@@ -127,6 +130,25 @@ let declare_definition ident (local,k) ce imps hook =
         declare_global_definition ident ce local k imps in
   hook local r
 
+let _ = Obligations.declare_definition_ref := declare_definition
+
+let do_definition ident k bl red_option c ctypopt hook =
+  let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in
+    if Flags.is_program_mode () then
+      let env = Global.env () in
+      let c = ce.const_entry_body in
+      let typ = match ce.const_entry_type with 
+	| Some t -> t
+	| None -> Retyping.get_type_of env evd c
+      in 
+      let evm = Obligations.non_instanciated_map env (ref evd) evd in
+      let obls, _, c, cty = 
+	Obligations.eterm_obligations env ident evd evm 0 c typ
+      in
+	ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
+    else let ce = check_definition def in
+      declare_definition ident k ce imps hook
+
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
 let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
@@ -488,6 +510,8 @@ let declare_fix kind f def t imps =
   maybe_declare_manual_implicits false gr imps;
   gr
 
+let _ = Obligations.declare_fix_ref := declare_fix
+
 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
@@ -522,15 +546,18 @@ let tactics_module = subtac_dir @ ["Tactics"]
 let init_reference dir s () = Coqlib.gen_reference "Command" dir s
 let init_constant dir s () = Coqlib.gen_constant "Command" dir s
 let make_ref l s = init_reference l s
+let fix_proto = init_constant tactics_module "fix_proto"
 let fix_sub_ref = make_ref fixsub_module "Fix_sub"
 let measure_on_R_ref = make_ref fixsub_module "MR"
 let well_founded = init_constant ["Init"; "Wf"] "well_founded"
 let mkSubset name typ prop =
   mkApp ((delayed_force build_sigma).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
-
 let sigT = Lazy.lazy_from_fun build_sigma_type
 
+let make_qref s = Qualid (dummy_loc, qualid_of_string s)
+let lt_ref = make_qref "Init.Peano.lt"
+
 let rec telescope = function
   | [] -> assert false
   | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
@@ -691,7 +718,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let evars, _, evars_def, evars_typ = 
     Obligations.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp 
   in
-    Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook
+    ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook)
 
 
 let interp_recursive isfix fixl notations =
@@ -705,7 +732,20 @@ let interp_recursive isfix fixl notations =
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
-  let env_rec = push_named_types env fixnames fixtypes in
+  let rec_sign =
+    List.fold_left2 
+      (fun env' id t ->
+	 if Flags.is_program_mode () then
+	   let sort = Retyping.get_type_of env !evdref t in
+	   let fixprot =
+	     try mkApp (delayed_force fix_proto, [|sort; t|])
+	     with e -> t
+	   in
+	     (id,None,fixprot) :: env'
+	 else (id,None,t) :: env')
+      [] fixnames fixtypes
+  in
+  let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
   let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
@@ -722,20 +762,23 @@ let interp_recursive isfix fixl notations =
   let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
   let fixtypes = List.map (nf_evar evd) fixtypes in
   let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
+
+  (* Build the fix declaration block *)
+  (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
+
+let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
-  List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs;
+  List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
   if not (List.mem None fixdefs) then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env isfix (List.combine fixnames fixdefs)
   end;
+  ((fixnames,fixdefs,fixtypes),info)
 
-  (* Build the fix declaration block *)
-  (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
-
-let interp_fixpoint = interp_recursive true
-let interp_cofixpoint = interp_recursive false
-
+let interp_fixpoint l ntns = check_recursive true (interp_recursive true l ntns)
+let interp_cofixpoint l ntns = check_recursive false (interp_recursive false l ntns)
+    
 let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
@@ -803,7 +846,93 @@ let extract_cofixpoint_components l =
     {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
+let check_program_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) = Evd.evar_source evk evd in
+	      (match k with
+	      | Evd.QuestionMark _
+	      | Evd.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 do_program_recursive fixkind fixl ntns =
+  let isfix = fixkind <> Obligations.IsCoFixpoint in
+  let (env, rec_sign, evd), fix, info = 
+    interp_recursive isfix fixl ntns 
+  in
+    (* Program-specific code *)
+    (* Get the interesting evars, those that were not instanciated *)
+  let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd 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 evars, _, def, typ = 
+      Obligations.eterm_obligations env id evd (Evd.undefined_evars evd)
+	(List.length rec_sign) 
+	(nf_evar evd def) (nf_evar evd typ)
+    in (id, def, typ, imps, evars)
+  in
+  let (fixnames,fixdefs,fixtypes) = fix in
+  let fiximps = List.map pi2 info in
+  let fixdefs = List.map Option.get fixdefs in
+  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
+    if isfix then begin
+      let possible_indexes = List.map compute_possible_guardness_evidences info 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)) fixl
+    end;
+    Obligations.add_mutual_definitions defs ntns fixkind
+
+let do_program_fixpoint l =
+  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+    match g, l with
+    | [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+	let recarg = 
+	  match n with
+	  | Some n -> mkIdentC (snd n)
+	  | None ->
+	      errorlabstrm "do_program_fixpoint"
+		(str "Recursive argument required for well-founded fixpoints")
+	in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
+	     
+    | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
+	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,ntns = extract_fixpoint_components true l in
+	let fixkind = Obligations.IsFixpoint g in
+	  do_program_recursive fixkind fixl ntns
+
+    | _, _ ->
+	errorlabstrm "do_program_fixpoint"
+	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+
 let do_fixpoint l =
+  if Flags.is_program_mode () then do_program_fixpoint l else
   let fixl,ntns = extract_fixpoint_components true l in
   let fix = interp_fixpoint fixl ntns in
   let possible_indexes =
@@ -812,4 +941,8 @@ let do_fixpoint l =
 
 let do_cofixpoint l =
   let fixl,ntns = extract_cofixpoint_components l in
-  declare_cofixpoint (interp_cofixpoint fixl ntns) ntns
+    if Flags.is_program_mode () then
+      do_program_recursive Obligations.IsCoFixpoint fixl ntns
+    else
+      let cofix = interp_cofixpoint fixl ntns in
+	declare_cofixpoint cofix ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 0adc66d56..3cced65f1 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -32,11 +32,15 @@ val set_declare_assumptions_hook : (types -> unit) -> unit
 
 val interp_definition :
   local_binder list -> red_expr option -> constr_expr ->
-  constr_expr option -> definition_entry * Impargs.manual_implicits
+  constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
-val declare_definition : identifier -> locality * definition_object_kind ->
+val declare_definition : identifier -> definition_kind ->
   definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a
 
+val do_definition : identifier -> definition_kind ->
+  local_binder list -> red_expr option -> constr_expr ->
+  constr_expr option -> unit declaration_hook -> unit
+
 (** {6 Parameters/Assumptions} *)
 
 val interp_assumption :
diff --git a/plugins/subtac/subtac_obligations.ml b/toplevel/obligations.ml
index 527c5e084..ae25b4fde 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/toplevel/obligations.ml
@@ -1,9 +1,6 @@
 open Printf
 open Pp
-open Subtac_utils
-open Command
 open Environ
-
 open Term
 open Names
 open Libnames
@@ -18,6 +15,289 @@ open Declare
 open Proof_type
 open Compat
 
+(**
+   - 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 Proof_type
+
+let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
+let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
+
+let trace s =
+  if !Flags.debug then (msgnl s; msgerr s)
+  else ()
+
+let succfix (depth, fixrels) =
+  (succ depth, List.map succ fixrels)
+
+let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
+
+let non_instanciated_map env evd evm =
+  List.fold_left
+    (fun evm (key, evi) ->
+       let (loc,k) = evar_source key !evd in
+	 match k with
+	 | QuestionMark _ -> Evd.add evm key evi
+	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
+	 | _ ->
+	     Pretype_errors.error_unsolvable_implicit loc env
+	       evm (Evarutil.nf_evar_info evm evi) k None)
+    Evd.empty (Evarutil.non_instantiated evm)
+
+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 tactics_module = ["Program";"Tactics"]
+let safe_init_constant md name () =
+  Coqlib.check_required_library ("Coq"::md);
+  Coqlib.gen_constant "Obligations" md name
+let fix_proto = safe_init_constant tactics_module "fix_proto"
+let hide_obligation = safe_init_constant tactics_module "obligation"
+
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Errors.errorlabstrm "Program" cmd
 let error s = pperror (str s)
@@ -63,7 +343,7 @@ type program_info = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : Tacexpr.declaration_hook;
+  prg_hook : unit Tacexpr.declaration_hook;
 }
 
 let assumption_message id =
@@ -211,10 +491,11 @@ 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"))
+      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
@@ -246,38 +527,15 @@ let subst_body expand 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
+    progmap_remove prg;
+    !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits
+      (fun local gr -> prg.prg_hook local gr; gr)
 
 open Pp
 open Ppconstr
@@ -331,7 +589,7 @@ let declare_mutual_definition l =
 	  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
+  let kns = list_map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
     Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
@@ -359,7 +617,7 @@ let declare_obligation prg obl body =
 	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);
+	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 =
@@ -380,7 +638,8 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	      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_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; }
 
@@ -455,10 +714,19 @@ let dependencies obls n =
       obls;
     !res
 
+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
+
 let kind_of_opacity o =
   match o with
-  | Define false | Expand -> Subtac_utils.goal_kind
-  | _ -> Subtac_utils.goal_proof_kind
+  | Define false | Expand -> goal_kind
+  | _ -> goal_proof_kind
 
 let not_transp_msg =
   str "Obligation should be transparent but was declared opaque." ++ spc () ++
@@ -467,6 +735,27 @@ let not_transp_msg =
 let warn_not_transp () = ppwarn not_transp_msg
 let error_not_transp () = pperror not_transp_msg
 
+let rec string_of_list sep f = function
+    [] -> ""
+  | x :: [] -> f x
+  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
+
+(* 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 rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
@@ -508,12 +797,12 @@ let rec solve_obligation prg num tac =
 			  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);
+		     Printer.pr_constr_env (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))
+		      ++ 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
@@ -543,7 +832,7 @@ and solve_obligation_by_tac prg obls i tac =
 		  | Some t -> t
 		  | None -> snd (get_default_tactic ())
 	    in
-	    let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
+	    let t = solve_by_tac (evar_of_obligation obl) tac in
 	      obls.(i) <- declare_obligation prg obl t;
 	      true
 	  else false
@@ -605,7 +894,8 @@ let show_obligations_of_prg ?(msg=true) prg =
 			 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 ())))
+				   hov 1 (Printer.pr_constr_env (Global.env ()) x.obl_type ++ 
+					    str "." ++ fnl ())))
 		   | Some _ -> ())
       obls
 
@@ -621,8 +911,8 @@ 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)
+	     Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
 
 let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
     ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
@@ -656,7 +946,9 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
 	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
+	    | Defined _ -> 
+		(* If one definition is turned into a constant, 
+		   the whole block is defined. *) true
 	    | _ -> false)
 	false deps
     in ()
diff --git a/plugins/subtac/subtac_obligations.mli b/toplevel/obligations.mli
index 284e975db..de020f8e3 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/toplevel/obligations.mli
@@ -1,10 +1,55 @@
+(************************************************************************)
+(*  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
 open Libnames
-open Evd
 open Proof_type
 open Vernacexpr
+open Decl_kinds
+open Tacexpr
+
+(** Forward declaration. *)
+val declare_fix_ref : (definition_object_kind -> identifier ->
+  constr -> types -> Impargs.manual_implicits -> global_reference) ref
+
+val declare_definition_ref :
+  (identifier -> locality * definition_object_kind ->
+     Entries.definition_entry -> Impargs.manual_implicits
+       -> global_reference declaration_hook -> global_reference) ref
+
+val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map
+
+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 *)
 
 type obligation_info =
   (identifier * Term.types * hole_kind located *
@@ -29,7 +74,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
+  ?hook:(unit Tacexpr.declaration_hook) -> obligation_info -> progress
 
 type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
 
@@ -43,7 +88,7 @@ val add_mutual_definitions :
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:Tacexpr.declaration_hook ->
+  ?hook:unit Tacexpr.declaration_hook ->
   notations ->
   fixpoint_kind -> unit
 
@@ -70,4 +115,3 @@ 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/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 7d891997b..2ca2f0739 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -17,6 +17,7 @@ Ppvernac
 Vernacinterp
 Mltop
 Vernacentries
+G_obligations
 Whelp
 Vernac
 Ide_intf
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7a7246733..20c9531fe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -343,8 +343,7 @@ let vernac_definition (local,k) (loc,id as lid) def hook =
           | Some r ->
 	      let (evc,env)= get_current_context () in
  		Some (interp_redexp env evc r) in
-	let ce,imps = interp_definition bl red_option c typ_opt in
-	declare_definition id (local,k) ce imps hook)
+	do_definition id (local,k) bl red_option c typ_opt hook)
 
 let vernac_start_proof kind l lettop hook =
   if Dumpglob.dump () then
@@ -1578,5 +1577,12 @@ let interp c = match c with
   (* Extensions *)
   | VernacExtend (opn,args) -> Vernacinterp.call (opn,args)
 
-let interp c = interp c ; check_locality ()
+let interp c = 
+  let mode = Flags.is_program_mode () in
+  let flag = mode || !program_flag in
+    Flags.program_mode := flag;
+    interp c; check_locality ();
+    program_flag := false;
+    Flags.program_mode := mode
+  (* with_program_flag (fun () -> interp c ; check_locality ()) *)
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 31d04fcfa..e49cd3b66 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -128,7 +128,8 @@ type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
 type locality_flag  = bool (* true = Local;         false = Global         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
-type instance_flag  = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
+type instance_flag  = bool option
+  (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type inductive_flag = Decl_kinds.recursivity_kind
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
@@ -481,3 +482,16 @@ let enforce_module_locality local =
 
 (**********************************************************************)
 
+(**********************************************************************)
+(* Managing the Program extension. *)
+
+let program_flag = ref false
+let with_program_flag m = 
+  if Flags.is_program_mode () then
+    (program_flag := false; m ())
+  else if !program_flag then 
+    (Flags.program_mode := true; 
+     m ();
+     Flags.program_mode := false;
+     program_flag := false)
+