Remove non-DFSG contentsupstream/8.4_beta+dfsg

18 files changed, 353 insertions, 327 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 3fb6824b..5ed335d0 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
@@ -28,11 +27,15 @@ type oblinfo =
     ev_hyps: named_context;
     ev_status: obligation_definition_status;
     ev_chop: int option;
-    ev_source: hole_kind located;
+    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. *)
 
@@ -210,7 +213,7 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	   | Some s -> s, None
 	   | None -> Define true, None
 	 in
-	 let tac = match ev.evar_extra with
+	 let tac = match evar_tactic.get ev.evar_extra with
 	   | Some t ->
 	       if Dyn.tag t = "tactic" then
 		 Some (Tacinterp.interp 
@@ -218,9 +221,9 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	       else None
 	   | None -> None
 	 in
-	 let info = { ev_name = (n, nstr); ev_hyps = hyps; 
-		      ev_status = status; ev_chop = chop;
-		      ev_source = (loc, k); ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
+	 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
@@ -231,12 +234,12 @@ let eterm_obligations env name isevars evm fs ?status t ty =
   let evars = 
     List.map (fun (ev, info) ->
       let { ev_name = (_, name); ev_status = status;
-	    ev_source = source; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+	    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, source, status, deps, tac) evts
+      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
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index b4bbe3d5..03d76f29 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -1,12 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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 $Id: eterm.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 open Environ
 open Tacmach
 open Term
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ce6d12be..ca1240e5 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -1,21 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
 
 (*
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
 
-(* $Id: g_subtac.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 
 open Flags
 open Util
@@ -37,14 +33,14 @@ module Tactic = Pcoq.Tactic
 
 module SubtacGram =
 struct
-  let gec s = Gram.Entry.create ("Subtac."^s)
+  let gec s = Gram.entry_create ("Subtac."^s)
 		(* types *)
-  let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+  let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc"
 
-  let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac"
+  let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac"
 end
 
-open Rawterm
+open Glob_term
 open SubtacGram
 open Util
 open Pcoq
@@ -94,7 +90,7 @@ VERNAC COMMAND EXTEND Subtac
 
 let try_catch_exn f e =
   try f e
-  with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn)
+  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
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 95cacc38..710149ae 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -1,13 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
+open Compat
 open Global
 open Pp
 open Util
@@ -27,7 +26,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 open Vernacexpr
@@ -50,7 +49,7 @@ open Tacinterp
 open Tacexpr
 
 let solve_tccs_in_type env id isevars evm c typ =
-  if not (evm = Evd.empty) then
+  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
@@ -89,7 +88,7 @@ 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 -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+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")
@@ -142,12 +141,12 @@ let subtac (loc, command) =
 	    (fun _ _ -> ())
       | DefineBody (bl, _, c, tycon) ->
 	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
-  | VernacFixpoint (l, b) ->
+  | 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 b)
+	ignore(Subtac_command.build_recursive l)
 
   | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
       if guard <> None then 
@@ -172,10 +171,10 @@ let subtac (loc, command) =
 	error "Declare Instance not supported here.";
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
-  | VernacCoFixpoint (l, b) ->
+  | VernacCoFixpoint l ->
       if Dumpglob.dump () then
 	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
-      ignore(Subtac_command.build_corecursive l b)
+      ignore(Subtac_command.build_corecursive l)
 
   (*| VernacEndProof e ->
     subtac_end_proof e*)
@@ -219,6 +218,11 @@ let subtac (loc, command) =
 
   | Type_errors.TypeError (env, exn) as e -> raise e
 
-  | Pretype_errors.PretypeError (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 -> raise e
+  | e -> 
+      (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
+      raise e
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 25aec39c..368d8bac 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Cases
 open Util
 open Names
@@ -23,7 +20,7 @@ open Sign
 open Reductionops
 open Typeops
 open Type_errors
-open Rawterm
+open Glob_term
 open Retyping
 open Pretype_errors
 open Evarutil
@@ -89,7 +86,7 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
 type rhs =
     { rhs_env    : env;
       avoid_ids  : identifier list;
-      it         : rawconstr;
+      it         : glob_constr;
     }
 
 type equation =
@@ -158,22 +155,22 @@ let feed_history arg = function
 
 (* This is for non exhaustive error message *)
 
-let rec rawpattern_of_partial_history args2 = function
+let rec glob_pattern_of_partial_history args2 = function
   | Continuation (n, args1, h) ->
       let args3 = make_anonymous_patvars (n - (List.length args2)) in
-      build_rawpattern (List.rev_append args1 (args2@args3)) h
+      build_glob_pattern (List.rev_append args1 (args2@args3)) h
   | Result pl -> pl
 
-and build_rawpattern args = function
+and build_glob_pattern args = function
   | Top -> args
   | MakeAlias (AliasLeaf, rh) ->
       assert (args = []);
-      rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
+      glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
   | MakeAlias (AliasConstructor pci, rh) ->
-      rawpattern_of_partial_history
+      glob_pattern_of_partial_history
 	[PatCstr (dummy_loc, pci, args, Anonymous)] rh
 
-let complete_history = rawpattern_of_partial_history []
+let complete_history = glob_pattern_of_partial_history []
 
 (* This is to build glued pattern-matching history and alias bodies *)
 
@@ -237,7 +234,7 @@ type pattern_matching_problem =
       mat      : matrix;
       caseloc  : loc;
       casestyle: case_style;
-      typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
+      typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -369,10 +366,10 @@ let find_tomatch_tycon isevars env loc = function
   | None -> empty_tycon
 
 let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
-  let loc = Some (loc_of_rawconstr tomatch) in
+  let loc = Some (loc_of_glob_constr tomatch) in
   let tycon = find_tomatch_tycon isevars env loc indopt in
   let j = typing_fun tycon env tomatch in
-  let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
+  let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in
   isevars := evd;
   let typ = nf_evar ( !isevars) j.uj_type in
   let t =
@@ -530,7 +527,7 @@ let extract_rhs pb =
 let occur_in_rhs na rhs =
   match na with
     | Anonymous -> false
-    | Name id -> occur_rawconstr id rhs.it
+    | Name id -> occur_glob_constr id rhs.it
 
 let is_dep_patt eqn = function
   | PatVar (_,name) -> occur_in_rhs name eqn.rhs
@@ -604,7 +601,7 @@ let regeneralize_index_tomatch n =
   genrec 0
 
 let rec replace_term n c k t =
-  if t = mkRel (n+k) then lift k c
+  if isRel t && destRel t = n+k then lift k c
   else map_constr_with_binders succ (replace_term n c) k t
 
 let replace_tomatch n c =
@@ -1518,7 +1515,7 @@ let mk_JMeq typ x typ' y =
   mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
 
-let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
+let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
 let constr_of_pat env isevars arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
@@ -1534,7 +1531,7 @@ let constr_of_pat env isevars arsign pat avoid =
     | PatCstr (l,((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
 	let IndType (indf, _) = 
-	  try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) 
+	  try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty)
 	  with Not_found -> error_case_not_inductive env 
 	    {uj_val = ty; uj_type = Typing.type_of env !isevars ty}
 	in
@@ -1548,7 +1545,7 @@ let constr_of_pat env isevars arsign pat avoid =
 	  List.fold_right2
 	    (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid)  ->
 	       let pat', sign', arg', typ', argtypargs, n', avoid =
-		 typ env (lift (n - m) t, []) ua avoid
+		 typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid
 	       in
 	       let args' = arg' :: List.map (lift n') args in
 	       let env' = push_rels sign' env in
@@ -1607,12 +1604,12 @@ let vars_of_ctx ctx =
       match b with
 	| Some t' when kind_of_term t' = Rel 0 ->
 	    prev,
-	    (RApp (dummy_loc,
-		(RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+	    (GApp (dummy_loc,
+		(GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars
 	| _ ->
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
-	      | Name n -> n, RVar (dummy_loc, n) :: vars)
+	      | Name n -> n, GVar (dummy_loc, n) :: vars)
       ctx (id_of_string "vars_of_ctx_error", [])
   in List.rev y
 
@@ -1744,13 +1741,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
-	   let bref = RVar (dummy_loc, branch_name) in
+	   let bref = GVar (dummy_loc, branch_name) in
 	     match vars_of_ctx rhs_rels with
 		 [] -> bref
-	       | l -> RApp (dummy_loc, bref, l)
+	       | l -> GApp (dummy_loc, bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> RApp (dummy_loc, branch, [ hole ])
+	     Some _ -> GApp (dummy_loc, branch, [ hole ])
 	   | None -> branch
 	 in
 	 incr i;
@@ -1786,7 +1783,7 @@ let abstract_tomatch env tomatchs tycon =
 	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
 	   | _ ->
 	       let tycon = Option.map
-		 (fun t -> subst_term_occ all_occurrences (lift 1 c) (lift 1 t)) tycon in
+		 (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in
 	       let name = next_ident_away (id_of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index bc2b2bb7..77537d33 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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 $Id: subtac_cases.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*i*)
 open Util
 open Names
@@ -15,7 +13,7 @@ open Term
 open Evd
 open Environ
 open Inductiveops
-open Rawterm
+open Glob_term
 open Evarutil
 (*i*)
 
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 960bf162..c08dd16d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -1,19 +1,16 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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 $Id: subtac_classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pretyping
 open Evd
 open Environ
 open Term
-open Rawterm
+open Glob_term
 open Topconstr
 open Names
 open Libnames
@@ -23,24 +20,28 @@ open Constrintern
 open Subtac_command
 open Typeclasses
 open Typeclasses_errors
-open Termops
 open Decl_kinds
 open Entries
 open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
 
-let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
+let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c =
   SPretyping.understand_tcc_evars evdref env kind
-    (intern_gen (kind=IsType) ~impls ( !evdref) env c)
+    (intern_gen (kind=IsType) ~impls !evdref env c)
 
-let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
+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 =
-  Constrintern.interp_context_gen
+  let impls_env, bl = Constrintern.interp_context_gen
     (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t)
-    (SPretyping.understand_judgment_tcc evdref) !evdref env params
+    (SPretyping.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
+    SPretyping.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
@@ -113,11 +114,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let subst = List.map (Evarutil.nf_evar sigma) subst in
   let props =
     match props with
-    | CRecord (loc, _, fs) ->
+    | 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
-    | _ -> Inr props
+    | Some p -> Inr p
+    | None -> Inl []
   in
   let subst =
     match props with
@@ -138,7 +140,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		  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
-		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+		    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 (Util.dummy_loc, None) :: props), rest
@@ -173,10 +179,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   Evarutil.check_evars env Evd.empty !evars termtype;
   let hook vis gr =
     let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-    let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
       Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-      Typeclasses.add_instance inst
+      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,false,Instance) ~hook obls
+    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
index 73ca5581..5b5c0203 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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 $Id: subtac_classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*i*)
 open Names
 open Decl_kinds
@@ -35,7 +33,7 @@ val new_instance :
   ?global:bool ->
   local_binder list ->
   typeclass_constraint ->
-  constr_expr ->
+  constr_expr option ->
   ?generalize:bool ->
   int option ->
   identifier * Subtac_obligations.progress
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index bdebdf85..74f31a90 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -1,13 +1,10 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Term
@@ -144,7 +141,7 @@ module Coercion = struct
 		let restargs = lift_args 1
 		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
 		in
-		let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
+		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
 		let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in
 		let evar = make_existential loc env isevars eq in
@@ -205,7 +202,7 @@ module Coercion = struct
 				 | Lambda (n, t, t') -> c, t'
 				     (*| Prod (n, t, t') -> t'*)
 				 | Evar (k, args) ->
-				     let (evs, t) = Evarutil.define_evar_as_lambda !isevars (k,args) in
+				     let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
 				       isevars := evs;
 				       let (n, dom, rng) = destLambda t in
 				       let (domk, args) = destEvar dom in
@@ -330,8 +327,8 @@ module Coercion = struct
   let apply_pattern_coercion loc pat p =
     List.fold_left
       (fun pat (co,n) ->
-	 let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
-	   Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+	 let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
+	   Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
       pat p
 
   (* raise Not_found if no coercion found *)
@@ -411,10 +408,10 @@ module Coercion = struct
     else
     let v', t' =
       try
-	let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
+	let t2,t1,p = lookup_path_between env evd (t,c1) in
 	  match v with
 	      Some v ->
-		let j = apply_coercion env ( evd) p
+		let j = apply_coercion env evd p
 		  {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
@@ -430,8 +427,8 @@ module Coercion = struct
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
-      kind_of_term (whd_betadeltaiota env ( evd) t),
-      kind_of_term (whd_betadeltaiota env ( evd) c1)
+      kind_of_term (whd_betadeltaiota env evd t),
+      kind_of_term (whd_betadeltaiota env evd c1)
     with
     | Prod (name,t1,t2), Prod (_,u1,u2) ->
         (* Conversion did not work, we may succeed with a coercion. *)
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index a83611a4..ecae6759 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -6,7 +6,7 @@ open Libobject
 open Pattern
 open Matching
 open Pp
-open Rawterm
+open Glob_term
 open Sign
 open Tacred
 open Util
@@ -21,7 +21,6 @@ open Tacmach
 open Tactic_debug
 open Topconstr
 open Term
-open Termops
 open Tacexpr
 open Safe_typing
 open Typing
@@ -53,7 +52,7 @@ let evar_nf isevars c =
   Evarutil.nf_evar !isevars c
 
 let interp_gen kind isevars env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(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' = SPretyping.understand_tcc_evars isevars env kind c' in
@@ -62,13 +61,13 @@ let interp_gen kind isevars env
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c
 
-let interp_type_evars isevars env ?(impls=[]) 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=[]) c typ =
+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=[]) c typ =
+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 =
@@ -85,25 +84,25 @@ let interp_constr_judgment isevars env c =
     { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
 
 let locate_if_isevar loc na = function
-  | RHole _ ->
+  | GHole _ ->
       (try match na with
-	| Name id ->  Reserve.find_reserved_type id
+	| Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> RHole (loc, Evd.BinderType na))
+      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
-    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
 
 let interp_context_evars evdref env params =
-  let bl = Constrintern.intern_context false ( !evdref) env params in
+  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_rawconstr t) na t in
+	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
 	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
 	      let d = (na,None,t) in
 	      let impls =
@@ -133,7 +132,7 @@ let collect_non_rec env =
       let i =
         list_try_find_i
           (fun i f ->
-             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+             if List.for_all (fun (_, def) -> not (Termops.occur_var env f def)) ldefrec
              then i else failwith "try_find_i")
           0 lnamerec
       in
@@ -184,11 +183,11 @@ let sigT = Lazy.lazy_from_fun build_sigma_type
 let sigT_info = lazy
   { ci_ind       = destInd (Lazy.force sigT).typ;
     ci_npar      = 2;
-    ci_cstr_nargs = [|2|];
+    ci_cstr_ndecls = [|2|];
     ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
   }
 
-let telescope = function
+let rec telescope = function
   | [] -> assert false
   | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
   | (n, None, t) :: tl ->
@@ -209,13 +208,14 @@ let telescope = function
 	(List.rev tys) tl (mkRel 1, [])
       in ty, ((n, Some last, t) :: subst), constr
 
-  | _ -> raise (Invalid_argument "telescope")
+  | (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 boxed =
+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
@@ -300,11 +300,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
     in
-    let newimpls = [(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)
+    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
@@ -325,10 +325,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
 	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_body = Evarutil.nf_evar !isevars body;
+            const_entry_secctx = None;
 	    const_entry_type = Some ty;
-	    const_entry_opaque = false;
-	    const_entry_boxed = false} 
+	    const_entry_opaque = false }
 	in 
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -417,7 +417,7 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
-let interp_recursive fixkind l boxed =
+let interp_recursive fixkind l =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
   let kind = fixkind <> IsCoFixpoint in
@@ -506,7 +506,7 @@ let out_n = function
     Some n -> n
   | None -> raise Not_found
 
-let build_recursive l b =
+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)] ->
@@ -514,24 +514,24 @@ let build_recursive l b =
 		    (match n with Some n -> mkIdentC (snd n) | None ->
 		      errorlabstrm "Subtac_command.build_recursive"
 			(str "Recursive argument required for well-founded fixpoints"))
-		    ntn false)
+		    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 false)
+		    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 b
+	  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 b =
+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 b
+  interp_recursive IsCoFixpoint fixl
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 0f24915e..72549a01 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -43,7 +43,7 @@ val interp_binder :     Evd.evar_map ref ->
 
 
 val telescope :
-  (Names.name * 'a option * Term.types) list ->
+  (Names.name * Term.types option * Term.types) list ->
   Term.types * (Names.name * Term.types option * Term.types) list *
     Term.constr
 
@@ -51,10 +51,10 @@ val build_wellfounded :
            Names.identifier * 'a * Topconstr.local_binder list *
            Topconstr.constr_expr * Topconstr.constr_expr ->
            Topconstr.constr_expr ->
-           Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
+           Topconstr.constr_expr -> 'b -> Subtac_obligations.progress
 
 val build_recursive :
-  (fixpoint_expr * decl_notation list) list -> bool -> unit
+  (fixpoint_expr * decl_notation list) list -> unit
 
 val build_corecursive :
-  (cofixpoint_expr * decl_notation list) list -> bool -> unit
+  (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d3a63410..64d9f72c 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 open Printf
 open Pp
 open Subtac_utils
@@ -16,6 +15,7 @@ open Util
 open Evd
 open Declare
 open Proof_type
+open Compat
 
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
@@ -30,13 +30,13 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ str (string_of_id ident)
   | None -> str "No obligations remaining"
 
-type obligation_info = (Names.identifier * Term.types * hole_kind located * 
+type obligation_info = (Names.identifier * Term.types * hole_kind located *
 			  obligation_definition_status * Intset.t * tactic option) array
 
 type obligation =
   { obl_name : identifier;
     obl_type : types;
-    obl_source : hole_kind located;
+    obl_location : hole_kind located;
     obl_body : constr option;
     obl_status : obligation_definition_status;
     obl_deps : Intset.t;
@@ -82,11 +82,29 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "transparency of Program obligations";
       optkey   = ["Transparent";"Obligations"];
       optread  = get_proofs_transparency;
       optwrite = set_proofs_transparency; }
 
+(* true = hide obligations *)
+let hide_obligations = ref false
+
+let set_hide_obligations = (:=) hide_obligations
+let get_hide_obligations () = !hide_obligations
+
+open Goptions
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "Hidding of Program obligations";
+      optkey   = ["Hide";"Obligations"];
+      optread  = get_hide_obligations;
+      optwrite = set_hide_obligations; }
+
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
 let get_obligation_body expand obl =
@@ -97,18 +115,54 @@ let get_obligation_body expand obl =
       | _ -> c
     else c
 
+let obl_substitution expand obls deps =
+  Intset.fold
+    (fun x acc ->
+       let xobl = obls.(x) in
+       let oblb =
+	 try get_obligation_body expand xobl
+	 with _ -> assert(false)
+       in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
+    deps []
+
 let subst_deps expand obls deps t =
-  let subst =
-    Intset.fold
-      (fun x acc ->
-	let xobl = obls.(x) in
-	let oblb =
-	  try get_obligation_body expand xobl
-	  with _ -> assert(false)
-	in (xobl.obl_name, oblb) :: acc)
-      deps []
-  in(*  Termops.it_mkNamedProd_or_LetIn t subst *)
-    Term.replace_vars subst t
+  let subst = obl_substitution expand obls deps in
+    Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
+
+let rec prod_app t n =
+  match kind_of_term (strip_outer_cast t) with
+    | Prod (_,_,b) -> subst1 n b
+    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
+    | _ ->
+	errorlabstrm "prod_app"
+	  (str"Needed a product, but didn't find one" ++ fnl ())
+
+
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_applist t nL = List.fold_left prod_app t nL
+
+let replace_appvars subst =
+  let rec aux c = 
+    let f, l = decompose_app c in
+      if isVar f then
+	try
+	  let c' = List.map (map_constr aux) l in
+	  let (t, b) = List.assoc (destVar f) subst in
+	    mkApp (delayed_force hide_obligation, 
+		   [| prod_applist t c'; applistc b c' |])
+	with Not_found -> map_constr aux c
+      else map_constr aux c
+  in map_constr aux
+       
+let subst_prog expand obls ints prg =
+  let subst = obl_substitution expand obls ints in
+    if get_hide_obligations () then
+      (replace_appvars subst prg.prg_body,
+       replace_appvars subst (Termops.refresh_universes prg.prg_type))
+    else 
+      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
+	(Term.replace_vars subst' prg.prg_body,
+	 Term.replace_vars subst' (Termops.refresh_universes prg.prg_type))
 
 let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
@@ -153,20 +207,32 @@ let _ =
 
 let progmap_union = ProgMap.fold ProgMap.add
 
-let (input,output) =
+let close sec =
+  if not (ProgMap.is_empty !from_prg) then
+    let keys = map_keys !from_prg in
+      errorlabstrm "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
+			      prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
+			      (str (if List.length keys = 1 then " has " else "have ") ++
+			       str "unsolved obligations"))
+
+let input : program_info ProgMap.t -> obj =
   declare_object
     { (default_object "Program state") with
-      classify_function = (fun () ->
-	if not (ProgMap.is_empty !from_prg) then
-	  errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
-				     prlist_with_sep spc (fun x -> Nameops.pr_id x)
-				     (map_keys !from_prg));
-	Dispose) }
+      cache_function = (fun (na, pi) -> from_prg := pi);
+      load_function = (fun _ (_, pi) -> from_prg := pi);
+      discharge_function = (fun _ -> close "section"; None);
+      classify_function = (fun _ -> close "module"; Dispose) }
     
 open Evd
 
 let progmap_remove prg =
-  from_prg := ProgMap.remove prg.prg_name !from_prg
+  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
+  
+let progmap_add n prg =
+  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
+
+let progmap_replace prg' = 
+  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
 
 let rec intset_to = function
     -1 -> Intset.empty
@@ -175,21 +241,16 @@ let rec intset_to = function
 let subst_body expand prg =
   let obls, _ = prg.prg_obligations in
   let ints = intset_to (pred (Array.length obls)) in
-    subst_deps expand obls ints prg.prg_body,
-  subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
+    subst_prog expand obls ints prg
 
 let declare_definition prg =
   let body, typ = subst_body true prg in
-    (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
-		  my_print_constr (Global.env()) body ++ str " : " ++
-		  my_print_constr (Global.env()) prg.prg_type);
-     with _ -> ());
-  let (local, boxed, kind) = prg.prg_kind 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;
-      const_entry_boxed = boxed}
+      const_entry_opaque = false }
   in
     (Command.get_declare_definition_hook ()) ce;
     match local with
@@ -207,7 +268,7 @@ let declare_definition prg =
     | (Global|Local) ->
 	let c =
 	  Declare.declare_constant
-	    prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
+	    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
@@ -255,7 +316,7 @@ let declare_mutual_definition l =
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let (local,boxed,kind) = first.prg_kind in
+  let (local,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
   let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
@@ -269,7 +330,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 boxed kind) fixnames fixdecls fixtypes fiximps in
+  let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
     Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
@@ -287,9 +348,9 @@ let declare_obligation prg obl body =
       let opaque = if get_proofs_transparency () then false else opaque in
       let ce = 
 	{ const_entry_body = body;
+          const_entry_secctx = None;
 	  const_entry_type = Some ty;
-	  const_entry_opaque = opaque;
-	  const_entry_boxed = false} 
+	  const_entry_opaque = opaque }
       in
       let constant = Declare.declare_constant obl.obl_name
 	(DefinitionEntry ce,IsProof Property)
@@ -307,14 +368,14 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	assert(obls = [||]);
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
-	       obl_source = (dummy_loc, QuestionMark Expand); obl_type = t;
+	       obl_location = dummy_loc, InternalHole; obl_type = t;
 	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
 	mkVar n
     | Some b ->
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_source = l; obl_type = reduce t; obl_status = o;
+	      obl_location = l; obl_type = reduce t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
@@ -359,7 +420,7 @@ let obligations_message rem =
 
 let update_obls prg obls rem =
   let prg' = { prg with prg_obligations = (obls, rem) } in
-    from_prg := map_replace prg.prg_name prg' !from_prg; 
+    progmap_replace prg';
     obligations_message rem;
     if rem > 0 then Remain rem
     else (
@@ -437,7 +498,7 @@ let rec solve_obligation prg num tac =
 		let obls = Array.copy obls in
 		let _ = obls.(num) <- obl in
 		let res = try update_obls prg obls (pred rem)
-		  with e -> pperror (Cerrors.explain_exn e)
+		  with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
 		in
 		  match res with
 		  | Remain n when n > 0 ->
@@ -485,10 +546,11 @@ and solve_obligation_by_tac prg obls i tac =
 	      true
 	  else false
 	with
-	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
+	| Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+	| Loc.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
-	    user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
+	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+	| Util.Anomaly _ as e -> raise e
 	| e -> false
 
 and solve_prg_obligations prg tac =
@@ -556,7 +618,7 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
     ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
@@ -568,23 +630,20 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
   else (
     let len = Array.length obls in
     let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
-      from_prg := ProgMap.add n prg !from_prg;
+      progmap_add n prg;
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) 
+let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
     ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
-  let upd = List.fold_left
-      (fun acc (n, b, t, imps, obls) ->
-	let prg = init_prog_info n (Some b) t deps (Some fixkind) 
-	  notations obls imps kind reduce hook 
-	in ProgMap.add n prg acc)
-      !from_prg l
-  in
-    from_prg := upd;
+    List.iter
+    (fun  (n, b, t, imps, obls) ->
+     let prg = init_prog_info n (Some b) t deps (Some fixkind) 
+       notations obls imps kind reduce hook 
+     in progmap_add n prg) l;
     let _defined =
       List.fold_left (fun finished x ->
 	if finished then finished
@@ -604,8 +663,8 @@ let admit_obligations n =
 	match x.obl_body with
 	| None ->
             let x = subst_deps_obl obls x in
-	    let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), 
-							 IsAssumption Conjectural) 
+	    let kn = Declare.declare_constant x.obl_name 
+              (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
 	    in
 	      assumption_message x.obl_name;
 	      obls.(i) <- { x with obl_body = Some (mkConst kn) }
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 5f6d1a2e..c1d665aa 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -8,7 +8,7 @@ open Vernacexpr
 type obligation_info =
   (identifier * Term.types * hole_kind located *
       obligation_definition_status * Intset.t * tactic option) array
-    (* ident, type, source, (opaque or transparent, expand or define),
+    (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
 
 type progress = (* Resolution status of a program *)
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 9de7ddf2..7c0d1232 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Global
 open Pp
 open Util
@@ -26,7 +24,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 
@@ -60,13 +58,10 @@ let my_print_rec_info env t =
   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_rawconstr env c) ++ *)
+(*   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 merge_evms x y =
-  Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y
-
 let interp env isevars c tycon =
   let j = pretype tycon env isevars ([],[]) c in
   let _ = isevars := Evarutil.nf_evar_map !isevars in
@@ -86,9 +81,9 @@ let find_with_index x l =
 
 open Vernacexpr
 
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
+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 -> Rawterm.rawconstr = 
+let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = 
   Constrintern.intern_type evd env
 
 let env_with_binders env isevars l =
@@ -119,14 +114,14 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon =
       | 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_rawterm 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_rawterm ~with_products:is_type c
+    | 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
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 48906b23..fa767790 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -13,7 +13,7 @@ module Pretyping : Pretyping.S
 val interp :
     Environ.env ->
     Evd.evar_map ref ->
-    Rawterm.rawconstr ->
+    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 ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 4f4ae92e..d5d427c7 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -1,21 +1,18 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping_F.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
+open Compat
 open Util
 open Names
 open Sign
 open Evd
 open Term
-open Termops
 open Reductionops
 open Environ
 open Type_errors
@@ -27,7 +24,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 open Pretyping
@@ -78,15 +75,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	for i = 0 to lt-1 do
           if not (e_cumul env evdref (vdefj.(i)).uj_type
 		    (lift lt lar.(i))) then
-            error_ill_typed_rec_body_loc loc env ( !evdref)
+            error_ill_typed_rec_body_loc loc env !evdref
               i lna vdefj lar
 	done
 
-  let check_branches_message loc env evdref c (explft,lft) =
+  let check_branches_message loc env evdref ind c (explft,lft) =
     for i = 0 to Array.length explft - 1 do
       if not (e_cumul env evdref lft.(i) explft.(i)) then
 	let sigma =  !evdref in
-	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
+	  error_ill_formed_branch_loc loc env sigma c (ind,i) lft.(i) explft.(i)
     done
 
   (* coerce to tycon if any *)
@@ -99,7 +96,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   (*
     let evar_type_case evdref env ct pt lft p c =
     let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c
-    in check_branches_message evdref env (c,ct) (bty,lft); (mind,rslty)
+    in check_branches_message evdref env mind (c,ct) (bty,lft); (mind,rslty)
   *)
 
   let strip_meta id = (* For Grammar v7 compatibility *)
@@ -108,7 +105,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       else id
 
   let invert_ltac_bound_name env id0 id =
-    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+    try mkRel (pi1 (Termops.lookup_rel_id id (rel_context env)))
     with Not_found ->
       errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
 	str " depends on pattern variable name " ++ pr_id id ++
@@ -117,7 +114,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let pretype_id loc env sigma (lvar,unbndltacvars) id =
     let id = strip_meta id in (* May happen in tactics defined by Grammar *)
       try
-	let (n,_,typ) = lookup_rel_id id (rel_context env) in
+	let (n,_,typ) = Termops.lookup_rel_id id (rel_context env) in
 	  { uj_val  = mkRel n; uj_type = lift n typ }
       with Not_found ->
 	try
@@ -153,7 +150,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     let s' = mkProd (Anonymous, ind, s) in
     let ccl = lift 1 (decomp n pj.uj_val) in
     let ccl' = mkLambda (Anonymous, ind, ccl) in
-      {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
+      {uj_val=Termops.it_mkLambda ccl' sign; uj_type=Termops.it_mkProd s' sign}
 
   (*************************************************************************)
   (* Main pretyping function                                               *)
@@ -162,9 +159,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     let c = constr_of_global ref in
       make_judge c (Retyping.get_type_of env Evd.empty c)
 
-  let pretype_sort = function
-    | RProp c -> judge_of_prop_contents c
-    | RType _ -> judge_of_new_Type ()
+  let pretype_sort evdref = function
+    | GProp c -> judge_of_prop_contents c
+    | GType _ -> evd_comb0 judge_of_new_Type evdref
 
   let split_tycon_lam loc env evd tycon =
     let rec real_split evd c =
@@ -192,44 +189,44 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   (* in environment [env], with existential variables [( evdref)] and *)
   (* the type constraint tycon *)
   let rec pretype (tycon : type_constraint) env evdref lvar c =
-(*     let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
+(*     let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *)
 (* 			       str " with tycon " ++ Evarutil.pr_tycon env tycon)  *)
 (*     with _ -> () *)
 (*     in *)
     match c with
-    | RRef (loc,ref) ->
+    | GRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_ref evdref env ref)
 	  tycon
 
-    | RVar (loc, id) ->
+    | GVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
-    | REvar (loc, ev, instopt) ->
+    | GEvar (loc, ev, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-	let hyps = evar_context (Evd.find ( !evdref) ev) in
+	let hyps = evar_context (Evd.find !evdref ev) in
 	let args = match instopt with
           | None -> instance_from_named_context hyps
           | Some inst -> failwith "Evar subtitutions not implemented" in
 	let c = mkEvar (ev, args) in
-	let j = (Retyping.get_judgment_of env ( !evdref) c) in
+	let j = (Retyping.get_judgment_of env !evdref c) in
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
-    | RPatVar (loc,(someta,n)) ->
-	anomaly "Found a pattern variable in a rawterm to type"
+    | GPatVar (loc,(someta,n)) ->
+	anomaly "Found a pattern variable in a glob_constr to type"
 
-    | RHole (loc,k) ->
+    | GHole (loc,k) ->
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
             | None | Some _ ->
-		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+		e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | RRec (loc,fixkind,names,bl,lar,vdef) ->
+    | GRec (loc,fixkind,names,bl,lar,vdef) ->
 	let rec type_bl env ctxt = function
             [] -> ctxt
           | (na,k,None,ty)::bl ->
@@ -260,7 +257,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    push_rec_types (names,marked_ftys,[||]) env
 	in
-	let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
+	let fixi = match fixkind with GFix (vn, i) -> i | GCoFix i -> i in
 	let vdefj =
 	  array_map2_i
 	    (fun i ctxt def ->
@@ -284,10 +281,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env evdref names ftys vdefj;
-	let ftys = Array.map (nf_evar ( !evdref)) ftys in
-	let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in
+	let ftys = Array.map (nf_evar !evdref) ftys in
+	let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
 	let fixj = match fixkind with
-	  | RFix (vn,i) ->
+	  | GFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
 	      (* If recursive argument was not given by user, we try all args.
 	         An earlier approach was to look only for inductive arguments,
@@ -303,16 +300,17 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	      let fixdecls = (names,ftys,fdefs) in
 	      let indexes = search_guard loc env possible_indexes fixdecls in
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
-	  | RCoFix i ->
+	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+	      (try check_cofix env cofix with e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
-    | RSort (loc,s) ->
-	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+    | GSort (loc,s) ->
+	let s' = pretype_sort evdref s in
+	inh_conv_coerce_to_tycon loc env evdref s' tycon
 
-    | RApp (loc,f,args) ->
+    | GApp (loc,f,args) ->
 	let length = List.length args in
 	let ftycon =
 	  let ty =
@@ -329,13 +327,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | _ -> None
 	in
 	let fj = pretype ftycon env evdref lvar f in
- 	let floc = loc_of_rawconstr f in
+ 	let floc = loc_of_glob_constr f in
 	let rec apply_rec env n resj tycon = function
 	  | [] -> resj
 	  | c::rest ->
-	      let argloc = loc_of_rawconstr c in
+	      let argloc = loc_of_glob_constr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
-              let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in
+              let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
 		      Option.iter (fun ty -> evdref :=
@@ -353,10 +351,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
 			error_cant_apply_not_functional_loc
-			  (join_loc floc argloc) env ( !evdref)
+			  (join_loc floc argloc) env !evdref
 	      		  resj [hj]
 	in
-	let resj = j_nf_evar ( !evdref) (apply_rec env 1 fj ftycon args) in
+	let resj = j_nf_evar !evdref (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
 	  | App (f,args) when isInd f or isConst f ->
@@ -367,7 +365,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  | _ -> resj in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLambda(loc,name,k,c1,c2)      ->
+    | GLambda(loc,name,k,c1,c2)      ->
 	let tycon' = evd_comb1
 	  (fun evd tycon ->
 	    match tycon with
@@ -385,32 +383,32 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let resj = judge_of_abstraction env name j j' in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RProd(loc,name,k,c1,c2)        ->
+    | GProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let var = (name,j.utj_val) in
-	let env' = push_rel_assum var env in
+	let env' = Termops.push_rel_assum var env in
 	let j' = pretype_type empty_valcon env' evdref lvar c2 in
 	let resj =
 	  try judge_of_product env name j j'
-	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+	  with TypeError _ as e -> Loc.raise loc e in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLetIn(loc,name,c1,c2)      ->
+    | GLetIn(loc,name,c1,c2)      ->
 	let j = pretype empty_tycon env evdref lvar c1 in
-	let t = refresh_universes j.uj_type in
+	let t = Termops.refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
 	let j' = pretype tycon (push_rel var env) evdref lvar c2 in
 	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	    uj_type = subst1 j.uj_val j'.uj_type }
 
-    | RLetTuple (loc,nal,(na,po),c,d) ->
+    | GLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
-	  try find_rectype env ( !evdref) cj.uj_type
+	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env ( !evdref) cj
+	    let cloc = loc_of_glob_constr c in
+	      error_case_not_inductive_loc cloc env !evdref cj
 	in
 	let cstrs = get_constructors env indf in
 	if Array.length cstrs <> 1 then
@@ -434,14 +432,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		 | Some p ->
 		     let env_p = push_rels psign env in
 		     let pj = pretype_type empty_valcon env_p evdref lvar p in
-		     let ccl = nf_evar ( !evdref) pj.utj_val in
+		     let ccl = nf_evar !evdref pj.utj_val in
 		     let psign = make_arity_signature env true indf in (* with names *)
 		     let p = it_mkLambda_or_LetIn ccl psign in
 		     let inst =
 		       (Array.to_list cs.cs_concl_realargs)
 		       @[build_dependent_constructor cs] in
 		     let lp = lift cs.cs_nargs p in
-		     let fty = hnf_lam_applist env ( !evdref) lp inst in
+		     let fty = hnf_lam_applist env !evdref lp inst in
 		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
@@ -454,12 +452,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     let tycon = lift_tycon cs.cs_nargs tycon in
 		     let fj = pretype tycon env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-		     let ccl = nf_evar ( !evdref) fj.uj_type in
+		     let ccl = nf_evar !evdref fj.uj_type in
 		     let ccl =
 		       if noccur_between 1 cs.cs_nargs ccl then
 			 lift (- cs.cs_nargs) ccl
 		       else
-			 error_cant_find_case_type_loc loc env ( !evdref)
+			 error_cant_find_case_type_loc loc env !evdref
 			   cj.uj_val in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
@@ -469,13 +467,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     in
 		       { uj_val = v; uj_type = ccl })
 
-    | RIf (loc,c,(na,po),b1,b2) ->
+    | GIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
-	  try find_rectype env ( !evdref) cj.uj_type
+	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env ( !evdref) cj in
+	    let cloc = loc_of_glob_constr c in
+	      error_case_not_inductive_loc cloc env !evdref cj in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
@@ -494,7 +492,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | Some p ->
 		let env_p = push_rels psign env in
 		let pj = pretype_type empty_valcon env_p evdref lvar p in
-		let ccl = nf_evar ( !evdref) pj.utj_val in
+		let ccl = nf_evar !evdref pj.utj_val in
 		let pred = it_mkLambda_or_LetIn ccl psign in
 		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
 		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
@@ -505,11 +503,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		let p = match tycon with
 		  | Some (None, ty) -> ty
 		  | None | Some _ ->
-                      e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+                      e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-	  let pred = nf_evar ( !evdref) pred in
-	  let p = nf_evar ( !evdref) p in
+	  let pred = nf_evar !evdref pred in
+	  let p = nf_evar !evdref p in
 	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
@@ -539,12 +537,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
-    | RCases (loc,sty,po,tml,eqns) ->
+    | GCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast (loc,c,k) ->
+    | GCast (loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
@@ -560,18 +558,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	in
 	  inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | RDynamic (loc,d) ->
-	if (Dyn.tag d) = "constr" then
-	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env ( !evdref) c) in
-	    j
-	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
-	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
-
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
-    | RHole loc ->
+    | GHole loc ->
 	(match valcon with
 	   | Some v ->
                let s =
@@ -586,12 +575,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		 { utj_val = v;
 		   utj_type = s }
 	   | None ->
-	       let s = new_Type_sort () in
+	       let s = Termops.new_Type_sort () in
 		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
 		   utj_type = s})
     | c ->
 	let j = pretype empty_tycon env evdref lvar c in
-	let loc = loc_of_rawconstr c in
+	let loc = loc_of_glob_constr c in
 	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	  match valcon with
 	    | None -> tj
@@ -599,7 +588,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env evdref v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
+                    (loc_of_glob_constr c) env !evdref tj.utj_val v
 
   let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
@@ -607,15 +596,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
 	  (pretype tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-    evdref := consider_remaining_unif_problems env !evdref;
-    if resolve_classes then
-      (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
-	  ~split:true ~fail:fail_evar env !evdref;
-       evdref := consider_remaining_unif_problems env !evdref);
-    let c = if expand_evar then nf_evar !evdref c' else c' in
-    if fail_evar then check_evars env Evd.empty !evdref c;
-    c
+	  (pretype_type empty_valcon env evdref lvar c).utj_val 
+    in
+      if resolve_classes then
+	(try 
+	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+	     ~split:true ~fail:true env !evdref;
+	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+	     ~split:true ~fail:false env !evdref
+	 with e -> if fail_evar then raise e else ());
+      evdref := consider_remaining_unif_problems env !evdref;
+      let c = if expand_evar then nf_evar !evdref c' else c' in
+      if fail_evar then check_evars env Evd.empty !evdref c;
+      c
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 362c4ddc..28bbdd35 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -15,10 +15,8 @@ let ($) f x = f x
 let contrib_name = "Program"
 
 let subtac_dir = [contrib_name]
-let fix_sub_module = "Wf"
-let utils_module = "Utils"
-let fixsub_module = subtac_dir @ [fix_sub_module]
-let utils_module = subtac_dir @ [utils_module]
+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
@@ -27,7 +25,6 @@ let safe_init_constant md name () =
   check_required_library ("Coq"::md);
   init_constant md name ()
 
-let fixsub = init_constant fixsub_module "Fix_sub"
 let ex_pi1 = init_constant utils_module "ex_pi1"
 let ex_pi2 = init_constant utils_module "ex_pi2"
 
@@ -55,11 +52,9 @@ let build_sig () =
 
 let sig_ = build_sig
 
-let fix_proto = init_constant tactics_module "fix_proto"
-let fix_proto_ref () = 
-  match Nametab.global (make_ref "Program.Tactics.fix_proto") with
-  | ConstRef c -> c
-  | _ -> assert false
+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"
@@ -92,12 +87,6 @@ let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
 let proj1 = init_constant ["Init"; "Logic"] "proj1"
 let proj2 = init_constant ["Init"; "Logic"] "proj2"
 
-let boolind = init_constant ["Init"; "Datatypes"] "bool"
-let sumboolind = init_constant ["Init"; "Specif"] "sumbool"
-let natind = init_constant ["Init"; "Datatypes"] "nat"
-let intind = init_constant ["ZArith"; "binint"] "Z"
-let existSind = init_constant ["Init"; "Specif"] "sigS"
-
 let existS = build_sigma_type
 
 let prod = build_prod
@@ -120,8 +109,8 @@ 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_rawconstr = Printer.pr_rawconstr_env
-let my_print_evardefs = Evd.pr_evar_map
+let my_print_glob_constr = Printer.pr_glob_constr_env
+let my_print_evardefs = Evd.pr_evar_map None
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
@@ -253,7 +242,7 @@ let build_dependent_sum l =
 		([intros;
 		  (tclTHENSEQ
 		     [constructor_tac false (Some 1) 1
-			(Rawterm.ImplicitBindings [mkVar n]);
+			(Glob_term.ImplicitBindings [mkVar n]);
 		      cont]);
 		 ])))
 	in
@@ -356,7 +345,7 @@ let destruct_ex ext ex =
       | _ -> [acc]
   in aux ex ext
 
-open Rawterm
+open Glob_term
 
 let id_of_name = function
     Name n -> n
@@ -418,7 +407,6 @@ let string_of_intset d =
 open Printer
 open Ppconstr
 open Nameops
-open Termops
 open Evd
 
 let pr_meta_map evd =
@@ -430,11 +418,11 @@ let pr_meta_map evd =
     | (mv,Cltyp (na,b)) ->
       	hov 0
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
-           print_constr b.rebus ++ fnl ())
+           Termops.print_constr b.rebus ++ fnl ())
     | (mv,Clval(na,b,_)) ->
       	hov 0
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-             print_constr (fst b).rebus ++ fnl ())
+             Termops.print_constr (fst b).rebus ++ fnl ())
   in
   prlist pr_meta_binding ml
 
@@ -445,11 +433,11 @@ let pr_evar_info evi =
     (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
     Printer.pr_named_context (Global.env()) (evar_context evi)
   in
-  let pty = print_constr evi.evar_concl 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"=> "  ++ print_constr c
+      | Evar_defined c -> spc() ++ str"=> "  ++ Termops.print_constr c
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
@@ -463,11 +451,11 @@ let pr_evar_map sigma =
 let pr_constraints pbs =
   h 0
     (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
-      print_constr t1 ++ spc() ++
+      Termops.print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
 	| Reduction.CUMUL -> "<=") ++
-      spc() ++ print_constr t2) pbs)
+      spc() ++ Termops.print_constr t2) pbs)
 
 let pr_evar_map evd =
   let pp_evm =
@@ -486,4 +474,4 @@ let tactics_tac s =
   lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
 
 let tactics_call tac args =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac 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
index f56c2932..de96cc60 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -6,7 +6,7 @@ open Pp
 open Evd
 open Decl_kinds
 open Topconstr
-open Rawterm
+open Glob_term
 open Util
 open Evarutil
 open Names
@@ -15,11 +15,9 @@ open Sign
 val ($) : ('a -> 'b) -> 'a -> 'b
 val contrib_name : string
 val subtac_dir : string list
-val fix_sub_module : string
 val fixsub_module : string list
 val init_constant : string list -> string -> constr delayed
 val init_reference : string list -> string -> global_reference delayed
-val fixsub : constr delayed
 val well_founded_ref : global_reference delayed
 val acc_ref : global_reference delayed
 val acc_inv_ref : global_reference delayed
@@ -35,7 +33,8 @@ val build_sig : unit -> coq_sigma_data
 val sig_ : coq_sigma_data delayed
 
 val fix_proto : constr delayed
-val fix_proto_ref : unit -> constant
+
+val hide_obligation : constr delayed
 
 val eq_ind : constr delayed
 val eq_rec : constr delayed
@@ -52,11 +51,6 @@ val jmeq_ind : constr delayed
 val jmeq_rec : constr delayed
 val jmeq_refl : constr delayed
 
-val boolind : constr delayed
-val sumboolind : constr delayed
-val natind : constr delayed
-val intind : constr delayed
-val existSind : constr delayed
 val existS : coq_sigma_data delayed
 val prod : coq_sigma_data delayed
 
@@ -74,7 +68,7 @@ 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_rawconstr : env -> rawconstr -> std_ppcmds
+val my_print_glob_constr : env -> glob_constr -> std_ppcmds
 val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds