Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

44 files changed, 216 insertions, 2477 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 27def8cc..362f6a61 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -29,7 +29,7 @@ let pr_goal gs =
     (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
     (str "thesis := "  ++ fnl ()),
     Printer.pr_context_of env,
-    Printer.pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+    Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
@@ -103,7 +103,7 @@ let proof_instr = Gram.entry_create "proofmode:instr"
 
 (* [Genarg.create_arg] creates a new embedding into Genarg. *)
 let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) =
-  Genarg.create_arg "proof_instr"
+  Genarg.create_arg None "proof_instr"
 let _ = Tacinterp.add_interp_genarg "proof_instr"
   begin
   begin fun e x -> (* declares the globalisation function *)
@@ -111,6 +111,7 @@ let _ = Tacinterp.add_interp_genarg "proof_instr"
       (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x))
   end,
   begin fun ist gl x -> (* declares the interpretation function *)
+    Tacmach.project gl ,
     Genarg.in_gen wit_proof_instr 
       (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x))
   end,
diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v
deleted file mode 100644
index 1b66c334..00000000
--- a/plugins/dp/Dp.v
+++ /dev/null
@@ -1,118 +0,0 @@
-(* Calls to external decision procedures *)
-
-Require Export ZArith.
-Require Export Classical.
-
-(* Zenon *)
-
-(*  Copyright 2004 INRIA  *)
-Lemma zenon_nottrue :
-  (~True -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_noteq : forall (T : Type) (t : T),
-  ((t <> t) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_and : forall P Q : Prop,
-  (P -> Q -> False) -> (P /\ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_or : forall P Q : Prop,
-  (P -> False) -> (Q -> False) -> (P \/ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_imply : forall P Q : Prop,
-  (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_equiv : forall P Q : Prop,
-  (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notand : forall P Q : Prop,
-  (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notor : forall P Q : Prop,
-  (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notimply : forall P Q : Prop,
-  (P -> ~Q -> False) -> (~(P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notequiv : forall P Q : Prop,
-  (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
-  (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
-  ((P t) -> False) -> ((forall x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
-  (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
-  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
-Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
-
-Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
-Proof. auto. Qed.
-
-Lemma zenon_equal_step :
-  forall (S T : Type) (fa fb : S -> T) (a b : S),
-  (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
-Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
-
-Lemma zenon_pnotp : forall P Q : Prop,
-  (P = Q) -> (P -> ~Q -> False).
-Proof. intros P Q Ha. rewrite Ha. auto. Qed.
-
-Lemma zenon_notequal : forall (T : Type) (a b : T),
-  (a = b) -> (a <> b -> False).
-Proof. auto. Qed.
-
-Ltac zenon_intro id :=
-  intro id || let nid := fresh in (intro nid; clear nid)
-.
-
-Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
-Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
-Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
-Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
-Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
-Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
-Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
-Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
-Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
-Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
-
-Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
-Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.
-
-(* Ergo *)
-
-Set Implicit Arguments.
-Section congr.
-  Variable t:Type.
-Lemma ergo_eq_concat_1 :
-  forall (P:t -> Prop) (x y:t),
-    P x -> x = y -> P y.
-Proof.
-  intros; subst; auto.
-Qed.
-
-Lemma ergo_eq_concat_2 :
-  forall (P:t -> t -> Prop) (x1 x2 y1 y2:t),
-    P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2.
-Proof.
-  intros; subst; auto.
-Qed.
-
-End congr.
diff --git a/plugins/dp/TODO b/plugins/dp/TODO
deleted file mode 100644
index 44349e21..00000000
--- a/plugins/dp/TODO
+++ /dev/null
@@ -1,24 +0,0 @@
-
-TODO
-----
-
-- axiomes pour les prédicats récursifs comme
-
-  Fixpoint even (n:nat) : Prop :=
-  match n with 
-  O => True
-  | S O => False
-  | S (S p) => even p
-  end.
-
-  ou encore In sur les listes du module Coq List.
-
-- discriminate
-
-- inversion (Set et Prop)
-
-
-BUGS
-----
-
-
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
deleted file mode 100644
index 837195e4..00000000
--- a/plugins/dp/dp.ml
+++ /dev/null
@@ -1,1133 +0,0 @@
-(* Authors: Nicolas Ayache and Jean-Christophe Filliâtre *)
-(* Tactics to call decision procedures *)
-
-(* Works in two steps:
-
-   - first the Coq context and the current goal are translated in
-     Polymorphic First-Order Logic (see fol.mli in this directory)
-
-   - then the resulting query is passed to the Why tool that translates
-     it to the syntax of the selected prover (Simplify, CVC Lite, haRVey,
-     Zenon)
-*)
-
-open Util
-open Pp
-open Libobject
-open Summary
-open Term
-open Tacmach
-open Tactics
-open Tacticals
-open Fol
-open Names
-open Nameops
-open Namegen
-open Coqlib
-open Hipattern
-open Libnames
-open Declarations
-open Dp_why
-
-let debug = ref false
-let set_debug b = debug := b
-let trace = ref false
-let set_trace b = trace := b
-let timeout = ref 10
-let set_timeout n = timeout := n
-
-let dp_timeout_obj : int -> obj =
-  declare_object
-    {(default_object "Dp_timeout") with
-       cache_function = (fun (_,x) -> set_timeout x);
-       load_function = (fun _ (_,x) -> set_timeout x)}
-
-let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
-
-let dp_debug_obj : bool -> obj =
-  declare_object
-    {(default_object "Dp_debug") with
-       cache_function = (fun (_,x) -> set_debug x);
-       load_function = (fun _ (_,x) -> set_debug x)}
-
-let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
-
-let dp_trace_obj : bool -> obj =
-  declare_object
-    {(default_object "Dp_trace") with
-       cache_function = (fun (_,x) -> set_trace x);
-       load_function = (fun _ (_,x) -> set_trace x)}
-
-let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
-
-let logic_dir = ["Coq";"Logic";"Decidable"]
-let coq_modules =
-  init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
-    @ [["Coq"; "ZArith"; "BinInt"];
-       ["Coq"; "Reals"; "Rdefinitions"];
-       ["Coq"; "Reals"; "Raxioms";];
-       ["Coq"; "Reals"; "Rbasic_fun";];
-       ["Coq"; "Reals"; "R_sqrt";];
-       ["Coq"; "Reals"; "Rfunctions";]]
-    @ [["Coq"; "omega"; "OmegaLemmas"]]
-
-let constant = gen_constant_in_modules "dp" coq_modules
-
-(* integers constants and operations *)
-let coq_Z = lazy (constant "Z")
-let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant "Zmult")
-let coq_Zopp = lazy (constant "Zopp")
-let coq_Zminus = lazy (constant "Zminus")
-let coq_Zdiv = lazy (constant "Zdiv")
-let coq_Zs = lazy (constant "Zs")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zle = lazy (constant "Zle")
-let coq_Zge = lazy (constant "Zge")
-let coq_Zlt = lazy (constant "Zlt")
-let coq_Z0 = lazy (constant "Z0")
-let coq_Zpos = lazy (constant "Zpos")
-let coq_Zneg = lazy (constant "Zneg")
-let coq_xH = lazy (constant "xH")
-let coq_xI = lazy (constant "xI")
-let coq_xO = lazy (constant "xO")
-let coq_iff = lazy (constant "iff")
-
-(* real constants and operations *)
-let coq_R = lazy (constant "R")
-let coq_R0 = lazy (constant "R0")
-let coq_R1 = lazy (constant "R1")
-let coq_Rgt = lazy (constant "Rgt")
-let coq_Rle = lazy (constant "Rle")
-let coq_Rge = lazy (constant "Rge")
-let coq_Rlt = lazy (constant "Rlt")
-let coq_Rplus = lazy (constant "Rplus")
-let coq_Rmult = lazy (constant "Rmult")
-let coq_Ropp = lazy (constant "Ropp")
-let coq_Rminus = lazy (constant "Rminus")
-let coq_Rdiv = lazy (constant "Rdiv")
-let coq_powerRZ = lazy (constant "powerRZ")
-
-(* not Prop typed expressions *)
-exception NotProp
-
-(* not first-order expressions *)
-exception NotFO
-
-(* Renaming of Coq globals *)
-
-let global_names = Hashtbl.create 97
-let used_names = Hashtbl.create 97
-
-let rename_global r =
-  try
-    Hashtbl.find global_names r
-  with Not_found ->
-    let rec loop id =
-      if Hashtbl.mem used_names id then
-	loop (lift_subscript id)
-      else begin
-	Hashtbl.add used_names id ();
-	let s = string_of_id id in
-	Hashtbl.add global_names r s;
-	s
-      end
-    in
-    loop (Nametab.basename_of_global r)
-
-let foralls =
-  List.fold_right
-    (fun (x,t) p -> Forall (x, t, p))
-
-let fresh_var = function
-  | Anonymous -> rename_global (VarRef (id_of_string "x"))
-  | Name x -> rename_global (VarRef x)
-
-(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
-   env names, and returns the new variables together with the new
-   environment *)
-let coq_rename_vars env vars =
-  let avoid = ref (Termops.ids_of_named_context (Environ.named_context env)) in
-  List.fold_right
-    (fun (na,t) (newvars, newenv) ->
-       let id = next_name_away na !avoid in
-       avoid := id :: !avoid;
-       id :: newvars, Environ.push_named (id, None, t) newenv)
-    vars ([],env)
-
-(* extract the prenex type quantifications i.e.
-   type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
-let decomp_type_quantifiers env t =
-  let rec loop vars t = match kind_of_term t with
-    | Prod (n, a, t) when is_Set a || is_Type a ->
-	loop ((n,a) :: vars) t
-    | _ ->
-	let vars, env = coq_rename_vars env vars in
-	let t = substl (List.map mkVar vars) t in
-	List.rev vars, env, t
-  in
-  loop [] t
-
-(* same thing with lambda binders (for axiomatize body) *)
-let decomp_type_lambdas env t =
-  let rec loop vars t = match kind_of_term t with
-    | Lambda (n, a, t) when is_Set a || is_Type a ->
-	loop ((n,a) :: vars) t
-    | _ ->
-	let vars, env = coq_rename_vars env vars in
-	let t = substl (List.map mkVar vars) t in
-	List.rev vars, env, t
-  in
-  loop [] t
-
-let decompose_arrows =
-  let rec arrows_rec l c = match kind_of_term c with
-    | Prod (_,t,c) when not (Termops.dependent (mkRel 1) c) -> arrows_rec (t :: l) c
-    | Cast (c,_,_) -> arrows_rec l c
-    | _ -> List.rev l, c
-  in
-  arrows_rec []
-
-let rec eta_expanse t vars env i =
-  assert (i >= 0);
-  if i = 0 then
-    t, vars, env
-  else
-    match kind_of_term (Typing.type_of env Evd.empty t) with
-      | Prod (n, a, b) when not (Termops.dependent (mkRel 1) b) ->
-	  let avoid = Termops.ids_of_named_context (Environ.named_context env) in
-	  let id = next_name_away n avoid in
-	  let env' = Environ.push_named (id, None, a) env in
-	  let t' = mkApp (t, [| mkVar id |]) in
-	  eta_expanse t' (id :: vars) env' (pred i)
-      | _ ->
-	  assert false
-
-let rec skip_k_args k cl = match k, cl with
-  | 0, _ -> cl
-  | _, _ :: cl -> skip_k_args (k-1) cl
-  | _, [] -> raise NotFO
-
-(* Coq global references *)
-
-type global = Gnot_fo | Gfo of Fol.decl
-
-let globals = ref Refmap.empty
-let globals_stack = ref []
-
-(* synchronization *)
-let () =
-  Summary.declare_summary "Dp globals"
-    { Summary.freeze_function = (fun () -> !globals, !globals_stack);
-      Summary.unfreeze_function =
-	(fun (g,s) -> globals := g; globals_stack := s);
-      Summary.init_function = (fun () -> ()) }
-
-let add_global r d = globals := Refmap.add r d !globals
-let mem_global r = Refmap.mem r !globals
-let lookup_global r = match Refmap.find r !globals with
-  | Gnot_fo -> raise NotFO
-  | Gfo d -> d
-
-let locals = Hashtbl.create 97
-
-let lookup_local r =  match Hashtbl.find locals r with
-  | Gnot_fo -> raise NotFO
-  | Gfo d -> d
-
-let iter_all_constructors i f =
-  let _, oib = Global.lookup_inductive i in
-  Array.iteri
-    (fun j tj -> f j (mkConstruct (i, j+1)))
-    oib.mind_nf_lc
-
-
-(* injection c [t1,...,tn] adds the injection axiom
-     forall x1:t1,...,xn:tn,y1:t1,...,yn:tn.
-       c(x1,...,xn)=c(y1,...,yn) -> x1=y1 /\ ... /\ xn=yn *)
-
-let injection c l =
-  let i = ref 0 in
-  let var s = incr i; id_of_string (s ^ string_of_int !i) in
-  let xl = List.map (fun t -> rename_global (VarRef (var "x")), t) l in
-  i := 0;
-  let yl = List.map (fun t -> rename_global (VarRef (var "y")), t) l in
-  let f =
-    List.fold_right2
-      (fun (x,_) (y,_) p -> And (Fatom (Eq (App (x,[]),App (y,[]))), p))
-      xl yl True
-  in
-  let vars = List.map (fun (x,_) -> App(x,[])) in
-  let f = Imp (Fatom (Eq (App (c, vars xl), App (c, vars yl))), f) in
-  let foralls = List.fold_right (fun (x,t) p -> Forall (x, t, p)) in
-  let f = foralls xl (foralls yl f) in
-  let ax = Axiom ("injection_" ^ c, f) in
-  globals_stack := ax :: !globals_stack
-
-(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
-   identifiers n1...nk with the same path as c, if they exist; otherwise
-   raises Not_found *)
-let rec_names_for c =
-  let mp,dp,_ = Names.repr_con c in
-  array_map_to_list
-    (function
-       | Name id ->
-	   let c' = Names.make_con mp dp (label_of_id id) in
-	   ignore (Global.lookup_constant c');
-	   msgnl (Printer.pr_constr (mkConst c'));
-	   c'
-       | Anonymous ->
-	   raise Not_found)
-
-(* abstraction tables *)
-
-let term_abstractions = Hashtbl.create 97
-
-let new_abstraction =
-  let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r
-
-(* Arithmetic constants *)
-
-exception NotArithConstant
-
-(* translates a closed Coq term p:positive into a FOL term of type int *)
-
-let big_two = Big_int.succ_big_int Big_int.unit_big_int
-
-let rec tr_positive p = match kind_of_term p with
-  | Term.Construct _ when p = Lazy.force coq_xH ->
-      Big_int.unit_big_int
-  | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
-(*
-      Plus (Mult (Cst 2, tr_positive a), Cst 1)
-*)
-      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
-  | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
-(*
-      Mult (Cst 2, tr_positive a)
-*)
-      Big_int.mult_big_int big_two (tr_positive a)
-  | Term.Cast (p, _, _) ->
-      tr_positive p
-  | _ ->
-      raise NotArithConstant
-
-(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
-let rec tr_arith_constant t = match kind_of_term t with
-  | Term.Construct _ when t = Lazy.force coq_Z0 ->
-      Cst Big_int.zero_big_int
-  | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
-      Cst (tr_positive a)
-  | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
-      Cst (Big_int.minus_big_int (tr_positive a))
-  | Term.Const _ when t = Lazy.force coq_R0 ->
-      RCst Big_int.zero_big_int
-  | Term.Const _ when t = Lazy.force coq_R1 ->
-      RCst Big_int.unit_big_int
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus ->
-      let ta = tr_arith_constant a in
-      let tb = tr_arith_constant b in
-      begin match ta,tb with
-        | RCst na, RCst nb -> RCst (Big_int.add_big_int na nb)
-        | _ -> raise NotArithConstant
-      end
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult ->
-      let ta = tr_arith_constant a in
-      let tb = tr_arith_constant b in
-      begin match ta,tb with
-        | RCst na, RCst nb -> RCst (Big_int.mult_big_int na nb)
-        | _ -> raise NotArithConstant
-      end
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_powerRZ ->
-      tr_powerRZ a b
-  | Term.Cast (t, _, _) ->
-      tr_arith_constant t
-  | _ ->
-      raise NotArithConstant
-
-(* translates a constant of the form (powerRZ 2 int_constant) *)
-and tr_powerRZ a b =
-  (* checking first that a is (R1 + R1) *)
-  match kind_of_term a with
-  | Term.App (f, [|c;d|]) when f = Lazy.force coq_Rplus ->
-      begin
-      match kind_of_term c,kind_of_term d with
-        | Term.Const _, Term.Const _
-            when c = Lazy.force coq_R1 && d = Lazy.force coq_R1 ->
-            begin
-              match tr_arith_constant b with
-                | Cst n -> Power2 n
-                | _ -> raise NotArithConstant
-            end
-        | _ -> raise NotArithConstant
-      end
-  | _ -> raise NotArithConstant
-
-
-(* translate a Coq term t:Set into a FOL type expression;
-   tv = list of type variables *)
-and tr_type tv env t =
-  let t = Reductionops.nf_betadeltaiota env Evd.empty t in
-  if t = Lazy.force coq_Z then
-    Tid ("int", [])
-  else if t = Lazy.force coq_R then
-    Tid ("real", [])
-  else match kind_of_term t with
-    | Var x when List.mem x tv ->
-	Tvar (string_of_id x)
-    | _ ->
-	let f, cl = decompose_app t in
-	begin try
-	  let r = global_of_constr f in
-	  match tr_global env r with
-	    | DeclType (id, k) ->
-		assert (k = List.length cl); (* since t:Set *)
-		Tid (id, List.map (tr_type tv env) cl)
-	    | _ ->
-		raise NotFO
-	with
-	  | Not_found ->
-	      raise NotFO
-	  | NotFO ->
-	      (* we need to abstract some part of (f cl) *)
-	      (*TODO*)
-	      raise NotFO
-	end
-
-and make_term_abstraction tv env c =
-  let ty = Typing.type_of env Evd.empty c in
-  let id = new_abstraction () in
-  match tr_decl env id ty with
-    | DeclFun (id,_,_,_) as _d ->
-        raise NotFO
-        (* [CM 07/09/2009] deactivated because it generates
-           unbound identifiers 'abstraction_<number>'
-	begin try
-	  Hashtbl.find term_abstractions c
-	with Not_found ->
-	  Hashtbl.add term_abstractions c id;
-	  globals_stack := d :: !globals_stack;
-	  id
-	end
-        *)
-    | _ ->
-	raise NotFO
-
-(* translate a Coq declaration id:ty in a FOL declaration, that is either
-   - a type declaration : DeclType (id, n) where n:int is the type arity
-   - a function declaration : DeclFun (id, tl, t) ; that includes constants
-   - a predicate declaration : DeclPred (id, tl)
-   - an axiom : Axiom (id, p)
- *)
-and tr_decl env id ty =
-  let tv, env, t = decomp_type_quantifiers env ty in
-  if is_Set t || is_Type t then
-    DeclType (id, List.length tv)
-  else if is_Prop t then
-    DeclPred (id, List.length tv, [])
-  else
-    let s = Typing.type_of env Evd.empty t in
-    if is_Prop s then
-      Axiom (id, tr_formula tv [] env t)
-    else
-      let l, t = decompose_arrows t in
-      let l = List.map (tr_type tv env) l in
-      if is_Prop t then
-	DeclPred(id, List.length tv, l)
-      else
-	let s = Typing.type_of env Evd.empty t in
-	if is_Set s || is_Type s then
-	  DeclFun (id, List.length tv, l, tr_type tv env t)
-	else
-	  raise NotFO
-
-(* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *)
-and tr_global env r = match r with
-  | VarRef id ->
-      lookup_local id
-  | r ->
-      try
-	lookup_global r
-      with Not_found ->
-	try
-	  let ty = Global.type_of_global r in
-	  let id = rename_global r in
-	  let d = tr_decl env id ty in
-	  (* r can be already declared if it is a constructor *)
-	  if not (mem_global r) then begin
-	    add_global r (Gfo d);
-	    globals_stack := d :: !globals_stack
-	  end;
-	  begin try axiomatize_body env r id d with NotFO -> () end;
-	  d
-	with NotFO ->
-	  add_global r Gnot_fo;
-	  raise NotFO
-
-and axiomatize_body env r id d = match r with
-  | VarRef _ ->
-      assert false
-  | ConstRef c ->
-      begin match body_of_constant (Global.lookup_constant c) with
-	| Some b ->
-	    let b = force b in
-	    let axioms =
-	      (match d with
-		 | DeclPred (id, _, []) ->
-		     let tv, env, b = decomp_type_lambdas env b in
-		     let value = tr_formula tv [] env b in
-		     [id, Iff (Fatom (Pred (id, [])), value)]
-		 | DeclFun (id, _, [], _) ->
-		     let tv, env, b = decomp_type_lambdas env b in
-		     let value = tr_term tv [] env b in
-		     [id, Fatom (Eq (Fol.App (id, []), value))]
-		 | DeclFun (id, _, l, _) | DeclPred (id, _, l) ->
-		     (*Format.eprintf "axiomatize_body %S@." id;*)
-		     let b = match kind_of_term b with
-		       (* a single recursive function *)
-		       | Fix (_, (_,_,[|b|])) ->
-			   subst1 (mkConst c) b
-                       (* mutually recursive functions *)
-		       | Fix ((_,i), (names,_,bodies)) ->
-                           (* we only deal with named functions *)
-			   begin try
-			     let l = rec_names_for c names in
-			     substl (List.rev_map mkConst l) bodies.(i)
-			   with Not_found ->
-			     b
-			   end
-		       | _ ->
-			   b
-		     in
-		     let tv, env, b = decomp_type_lambdas env b in
-		     let vars, t = decompose_lam b in
-		     let n = List.length l in
-		     let k = List.length vars in
-		     assert (k <= n);
-		     let vars, env = coq_rename_vars env vars in
-		     let t = substl (List.map mkVar vars) t in
-		     let t, vars, env = eta_expanse t vars env (n-k) in
-		     let vars = List.rev vars in
-		     let bv = vars in
-		     let vars = List.map (fun x -> string_of_id x) vars in
-		     let fol_var x = Fol.App (x, []) in
-		     let fol_vars = List.map fol_var vars in
-		     let vars = List.combine vars l in
-		     begin match d with
-		       | DeclFun (_, _, _, ty) ->
-			   begin match kind_of_term t with
-			     | Case (ci, _, e, br) ->
-				 equations_for_case env id vars tv bv ci e br
-			     | _ ->
-				 let t = tr_term tv bv env t in
-				 let ax =
-				   add_proof (Fun_def (id, vars, ty, t))
-				 in
-				 let p = Fatom (Eq (App (id, fol_vars), t)) in
-				 [ax, foralls vars p]
-			   end
-		       | DeclPred _ ->
-			   let value = tr_formula tv bv env t in
-			   let p = Iff (Fatom (Pred (id, fol_vars)), value) in
-			   [id, foralls vars p]
-		       | _ ->
-			   assert false
-		     end
-		 | DeclType _ ->
-		     raise NotFO
-		 | Axiom _ -> assert false)
-	    in
-	    let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in
-	    globals_stack := axioms @ !globals_stack
-	| None ->
-	    () (* Coq axiom *)
-      end
-  | IndRef i ->
-      iter_all_constructors i
-	(fun _ c ->
-	   let rc = global_of_constr c in
-	   try
-	     begin match tr_global env rc with
-	       | DeclFun (_, _, [], _) -> ()
-	       | DeclFun (idc, _, al, _) -> injection idc al
-	       | _ -> ()
-	     end
-	   with NotFO ->
-	     ())
-  | _ -> ()
-
-and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
-  | Var x when List.exists (fun (y, _) -> string_of_id x = y) vars ->
-      let eqs = ref [] in
-      iter_all_constructors ci.ci_ind
-	(fun j cj ->
-	   try
-	     let cjr = global_of_constr cj in
-	     begin match tr_global env cjr with
-	       | DeclFun (idc, _, l, _) ->
-		   let b = br.(j) in
-		   let rec_vars, b = decompose_lam b in
-		   let rec_vars, env = coq_rename_vars env rec_vars in
-		   let coq_rec_vars = List.map mkVar rec_vars in
-		   let b = substl coq_rec_vars b in
-		   let rec_vars = List.rev rec_vars in
-		   let coq_rec_term = applist (cj, List.rev coq_rec_vars) in
-		   let b = replace_vars [x, coq_rec_term] b in
-		   let bv = bv @ rec_vars in
-		   let rec_vars = List.map string_of_id rec_vars in
-		   let fol_var x = Fol.App (x, []) in
-		   let fol_rec_vars = List.map fol_var rec_vars in
-		   let fol_rec_term = App (idc, fol_rec_vars) in
-		   let rec_vars = List.combine rec_vars l in
-		   let fol_vars = List.map fst vars in
-		   let fol_vars = List.map fol_var fol_vars in
-		   let fol_vars = List.map (fun y -> match y with
-					      | App (id, _) ->
-						  if id = string_of_id x
-						  then fol_rec_term
-						  else y
-					      | _ -> y)
-				    fol_vars in
-		   let vars = vars @ rec_vars in
-		   let rec remove l e = match l with
-		     | [] -> []
-		     | (y, t)::l' -> if y = string_of_id e then l'
-		       else (y, t)::(remove l' e) in
-		   let vars = remove vars x in
-		   let p =
-		     Fatom (Eq (App (id, fol_vars),
-				tr_term tv bv env b))
-		   in
-		   eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs
-	       | _ ->
-		   assert false end
-	   with NotFO ->
-	     ());
-      !eqs
-  | _ ->
-      raise NotFO
-
-(* assumption: t:T:Set *)
-and tr_term tv bv env t =
-      try
-	tr_arith_constant t
-      with NotArithConstant ->
-  match kind_of_term t with
-    (* binary operations on integers *)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus ->
-      Plus (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus ->
-      Moins (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult ->
-      Mult (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv ->
-      Div (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a|]) when f = Lazy.force coq_Zopp ->
-      Opp (tr_term tv bv env a)
-    (* binary operations on reals *)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus ->
-      Plus (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rminus ->
-      Moins (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult ->
-      Mult (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rdiv ->
-      Div (tr_term tv bv env a, tr_term tv bv env b)
-  | Term.Var id when List.mem id bv ->
-      App (string_of_id id, [])
-  | _ ->
-	let f, cl = decompose_app t in
-	begin try
-	  let r = global_of_constr f in
-	  match tr_global env r with
-	    | DeclFun (s, k, _, _) ->
-		let cl = skip_k_args k cl in
-		Fol.App (s, List.map (tr_term tv bv env) cl)
-	    | _ ->
-		raise NotFO
-	with
-	  | Not_found ->
-	      raise NotFO
-	  | NotFO -> (* we need to abstract some part of (f cl) *)
-	      let rec abstract app = function
-		| [] ->
-		    Fol.App (make_term_abstraction tv env app, [])
-		| x :: l as args ->
-		    begin try
-		      let s = make_term_abstraction tv env app in
-		      Fol.App (s, List.map (tr_term tv bv env) args)
-		    with NotFO ->
-		      abstract (applist (app, [x])) l
-		    end
-	      in
-	      let app,l = match cl with
-		| x :: l -> applist (f, [x]), l | [] -> raise NotFO
-	      in
-	      abstract app l
-	end
-
-and quantifiers n a b tv bv env =
-  let vars, env = coq_rename_vars env [n,a] in
-  let id = match vars with [x] -> x | _ -> assert false in
-  let b = subst1 (mkVar id) b in
-  let t = tr_type tv env a in
-  let bv = id :: bv in
-  id, t, bv, env, b
-
-(* assumption: f is of type Prop *)
-and tr_formula tv bv env f =
-  let c, args = decompose_app f in
-  match kind_of_term c, args with
-    | Var id, [] ->
-	Fatom (Pred (rename_global (VarRef id), []))
-    | _, [t;a;b] when c = build_coq_eq () ->
-	let ty = Typing.type_of env Evd.empty t in
-	if is_Set ty || is_Type ty then
-	  let _ = tr_type tv env t in
-	  Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b))
-	else
-	  raise NotFO
-          (* comparisons on integers *)
-    | _, [a;b] when c = Lazy.force coq_Zle ->
-	Fatom (Le (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [a;b] when c = Lazy.force coq_Zlt ->
-	Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [a;b] when c = Lazy.force coq_Zge ->
-	Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [a;b] when c = Lazy.force coq_Zgt ->
-	Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b))
-          (* comparisons on reals *)
-    | _, [a;b] when c = Lazy.force coq_Rle ->
-	Fatom (Le (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [a;b] when c = Lazy.force coq_Rlt ->
-	Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [a;b] when c = Lazy.force coq_Rge ->
-	Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [a;b] when c = Lazy.force coq_Rgt ->
-	Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b))
-    | _, [] when c = build_coq_False () ->
-	False
-    | _, [] when c = build_coq_True () ->
-	True
-    | _, [a] when c = build_coq_not () ->
-	Not (tr_formula tv bv env a)
-    | _, [a;b] when c = build_coq_and () ->
-	And (tr_formula tv bv env a, tr_formula tv bv env b)
-    | _, [a;b] when c = build_coq_or () ->
-	Or (tr_formula tv bv env a, tr_formula tv bv env b)
-    | _, [a;b] when c = Lazy.force coq_iff ->
-	Iff (tr_formula tv bv env a, tr_formula tv bv env b)
-    | Prod (n, a, b), _ ->
-        if is_Prop (Typing.type_of env Evd.empty a) then
-	  Imp (tr_formula tv bv env a, tr_formula tv bv env b)
-	else
-	  let id, t, bv, env, b = quantifiers n a b tv bv env in
-	  Forall (string_of_id id, t, tr_formula tv bv env b)
-    | _, [_; a] when c = build_coq_ex () ->
-	begin match kind_of_term a with
-	  | Lambda(n, a, b) ->
-	      let id, t, bv, env, b = quantifiers n a b tv bv env in
-	      Exists (string_of_id id, t, tr_formula tv bv env b)
-	  | _ ->
-	      (* unusual case of the shape (ex p) *)
-	      raise NotFO (* TODO: we could eta-expanse *)
-	end
-    | _ ->
-	begin try
-	  let r = global_of_constr c in
-	  match tr_global env r with
-	    | DeclPred (s, k, _) ->
-		let args = skip_k_args k args in
-		Fatom (Pred (s, List.map (tr_term tv bv env) args))
-	    | _ ->
-		raise NotFO
-	with Not_found ->
-	  raise NotFO
-	end
-
-
-let tr_goal gl =
-  Hashtbl.clear locals;
-  let tr_one_hyp (id, ty) =
-    try
-      let s = rename_global (VarRef id) in
-      let d = tr_decl (pf_env gl) s ty in
-      Hashtbl.add locals id (Gfo d);
-      d
-    with NotFO ->
-      Hashtbl.add locals id Gnot_fo;
-      raise NotFO
-  in
-  let hyps =
-    List.fold_right
-      (fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc)
-      (pf_hyps_types gl) []
-  in
-  let c = tr_formula [] [] (pf_env gl) (pf_concl gl) in
-  let hyps = List.rev_append !globals_stack (List.rev hyps) in
-  hyps, c
-
-
-type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy | CVC3 | Z3
-
-let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
-
-let sprintf = Format.sprintf
-
-let file_contents f =
-  let buf = Buffer.create 1024 in
-  try
-    let c = open_in f in
-    begin try
-      while true do
-	let s = input_line c in Buffer.add_string buf s;
-	Buffer.add_char buf '\n'
-      done;
-      assert false
-    with End_of_file ->
-      close_in c;
-      Buffer.contents buf
-    end
-  with _ ->
-    sprintf "(cannot open %s)" f
-
-let timeout_sys_command cmd =
-  if !debug then Format.eprintf "command line: %s@." cmd;
-  let out = Filename.temp_file "out" "" in
-  let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
-  let ret = Sys.command cmd in
-  if !debug then
-    Format.eprintf "Output file %s:@.%s@." out (file_contents out);
-  ret, out
-
-let timeout_or_failure c cmd out =
-  if c = 152 then
-    Timeout
-  else
-    Failure
-      (sprintf "command %s failed with output:\n%s " cmd (file_contents out))
-
-let call_prover ?(opt="") file =
-  if !debug then Format.eprintf "calling prover on %s@." file;
-  let out = Filename.temp_file "out" "" in
-  let cmd =
-    sprintf "why-dp -timeout %d -batch %s > %s 2>&1" !timeout file out in
-  match Sys.command cmd with
-      0 -> Valid None
-    | 1 -> Failure (sprintf "could not run why-dp\n%s" (file_contents out))
-    | 2 -> Invalid
-    | 3 -> DontKnow
-    | 4 -> Timeout
-    | 5 -> Failure (sprintf "prover failed:\n%s" (file_contents out))
-    | n -> Failure (sprintf "Unknown exit status of why-dp: %d" n)
-
-let prelude_files = ref ([] : string list)
-
-let set_prelude l = prelude_files := l
-
-let dp_prelude_obj : string list -> obj =
-  declare_object
-    {(default_object "Dp_prelude") with
-       cache_function = (fun (_,x) -> set_prelude x);
-       load_function = (fun _ (_,x) -> set_prelude x)}
-
-let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
-
-let why_files f = String.concat " " (!prelude_files @ [f])
-
-let call_simplify fwhy =
-  let cmd =
-    sprintf "why --simplify %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
-(*
-  let cmd =
-    sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
-      !timeout fsx
-  in
-  let out = Sys.command cmd in
-  let r =
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
-  in
-*)
-  let r = call_prover fsx in
-  if not !debug then remove_files [fwhy; fsx];
-  r
-
-let call_ergo fwhy =
-  let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
-  (*let ftrace = Filename.temp_file "ergo_trace" "" in*)
-  (*NB: why-dp can't handle -cctrace
-  let cmd =
-    if !trace then
-      sprintf "alt-ergo -cctrace %s %s" ftrace fwhy
-
-    else
-      sprintf "alt-ergo %s" fwhy
-  in*)
-  let r = call_prover fwhy in
-  if not !debug then remove_files [fwhy; (*out*)];
-  r
-
-
-let call_zenon fwhy =
-  let cmd =
-    sprintf "why --no-zenon-prelude --zenon %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
-(*  why-dp won't let us having coqterm...
-  let out = Filename.temp_file "dp_out" "" in
-  let cmd =
-    sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out
-  in
-  let c = Sys.command cmd in
-  if not !debug then remove_files [fwhy; fznn];
-  if c = 137 then
-    Timeout
-  else begin
-    if c <> 0 then anomaly ("command failed: " ^ cmd);
-    if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then
-      error "Zenon failed";
-    let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in
-    if c = 0 then Valid (Some out) else Invalid
-  end
- *)
-   let r = call_prover fznn in
-   if not !debug then remove_files [fwhy; fznn];
-   r
-
-let call_smt ~smt fwhy =
-  let cmd = 
-    sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
-  let opt = "-smt-solver " ^ smt in
-  let r = call_prover ~opt fsmt in
-  if not !debug then remove_files [fwhy; fsmt];
-  r
-
-(*
-let call_yices fwhy =
-  let cmd =
-    sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
-  let cmd =
-    sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
-      !timeout fsmt
-  in
-  let out = Sys.command cmd in
-  let r =
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
-  in
-  if not !debug then remove_files [fwhy; fsmt];
-  r
-
-let call_cvc3 fwhy =
-  let cmd =
-    sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
-  let cmd =
-    sprintf "why-cpulimit %d cvc3 -lang smt %s > out 2>&1 && grep -q -w unsat out"
-      !timeout fsmt
-  in
-  let out = Sys.command cmd in
-  let r =
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
-  in
-  if not !debug then remove_files [fwhy; fsmt];
-  r
-*)
-
-let call_cvcl fwhy =
-  let cmd =
-    sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
-(*
-  let cmd =
-    sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out"
-      !timeout fcvc
-  in
-  let out = Sys.command cmd in
-  let r =
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout
-  in
-*)
-  let r = call_prover fcvc in
-  if not !debug then remove_files [fwhy; fcvc];
-  r
-
-let call_harvey fwhy =
-  let cmd =
-    sprintf "why --harvey --encoding strat %s" (why_files fwhy)
-  in
-  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
-  let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
-(*
-  let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in
-  if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed");
-  let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in
-  let outf = Filename.temp_file "rv" ".out" in
-  let out =
-    Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1"
-		   !timeout f outf)
-  in
-  let r =
-    if out <> 0 then
-      Timeout
-    else
-      let cmd =
-	sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
-      in
-      if Sys.command cmd = 0 then Valid None else Invalid
-  in
-  if not !debug then remove_files [fwhy; frv; outf];
-*)
-  let r = call_prover frv in
-  if not !debug then remove_files [fwhy; frv];
-  r
-
-let call_gwhy fwhy =
-  let cmd = sprintf "gwhy %s" (why_files fwhy) in
-  if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
-  NoAnswer
-
-let ergo_proof_from_file f gl =
-  let s =
-    let buf = Buffer.create 1024 in
-    let c = open_in f in
-    try
-      while true do Buffer.add_string buf (input_line c) done; assert false
-    with End_of_file ->
-      close_in c;
-      Buffer.contents buf
-  in
-  let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in
-  let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in
-  exact_check t gl
-
-let call_prover prover q =
-  let fwhy = Filename.temp_file "coq_dp" ".why" in
-  Dp_why.output_file fwhy q;
-  match prover with
-    | Simplify -> call_simplify fwhy
-    | Ergo -> call_ergo fwhy
-    | CVC3 -> call_smt ~smt:"cvc3" fwhy
-    | Yices -> call_smt ~smt:"yices" fwhy
-    | Z3 -> call_smt ~smt:"z3" fwhy
-    | Zenon -> call_zenon fwhy
-    | CVCLite -> call_cvcl fwhy
-    | Harvey -> call_harvey fwhy
-    | Gwhy -> call_gwhy fwhy
-
-let dp prover gl =
-  Coqlib.check_required_library ["Coq";"ZArith";"ZArith"];
-  let concl_type = pf_type_of gl (pf_concl gl) in
-  if not (is_Prop concl_type) then error "Conclusion is not a Prop";
-  try
-    let q = tr_goal gl in
-    begin match call_prover prover q with
-      | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
-      | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
-      | Valid _ -> Tactics.admit_as_an_axiom gl
-      | Invalid -> error "Invalid"
-      | DontKnow -> error "Don't know"
-      | Timeout -> error "Timeout"
-      | Failure s -> error s
-      | NoAnswer -> Tacticals.tclIDTAC gl
-    end
-  with NotFO ->
-    error "Not a first order goal"
-
-
-let simplify = tclTHEN intros (dp Simplify)
-let ergo = tclTHEN intros (dp Ergo)
-let cvc3 = tclTHEN intros (dp CVC3)
-let yices = tclTHEN intros (dp Yices)
-let z3 = tclTHEN intros (dp Z3)
-let cvc_lite = tclTHEN intros (dp CVCLite)
-let harvey = dp Harvey
-let zenon = tclTHEN intros (dp Zenon)
-let gwhy = tclTHEN intros (dp Gwhy)
-
-let dp_hint l =
-  let env = Global.env () in
-  let one_hint (qid,r) =
-    if not (mem_global r) then begin
-      let ty = Global.type_of_global r in
-      let s = Typing.type_of env Evd.empty ty in
-      if is_Prop s then
-	try
-	  let id = rename_global r in
-	  let tv, env, ty = decomp_type_quantifiers env ty in
-	  let d = Axiom (id, tr_formula tv [] env ty) in
-	  add_global r (Gfo d);
-	  globals_stack := d :: !globals_stack
-	with NotFO ->
-	  add_global r Gnot_fo;
-	  msg_warning
-	    (pr_reference qid ++
-	     str " ignored (not a first order proposition)")
-	else begin
-	  add_global r Gnot_fo;
-	  msg_warning
-	    (pr_reference qid ++ str " ignored (not a proposition)")
-	end
-    end
-  in
-  List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
-
-let dp_hint_obj : reference list -> obj =
-  declare_object
-    {(default_object "Dp_hint") with
-       cache_function = (fun (_,l) -> dp_hint l);
-       load_function = (fun _ (_,l) -> dp_hint l)}
-
-let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
-
-let dp_predefined qid s =
-  let r = Nametab.global qid in
-  let ty = Global.type_of_global r in
-  let env = Global.env () in
-  let id = rename_global r in
-  try
-    let d = match tr_decl env id ty with
-      | DeclType (_, n) -> DeclType (s, n)
-      | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty)
-      | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl)
-      | Axiom _ as d -> d
-    in
-    match d with
-      | Axiom _ ->  msg_warning (str " ignored (axiom)")
-      | d -> add_global r (Gfo d)
-  with NotFO ->
-    msg_warning (str " ignored (not a first order declaration)")
-
-let dp_predefined_obj : reference * string -> obj =
-  declare_object
-    {(default_object "Dp_predefined") with
-       cache_function = (fun (_,(id,s)) -> dp_predefined id s);
-       load_function = (fun _ (_,(id,s)) -> dp_predefined id s)}
-
-let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
-
-let _ = declare_summary "Dp options"
-	  { freeze_function =
-	      (fun () -> !debug, !trace, !timeout, !prelude_files);
-	    unfreeze_function =
-	      (fun (d,tr,tm,pr) ->
-		debug := d; trace := tr; timeout := tm; prelude_files := pr);
-	    init_function =
-	      (fun () ->
-		debug := false; trace := false; timeout := 10;
-		prelude_files := []) }
diff --git a/plugins/dp/dp.mli b/plugins/dp/dp.mli
deleted file mode 100644
index f40f8688..00000000
--- a/plugins/dp/dp.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-
-open Libnames
-open Proof_type
-
-val simplify : tactic
-val ergo : tactic
-val cvc3 : tactic
-val yices : tactic
-val cvc_lite : tactic
-val harvey : tactic
-val zenon : tactic
-val gwhy : tactic
-val z3: tactic
-
-val dp_hint : reference list -> unit
-val dp_timeout : int -> unit
-val dp_debug : bool -> unit
-val dp_trace : bool -> unit
-val dp_prelude : string list -> unit
-val dp_predefined : reference -> string -> unit
diff --git a/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib
deleted file mode 100644
index 63252d6a..00000000
--- a/plugins/dp/dp_plugin.mllib
+++ /dev/null
@@ -1,5 +0,0 @@
-Dp_why
-Dp_zenon
-Dp
-G_dp
-Dp_plugin_mod
diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml
deleted file mode 100644
index 199c3087..00000000
--- a/plugins/dp/dp_why.ml
+++ /dev/null
@@ -1,185 +0,0 @@
-
-(* Pretty-print PFOL (see fol.mli) in Why syntax *)
-
-open Format
-open Fol
-
-type proof =
-  | Immediate of Term.constr
-  | Fun_def of string * (string * typ) list * typ * term
-
-let proofs = Hashtbl.create 97
-let proof_name =
-  let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r
-
-let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n
-
-let find_proof = Hashtbl.find proofs
-
-let rec print_list sep print fmt = function
-  | [] -> ()
-  | [x] -> print fmt x
-  | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-let space fmt () = fprintf fmt "@ "
-let comma fmt () = fprintf fmt ",@ "
-
-let is_why_keyword =
-  let h = Hashtbl.create 17 in
-  List.iter
-    (fun s -> Hashtbl.add h s ())
-    ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin";
-     "bool"; "do"; "done"; "else"; "end"; "exception"; "exists";
-     "external"; "false"; "for"; "forall"; "fun"; "function"; "goal";
-     "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not";
-     "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises";
-     "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try";
-     "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ];
-  Hashtbl.mem h
-
-let ident fmt s =
-  if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s
-
-let rec print_typ fmt = function
-  | Tvar x -> fprintf fmt "'%a" ident x
-  | Tid ("int", []) -> fprintf fmt "int"
-  | Tid ("real", []) -> fprintf fmt "real"
-  | Tid (x, []) -> fprintf fmt "%a" ident x
-  | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x
-  | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x
-
-let print_arg fmt (id,typ) = fprintf fmt "%a: %a" ident id print_typ typ
-
-let rec print_term fmt = function
-  | Cst n ->
-      fprintf fmt "%s" (Big_int.string_of_big_int n)
-  | RCst s ->
-      fprintf fmt "%s.0" (Big_int.string_of_big_int s)
-  | Power2 n ->
-      fprintf fmt "0x1p%s" (Big_int.string_of_big_int n)
-  | Plus (a, b) ->
-      fprintf fmt "@[(%a +@ %a)@]" print_term a print_term b
-  | Moins (a, b) ->
-      fprintf fmt "@[(%a -@ %a)@]" print_term a print_term b
-  | Mult (a, b) ->
-      fprintf fmt "@[(%a *@ %a)@]" print_term a print_term b
-  | Div (a, b) ->
-      fprintf fmt "@[(%a /@ %a)@]" print_term a print_term b
-  | Opp (a) ->
-      fprintf fmt "@[(-@ %a)@]" print_term a
-  | App (id, []) ->
-      fprintf fmt "%a" ident id
-  | App (id, tl) ->
-      fprintf fmt "@[%a(%a)@]" ident id print_terms tl
-
-and print_terms fmt tl =
-  print_list comma print_term fmt tl
-
-let rec print_predicate fmt p =
-  let pp = print_predicate in
-  match p with
-  | True ->
-      fprintf fmt "true"
-  | False ->
-      fprintf fmt "false"
-  | Fatom (Eq (a, b)) ->
-      fprintf fmt "@[(%a =@ %a)@]" print_term a print_term b
-  | Fatom (Le (a, b)) ->
-      fprintf fmt "@[(%a <=@ %a)@]" print_term a print_term b
-  | Fatom (Lt (a, b))->
-      fprintf fmt "@[(%a <@ %a)@]" print_term a print_term b
-  | Fatom (Ge (a, b)) ->
-      fprintf fmt "@[(%a >=@ %a)@]" print_term a print_term b
-  | Fatom (Gt (a, b)) ->
-      fprintf fmt "@[(%a >@ %a)@]" print_term a print_term b
-  | Fatom (Pred (id, [])) ->
-      fprintf fmt "%a" ident id
-  | Fatom (Pred (id, tl)) ->
-      fprintf fmt "@[%a(%a)@]" ident id print_terms tl
-  | Imp (a, b) ->
-      fprintf fmt "@[(%a ->@ %a)@]" pp a pp b
-  | Iff (a, b) ->
-      fprintf fmt "@[(%a <->@ %a)@]" pp a pp b
-  | And (a, b) ->
-      fprintf fmt "@[(%a and@ %a)@]" pp a pp b
-  | Or (a, b) ->
-      fprintf fmt "@[(%a or@ %a)@]" pp a pp b
-  | Not a ->
-      fprintf fmt "@[(not@ %a)@]" pp a
-  | Forall (id, t, p) ->
-      fprintf fmt "@[(forall %a:%a.@ %a)@]" ident id print_typ t pp p
-  | Exists (id, t, p) ->
-      fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p
-
-let rec remove_iff args = function
-    Forall (id,t,p) -> remove_iff ((id,t)::args) p
-  | Iff(_,b) -> List.rev args, b
-  | _ -> raise Not_found
-
-let print_query fmt (decls,concl) =
-  let find_declared_preds l =
-    function
-        DeclPred (id,_,args) -> (id,args) :: l
-      | _ -> l
-  in
-  let find_defined_preds declared l = function
-      Axiom(id,f) ->
-        (try
-           let _decl = List.assoc id declared in
-           (id,remove_iff [] f)::l
-         with Not_found -> l)
-    | _ -> l
-  in
-  let declared_preds =
-    List.fold_left find_declared_preds [] decls in
-  let defined_preds =
-    List.fold_left (find_defined_preds declared_preds) [] decls
-  in
-  let print_dtype = function
-    | DeclType (id, 0) ->
-	fprintf fmt "@[type %a@]@\n@\n" ident id
-    | DeclType (id, 1) ->
-	fprintf fmt "@[type 'a %a@]@\n@\n" ident id
-    | DeclType (id, n) ->
-	fprintf fmt "@[type (";
-	for i = 1 to n do
-	  fprintf fmt "'a%d" i; if i < n then fprintf fmt ", "
-	done;
-	fprintf fmt ") %a@]@\n@\n" ident id
-    | DeclFun _ | DeclPred _ | Axiom _ ->
-	()
-  in
-  let print_dvar_dpred = function
-    | DeclFun (id, _, [], t) ->
-	fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t
-    | DeclFun (id, _, l, t) ->
-	fprintf fmt "@[logic %a : %a -> %a@]@\n@\n"
-	  ident id (print_list comma print_typ) l print_typ t
-    | DeclPred (id, _, []) when not (List.mem_assoc id defined_preds) ->
-	fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id
-    | DeclPred (id, _, l) when not (List.mem_assoc id defined_preds) ->
-	fprintf fmt "@[logic %a : %a -> prop@]@\n@\n"
-	  ident id (print_list comma print_typ) l
-    | DeclType _ | Axiom _ | DeclPred _ ->
-	()
-  in
-  let print_assert = function
-    | Axiom(id,_) when List.mem_assoc id defined_preds ->
-        let args, def = List.assoc id defined_preds in
-        fprintf fmt "@[predicate %a(%a) =@\n%a@]@\n" ident id
-          (print_list comma print_arg) args print_predicate def  
-    | Axiom (id, f)  ->
-	fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f
-    | DeclType _ | DeclFun _ | DeclPred _ ->
-	()
-  in
-  List.iter print_dtype decls;
-  List.iter print_dvar_dpred decls;
-  List.iter print_assert decls;
-  fprintf fmt "@[<hov 2>goal coq___goal: %a@]" print_predicate concl
-
-let output_file f q =
-  let c = open_out f in
-  let fmt = formatter_of_out_channel c in
-  fprintf fmt "@[%a@]@." print_query q;
-  close_out c
diff --git a/plugins/dp/dp_why.mli b/plugins/dp/dp_why.mli
deleted file mode 100644
index 0efa24a2..00000000
--- a/plugins/dp/dp_why.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-
-open Fol
-
-(* generation of the Why file *)
-
-val output_file : string -> query -> unit
-
-(* table to translate the proofs back to Coq (used in dp_zenon) *)
-
-type proof =
-  | Immediate of Term.constr
-  | Fun_def of string * (string * typ) list * typ * term
-
-val add_proof : proof -> string
-val find_proof : string -> proof
-
-
diff --git a/plugins/dp/dp_zenon.mli b/plugins/dp/dp_zenon.mli
deleted file mode 100644
index 0a727d1f..00000000
--- a/plugins/dp/dp_zenon.mli
+++ /dev/null
@@ -1,7 +0,0 @@
-
-open Fol
-
-val set_debug : bool -> unit
-
-val proof_from_file : string -> Proof_type.tactic
-
diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll
deleted file mode 100644
index 949e91e3..00000000
--- a/plugins/dp/dp_zenon.mll
+++ /dev/null
@@ -1,189 +0,0 @@
-
-{
-
-  open Lexing
-  open Pp
-  open Util
-  open Names
-  open Tacmach
-  open Dp_why
-  open Tactics
-  open Tacticals
-
-  let debug = ref false
-  let set_debug b = debug := b
-
-  let buf = Buffer.create 1024
-
-  let string_of_global env ref =
-    Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref)
-
-  let axioms = ref []
-
-  (* we cannot interpret the terms as we read them (since some lemmas
-     may need other lemmas to be already interpreted) *)
-  type lemma = { l_id : string; l_type : string; l_proof : string }
-  type zenon_proof = lemma list * string
-
-}
-
-let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+
-let space = [' ' '\t' '\r']
-
-rule start = parse
-| "(* BEGIN-PROOF *)" "\n" { scan lexbuf }
-| _ { start lexbuf }
-| eof { anomaly "malformed Zenon proof term" }
-
-(* here we read the lemmas and the main proof term;
-   meanwhile we maintain the set of axioms that were used *)
-
-and scan = parse
-| "Let" space (ident as id) space* ":"
-  { let t = read_coq_term lexbuf in
-    let p = read_lemma_proof lexbuf in
-    let l,pr = scan lexbuf in
-    { l_id = id; l_type = t; l_proof = p } :: l, pr }
-| "Definition theorem:"
-  { let t = read_main_proof lexbuf in [], t }
-| _ | eof
-  { anomaly "malformed Zenon proof term" }
-
-and read_coq_term = parse
-| "." "\n"
-  { let s = Buffer.contents buf in Buffer.clear buf; s }
-| "coq__" (ident as id) (* a Why keyword renamed *)
-  { Buffer.add_string buf id; read_coq_term lexbuf }
-| ("dp_axiom__" ['0'-'9']+) as id
-  { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf }
-| _ as c
-  { Buffer.add_char buf c; read_coq_term lexbuf }
-| eof
-  { anomaly "malformed Zenon proof term" }
-
-and read_lemma_proof = parse
-| "Proof" space
-  { read_coq_term lexbuf }
-| _ | eof
-  { anomaly "malformed Zenon proof term" }
-
-(* skip the main proof statement and then read its term *)
-and read_main_proof = parse
-| ":=" "\n"
-  { read_coq_term lexbuf }
-| _
-  { read_main_proof lexbuf }
-| eof
-  { anomaly "malformed Zenon proof term" }
-
-
-{
-
-  let read_zenon_proof f =
-    Buffer.clear buf;
-    let c = open_in f in
-    let lb = from_channel c in
-    let p = start lb in
-    close_in c;
-    if not !debug then begin try Sys.remove f with _ -> () end;
-    p
-
-  let constr_of_string gl s =
-    let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
-    Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
-
-  (* we are lazy here: we build strings containing Coq terms using a *)
-  (* pretty-printer Fol -> Coq *)
-  module Coq = struct
-    open Format
-    open Fol
-
-    let rec print_list sep print fmt = function
-      | [] -> ()
-      | [x] -> print fmt x
-      | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-    let space fmt () = fprintf fmt "@ "
-    let comma fmt () = fprintf fmt ",@ "
-
-    let rec print_typ fmt = function
-      | Tvar x -> fprintf fmt "%s" x
-      | Tid ("int", []) -> fprintf fmt "Z"
-      | Tid (x, []) -> fprintf fmt "%s" x
-      | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t
-      | Tid (x,tl) ->
-	  fprintf fmt "(%s %a)" x (print_list comma print_typ) tl
-
-    let rec print_term fmt = function
-      | Cst n ->
-	  fprintf fmt "%s" (Big_int.string_of_big_int n)
-      | RCst s ->
-          fprintf fmt "%s" (Big_int.string_of_big_int s)
-      | Power2 n ->
-          fprintf fmt "@[(powerRZ 2 %s)@]" (Big_int.string_of_big_int n)
-
-          (* TODO: bug, it might be operations on reals *)
-      | Plus (a, b) ->
-	  fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b
-      | Moins (a, b) ->
-	  fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b
-      | Mult (a, b) ->
-	  fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b
-      | Div (a, b) ->
-	  fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b
-      | Opp (a) ->
-	  fprintf fmt "@[(Zopp %a)@]" print_term a
-      | App (id, []) ->
-	  fprintf fmt "%s" id
-      | App (id, tl) ->
-	  fprintf fmt "@[(%s %a)@]" id print_terms tl
-
-    and print_terms fmt tl =
-      print_list space print_term fmt tl
-
-    (* builds the text for "forall vars, f vars = t" *)
-    let fun_def_axiom f vars t =
-      let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in
-      fprintf str_formatter
-	"@[(forall %a, %s %a = %a)@]@."
-	(print_list space binder) vars f
-	(print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars
-	print_term t;
-      flush_str_formatter ()
-
-  end
-
-  let prove_axiom id = match Dp_why.find_proof id with
-    | Immediate t ->
-	exact_check t
-    | Fun_def (f, vars, ty, t) ->
-	tclTHENS
-	  (fun gl ->
-	     let s = Coq.fun_def_axiom f vars t in
-	     if !debug then Format.eprintf "axiom fun def = %s@." s;
-	     let c = constr_of_string gl s in
-	     assert_tac (Name (id_of_string id)) c gl)
-	  [tclTHEN intros reflexivity; tclIDTAC]
-
-  let exact_string s gl =
-    let c = constr_of_string gl s in
-    exact_check c gl
-
-  let interp_zenon_proof (ll,p) =
-    let interp_lemma l gl =
-      let ty = constr_of_string gl l.l_type in
-      tclTHENS
-	(assert_tac (Name (id_of_string l.l_id)) ty)
-	[exact_string l.l_proof; tclIDTAC]
-	gl
-    in
-    tclTHEN (tclMAP interp_lemma ll) (exact_string p)
-
-  let proof_from_file f =
-    axioms := [];
-    msgnl (str "proof_from_file " ++ str f);
-    let zp = read_zenon_proof f in
-    msgnl (str "proof term is " ++ str (snd zp));
-    tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp)
-
-}
diff --git a/plugins/dp/fol.mli b/plugins/dp/fol.mli
deleted file mode 100644
index 4fb763a6..00000000
--- a/plugins/dp/fol.mli
+++ /dev/null
@@ -1,58 +0,0 @@
-
-(* Polymorphic First-Order Logic (that is Why's input logic) *)
-
-type typ =
-  | Tvar of string
-  | Tid of string * typ list
-
-type term =
-  | Cst of Big_int.big_int
-  | RCst of Big_int.big_int
-  | Power2 of Big_int.big_int
-  | Plus of term * term
-  | Moins of term * term
-  | Mult of term * term
-  | Div of term * term
-  | Opp of term
-  | App of string * term list
-
-and atom =
-  | Eq of term * term
-  | Le of term * term
-  | Lt of term * term
-  | Ge of term * term
-  | Gt of term * term
-  | Pred of string * term list
-
-and form =
-  | Fatom of atom
-  | Imp of form * form
-  | Iff of form * form
-  | And of form * form
-  | Or of form * form
-  | Not of form
-  | Forall of string * typ * form
-  | Exists of string * typ * form
-  | True
-  | False
-
-(* the integer indicates the number of type variables *)
-type decl =
-  | DeclType of string * int
-  | DeclFun of string * int * typ list * typ
-  | DeclPred of string * int * typ list
-  | Axiom of string * form
-
-type query = decl list * form
-
-
-(* prover result *)
-
-type prover_answer =
-  | Valid of string option
-  | Invalid
-  | DontKnow
-  | Timeout
-  | NoAnswer
-  | Failure of string
-
diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
deleted file mode 100644
index 001ccce8..00000000
--- a/plugins/dp/g_dp.ml4
+++ /dev/null
@@ -1,77 +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*)
-
-open Dp
-
-TACTIC EXTEND Simplify
-  [ "simplify" ] -> [ simplify ]
-END
-
-TACTIC EXTEND Ergo
-  [ "ergo" ] -> [ ergo ]
-END
-
-TACTIC EXTEND Yices
-  [ "yices" ] -> [ yices ]
-END
-
-TACTIC EXTEND CVC3
-  [ "cvc3" ] -> [ cvc3 ]
-END
-
-TACTIC EXTEND Z3
-  [ "z3" ] -> [ z3 ]
-END
-
-TACTIC EXTEND CVCLite
-  [ "cvcl" ] -> [ cvc_lite ]
-END
-
-TACTIC EXTEND Harvey
-  [ "harvey" ] -> [ harvey ]
-END
-
-TACTIC EXTEND Zenon
-  [ "zenon" ] -> [ zenon ]
-END
-
-TACTIC EXTEND Gwhy
-  [ "gwhy" ] -> [ gwhy ]
-END
-
-(* should be part of basic tactics syntax *)
-TACTIC EXTEND admit
-  [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
-END
-
-VERNAC COMMAND EXTEND Dp_hint
-  [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ]
-END
-
-VERNAC COMMAND EXTEND Dp_timeout
-| [ "Dp_timeout" natural(n) ] -> [ dp_timeout n ]
-END
-
-VERNAC COMMAND EXTEND Dp_prelude
-| [ "Dp_prelude" string_list(l) ] -> [ dp_prelude l ]
-END
-
-VERNAC COMMAND EXTEND Dp_predefined
-| [ "Dp_predefined" global(g) "=>" string(s) ] -> [ dp_predefined g s ]
-END
-
-VERNAC COMMAND EXTEND Dp_debug
-| [ "Dp_debug" ] -> [ dp_debug true; Dp_zenon.set_debug true ]
-END
-
-VERNAC COMMAND EXTEND Dp_trace
-| [ "Dp_trace" ] -> [ dp_trace true ]
-END
-
diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v
deleted file mode 100644
index ce660052..00000000
--- a/plugins/dp/test2.v
+++ /dev/null
@@ -1,80 +0,0 @@
-Require Import ZArith.
-Require Import Classical.
-Require Import List.
-
-Open Scope list_scope.
-Open Scope Z_scope.
-
-Dp_debug.
-Dp_timeout 3.
-Require Export zenon.
-
-Definition neg (z:Z) : Z := match z with
-  | Z0 => Z0
-  | Zpos p => Zneg p
-  | Zneg p => Zpos p
-  end.
-
-Goal forall z, neg (neg z) = z.
-  Admitted.
-
-Open Scope nat_scope.
-Print plus.
-
-Goal forall x, x+0=x.
-  induction x; ergo.
-  (* simplify resoud le premier, pas le second *)
-  Admitted.
-
-Goal 1::2::3::nil = 1::2::(1+2)::nil.
-  zenon.
-  Admitted.
-
-Definition T := nat.
-Parameter fct : T -> nat.
-Goal fct O = O.
- Admitted.
-
-Fixpoint even (n:nat) : Prop :=
-  match n with
-  O => True
-  | S O => False
-  | S (S p) => even p
-  end.
-
-Goal even 4%nat.
-  try zenon.
-  Admitted.
-
-Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil.
-
-Definition head :=
-fun (A : Set) (l : list A) =>
-match l with
-| nil => None (A:=A)
-| x :: _ => Some x
-end.
-
-Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
-
-Admitted.
-
-(*
-BUG avec head prédéfini : manque eta-expansion sur A:Set
-
-Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
-
-Print value.
-Print Some.
-
-zenon.
-*)
-
-Inductive IN (A:Set) : A -> list A -> Prop :=
-  | IN1 : forall x l, IN A x (x::l)
-  | IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
-Arguments IN [A] _ _.
-
-Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
-  zenon.
-Print In.
diff --git a/plugins/dp/tests.v b/plugins/dp/tests.v
deleted file mode 100644
index dc85d2ee..00000000
--- a/plugins/dp/tests.v
+++ /dev/null
@@ -1,300 +0,0 @@
-
-Require Import ZArith.
-Require Import Classical.
-Require Export Reals.
-
-
-(* real numbers *)
-
-Lemma real_expr: (0 <= 9 * 4)%R.
-ergo.
-Qed.
-
-Lemma powerRZ_translation: (powerRZ 2 15 < powerRZ 2 17)%R.
-ergo.
-Qed.
-
-Dp_debug.
-Dp_timeout 3.
-
-(* module renamings *)
-
-Module M.
-  Parameter t : Set.
-End M.
-
-Lemma test_module_0 : forall x:M.t, x=x.
-ergo.
-Qed.
-
-Module N := M.
-
-Lemma test_module_renaming_0 : forall x:N.t, x=x.
-ergo.
-Qed.
-
-Dp_predefined M.t => "int".
-
-Lemma test_module_renaming_1 : forall x:N.t, x=x.
-ergo.
-Qed.
-
-(* Coq lists *)
-
-Require Export List.
-
-Lemma test_pol_0 : forall l:list nat, l=l.
-ergo.
-Qed.
-
-Parameter nlist: list nat -> Prop.
-
-Lemma poly_1 : forall l,  nlist l -> True.
-intros.
-simplify.
-Qed.
-
-(* user lists *)
-
-Inductive list (A:Set) : Set :=
-| nil : list A
-| cons: forall a:A, list A -> list A.
-
-Fixpoint app (A:Set) (l m:list A) {struct l} : list A :=
-match l with
-| nil => m
-| cons a l1 => cons A a (app A l1 m)
-end.
-
-Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True.
-intros; ergo.
-Qed.
-
-(* polymorphism *)
-Require Import List.
-
-Inductive mylist (A:Set) : Set :=
-  mynil : mylist A
-| mycons : forall a:A, mylist A -> mylist A.
-
-Parameter my_nlist: mylist nat -> Prop.
-
- Goal forall l,  my_nlist l -> True.
- intros.
- simplify.
-Qed.
-
-(* First example with the 0 and the equality translated *)
-
-Goal 0 = 0.
-simplify.
-Qed.
-
-(* Examples in the Propositional Calculus
-   and theory of equality *)
-
-Parameter A C : Prop.
-
-Goal A -> A.
-simplify.
-Qed.
-
-
-Goal A -> (A \/ C).
-
-simplify.
-Qed.
-
-
-Parameter x y z : Z.
-
-Goal x = y -> y = z -> x = z.
-ergo.
-Qed.
-
-
-Goal ((((A -> C) -> A) -> A) -> C) -> C.
-
-ergo.
-Qed.
-
-(* Arithmetic *)
-Open Scope Z_scope.
-
-Goal 1 + 1 = 2.
-yices.
-Qed.
-
-
-Goal 2*x + 10 = 18 -> x = 4.
-
-simplify.
-Qed.
-
-
-(* Universal quantifier *)
-
-Goal (forall (x y : Z), x = y) -> 0=1.
-try zenon.
-ergo.
-Qed.
-
-Goal forall (x: nat), (x + 0 = x)%nat.
-
-induction x0; ergo.
-Qed.
-
-
-(* No decision procedure can solve this problem
-  Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a.
-*)
-
-
-(* Functions definitions *)
-
-Definition fst (x y : Z) : Z := x.
-
-Goal forall (g : Z -> Z) (x y : Z), g (fst x y) = g x.
-
-simplify.
-Qed.
-
-
-(* Eta-expansion example *)
-
-Definition snd_of_3 (x y z : Z) : Z := y.
-
-Definition f : Z -> Z -> Z := snd_of_3 0.
-
-Goal forall (x y z z1 : Z), snd_of_3 x y z = f y z1.
-
-simplify.
-Qed.
-
-
-(* Inductive types definitions - call to dp/injection function *)
-
-Inductive even : Z -> Prop :=
-| even_0 : even 0
-| even_plus2 : forall z : Z, even z -> even (z + 2).
-
-
-(* Simplify and Zenon can't prove this goal before the timeout
-   unlike CVC Lite *)
-
-Goal even 4.
-ergo.
-Qed.
-
-
-Definition skip_z (z : Z) (n : nat) := n.
-
-Definition skip_z1 := skip_z.
-
-Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n.
-yices.
-Qed.
-
-
-(* Axioms definitions and dp_hint *)
-
-Parameter add : nat -> nat -> nat.
-Axiom add_0 : forall (n : nat), add 0%nat n = n.
-Axiom add_S : forall (n1 n2 : nat), add (S n1) n2 = S (add n1 n2).
-
-Dp_hint add_0.
-Dp_hint add_S.
-
-(* Simplify can't prove this goal before the timeout
-   unlike zenon *)
-
-Goal forall n : nat, add n 0 = n.
-induction n ; yices.
-Qed.
-
-
-Definition pred (n : nat) : nat := match n with
-  | 0%nat => 0%nat
-  | S n' => n'
-end.
-
-Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat.
-yices.
-(*zenon.*)
-Qed.
-
-
-Fixpoint plus (n m : nat) {struct n} : nat :=
-  match n with
-  | 0%nat => m
-  | S n' => S (plus n' m)
-end.
-
-Goal forall n : nat, plus n 0%nat = n.
-
-induction n; ergo.
-Qed.
-
-
-(* Mutually recursive functions *)
-
-Fixpoint even_b (n : nat) : bool := match n with
-  | O => true
-  | S m => odd_b m
-end
-with odd_b (n : nat) : bool := match n with
-  | O => false
-  | S m => even_b m
-end.
-
-Goal even_b (S (S O)) = true.
-ergo.
-(*
-simplify.
-zenon.
-*)
-Qed.
-
-
-(* sorts issues *)
-
-Parameter foo : Set.
-Parameter ff : nat -> foo -> foo -> nat.
-Parameter g : foo -> foo.
-Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.
-yices.
-(*zenon.*)
-Qed.
-
-
-
-(* abstractions *)
-
-Parameter poly_f : forall A:Set, A->A.
-
-Goal forall x:nat, poly_f nat x = poly_f nat x.
-ergo.
-(*zenon.*)
-Qed.
-
-
-
-(* Anonymous mutually recursive functions : no equations are produced
-
-Definition mrf :=
-  fix even2 (n : nat) : bool := match n with
-    | O => true
-    | S m => odd2 m
-  end
-  with odd2 (n : nat) : bool := match n with
-    | O => false
-    | S m => even2 m
-  end for even.
-
-   Thus this goal is unsolvable
-
-Goal mrf (S (S O)) = true.
-
-zenon.
-
-*)
diff --git a/plugins/dp/vo.itarget b/plugins/dp/vo.itarget
deleted file mode 100644
index 4d282709..00000000
--- a/plugins/dp/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Dp.vo
diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v
deleted file mode 100644
index 89028c4f..00000000
--- a/plugins/dp/zenon.v
+++ /dev/null
@@ -1,92 +0,0 @@
-(*  Copyright 2004 INRIA  *)
-Require Export Classical.
-
-Lemma zenon_nottrue :
-  (~True -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_noteq : forall (T : Type) (t : T),
-  ((t <> t) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_and : forall P Q : Prop,
-  (P -> Q -> False) -> (P /\ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_or : forall P Q : Prop,
-  (P -> False) -> (Q -> False) -> (P \/ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_imply : forall P Q : Prop,
-  (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_equiv : forall P Q : Prop,
-  (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notand : forall P Q : Prop,
-  (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notor : forall P Q : Prop,
-  (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notimply : forall P Q : Prop,
-  (P -> ~Q -> False) -> (~(P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notequiv : forall P Q : Prop,
-  (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
-  (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
-  ((P t) -> False) -> ((forall x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
-  (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
-  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
-Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
-
-Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
-Proof. auto. Qed.
-
-Lemma zenon_equal_step :
-  forall (S T : Type) (fa fb : S -> T) (a b : S),
-  (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
-Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
-
-Lemma zenon_pnotp : forall P Q : Prop,
-  (P = Q) -> (P -> ~Q -> False).
-Proof. intros P Q Ha. rewrite Ha. auto. Qed.
-
-Lemma zenon_notequal : forall (T : Type) (a b : T),
-  (a = b) -> (a <> b -> False).
-Proof. auto. Qed.
-
-Ltac zenon_intro id :=
-  intro id || let nid := fresh in (intro nid; clear nid)
-.
-
-Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
-Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
-Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
-Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
-Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
-Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
-Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
-Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
-Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
-Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
-
-Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
-Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 73062328..83ebb139 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -155,7 +155,9 @@ let factor_fix env l cb msb =
 	 function
 	   | (l,SFBconst cb') ->
 	       let check' = check_fix env cb' (j+1) in
-	       if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible;
+	       if not (fst check = fst check' &&
+		   prec_declaration_equal (snd check) (snd check'))
+	       then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
     labels, recd, msb''
@@ -196,13 +198,14 @@ let rec msid_of_seb = function
   | SEBwith (seb,_) -> msid_of_seb seb
   | _ -> assert false
 
-let env_for_mtb_with env mp seb idl =
+let env_for_mtb_with_def env mp seb idl =
   let sig_b = match seb with
     | SEBstruct(sig_b) -> sig_b
     | _ -> assert false
   in
   let l = label_of_id (List.hd idl) in
-  let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in
+  let spot = function (l',SFBconst _) -> l = l' | _ -> false in
+  let before = fst (list_split_when spot sig_b) in
   Modops.add_signature mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
@@ -241,7 +244,7 @@ let rec extract_sfb_spec env mp = function
 and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
   | SEBident mp -> Visit.add_mp_all mp; MTident mp
   | SEBwith(seb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
+      let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in
       let mt = extract_seb_spec env mp1 (seb,seb') in
       (match extract_with_type env' cb with (* cb peut contenir des kn  *)
 	 | None -> mt
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9e8dd828..4e0dbcab 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -194,6 +194,15 @@ let signature_of_structure s =
 
 (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
 
+let is_modular = function
+  | SEdecl _ -> false
+  | SEmodule _ | SEmodtype _ -> true
+
+let rec search_structure l m = function
+  | [] -> raise Not_found
+  | (lab,d)::_ when lab=l && is_modular d = m -> d
+  | _::fields -> search_structure l m fields
+
 let get_decl_in_structure r struc =
   try
     let base_mp,ll = labels_of_ref r in
@@ -202,7 +211,7 @@ let get_decl_in_structure r struc =
     let rec go ll sel = match ll with
       | [] -> assert false
       | l :: ll ->
-	  match List.assoc l sel with
+	  match search_structure l (ll<>[]) sel with
 	    | SEdecl d -> d
 	    | SEmodtype m -> assert false
 	    | SEmodule m ->
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 4a38c48d..034dc3c2 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -134,8 +134,6 @@ TACTIC EXTEND firstorder
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
       [ gen_ground_tac true (Option.map eval_tactic t) l l' ]
-|   [ "firstorder" tactic_opt(t) ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) [] [] ]
 END
 
 TACTIC EXTEND gintuition
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1d1e4a2a..33d77568 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1371,7 +1371,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 (* 		 let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
 (* 		 rewrite *)
 (* 	      ) *)
-	      Eauto.gen_eauto false (false,5) [] (Some [])
+	      Eauto.gen_eauto (false,5) [] (Some [])
 	    ]
 	    gls
 
@@ -1449,7 +1449,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			   (
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
-				      false
 				      (true,5)
 				      [Evd.empty,Lazy.force refl_equal]
 				      [Auto.Hint_db.empty empty_transparent_state false]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 123399d5..06abb8ce 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna
 let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
   (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
   (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) =
-  Genarg.create_arg "function_rec_definition_loc"
+  Genarg.create_arg None "function_rec_definition_loc"
 VERNAC COMMAND EXTEND Function
    ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
 	[
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0b04a572..95ca86c2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -588,15 +588,15 @@ let rec reflexivity_with_destruct_cases g =
     )
   in
   (tclFIRST
-    [ reflexivity;
-      tclTHEN (tclPROGRESS discr_inject) (destruct_case ());
+    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity;
+      observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
       (*  We reach this point ONLY if
 	  the same value is matched (at least) two times
 	  along binding path.
 	  In this case, either we have a discriminable hypothesis and we are done,
 	  either at least an injectable one and we do the injection before continuing
       *)
-      tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases
+      observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases)
     ])
     g
 
@@ -752,6 +752,7 @@ let do_save () = Lemmas.save_named false
 *)
 
 let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
+  let previous_state = States.freeze () in
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let funs_constr = Array.map mkConst funs  in
   try
@@ -793,22 +794,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Lemmas.start_proof
-	   (*i The next call to mk_correct_id is valid since we are constructing the lemma
+	 (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
-	     i*)
-	   (mk_correct_id f_id)
+	 i*)
+	 let lem_id = mk_correct_id f_id in
+	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
-	 Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
+	 Pfedit.by
+	   (observe_tac ("prove correctness ("^(string_of_id f_id)^")")
+	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
-	 update_Function
-	   {finfo with
-	      correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id)))
-	   }
-
+	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
+	 update_Function {finfo with correctness_lemma = Some lem_cst}
       )
       funs;
     let lemmas_types_infos =
@@ -845,34 +845,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Lemmas.start_proof
-	   (*i The next call to mk_complete_id is valid since we are constructing the lemma
+	 (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
-	     i*)
-	   (mk_complete_id f_id)
+	   i*)
+	 let lem_id = mk_complete_id f_id in
+	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
-	 Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
+	 Pfedit.by
+	   (observe_tac ("prove completeness ("^(string_of_id f_id)^")")
+	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
-	 update_Function
-	   {finfo with
-	      completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id)))
-	   }
+	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
+	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs;
   with e ->
     (* In case of problem, we reset all the lemmas *)
-    (*i The next call to mk_correct_id is valid since we are erasing the lemmas
-      Ensures by: obvious
-      i*)
-    let first_lemma_id =
-      let f_id = id_of_label (con_label funs.(0)) in
-
-      mk_correct_id f_id
-    in
-     ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ());
+    Pfedit.delete_all_proofs ();
+    States.unfreeze previous_state;
     raise e
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 55ebd31b..3355300e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -48,7 +48,8 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+    (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
@@ -232,18 +233,19 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
   | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[])
   | Var(_) when eq_constr expr f -> errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function")
   | Var(id) -> (fun l -> expr), []
-  | Meta(_) -> error "find_call_occs : Meta"
-  | Evar(_) -> error "find_call_occs : Evar"
+  | Meta(_) -> error "Found a metavariable. Can not treat such a term" 
+  | Evar(_) -> error "Found an evar. Can not treat such a term"
   | Sort(_)  -> (fun l -> expr), []
   | Cast(b,_,_) -> find_call_occs nb_arg nb_lam f b
-  | Prod(_,_,_) -> error "find_call_occs : Prod"
+  | Prod(na,t,b) -> 
+    error "Found a product. Can not treat such a term"
   | Lambda(na,t,b) ->
       begin
 	match find_call_occs nb_arg (succ nb_lam) f b with
 	  | _, [] ->  (* Lambda are authorized as long as they do not contain
 			 recursives calls *)
 	      (fun l -> expr),[]
-	  | _ ->  error "find_call_occs : Lambda"
+	  | _ ->  error "Found a lambda which body contains a recursive call. Such terms are not allowed"
       end
   | LetIn(na,v,t,b) ->
       begin
@@ -254,7 +256,7 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
 	      ((fun  l -> mkLetIn(na,v,t,cf l)),l)
 	  | (cf,(_::_ as l)),(_,[]) ->
 	      ((fun l -> mkLetIn(na,cf l,t,b)), l)
-	  | _ -> error "find_call_occs : LetIn"
+	  | _ -> error "Found a letin with recursive calls in both variable value and body. Such terms are not allowed."
       end
   | Const(_) -> (fun l -> expr), []
   | Ind(_) -> (fun l -> expr), []
@@ -263,8 +265,8 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
       (match find_call_occs nb_arg nb_lam f a with
 	cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
       | _ -> (fun l -> expr),[])
-  | Fix(_) -> error "find_call_occs : Fix"
-  | CoFix(_) -> error "find_call_occs : CoFix";;
+  | Fix(_) -> error "Found a local fixpoint. Can not treat such a term"
+  | CoFix(_) -> error "Found a local cofixpoint : CoFix";;
 
 let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
@@ -896,6 +898,20 @@ let build_and_l l =
   let conj_constr = coq_conj () in
   let mk_and p1 p2 =
     Term.mkApp(and_constr,[|p1;p2|]) in
+  let rec is_well_founded t = 
+    match kind_of_term t with 
+      | Prod(_,_,t') -> is_well_founded t'
+      | App(_,_) -> 
+	let (f,_) = decompose_app t in 
+	eq_constr f (well_founded ())
+      | _ -> assert false
+  in
+  let compare t1 t2 = 
+    let b1,b2= is_well_founded t1,is_well_founded t2 in 
+    if (b1&&b2) || not (b1 || b2) then 0
+    else if b1 && not b2 then 1 else -1
+  in
+  let l = List.sort compare l in 
   let rec f  = function
     | [] -> failwith "empty list of subgoals!"
     | [p] -> p,tclIDTAC,1
@@ -1006,7 +1022,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 			  (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
 			  e_assumption;
 		      Eauto.eauto_with_bases
-			false
 			(true,5)
 			[Evd.empty,delayed_force refl_equal]
 			[Auto.Hint_db.empty empty_transparent_state false]
@@ -1378,6 +1393,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
+  let previous_label = Lib.current_command_label () in
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
@@ -1429,7 +1445,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
-(* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
 	  stop := true;
 	end
     end;
@@ -1461,10 +1476,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       hook
   with e ->
     begin
-      ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
-(*       anomaly "Cannot create termination Lemma" *)
+      (try ignore (Backtrack.backto previous_label) with _ -> ());
+      (*       anomaly "Cannot create termination Lemma" *)
       raise e
     end
-
-
-
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 1ad49bb8..8b7ee55b 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -895,7 +895,9 @@ struct
   let parse_expr parse_constant parse_exp ops_spec env term =
     if debug
     then (Pp.pp (Pp.str "parse_expr: ");
-          Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ());
+          Pp.pp (Printer.prterm term);
+          Pp.pp (Pp.str "\n");
+          Pp.pp_flush ());
 
 (*
     let constant_or_variable env term =
@@ -991,8 +993,12 @@ struct
         else raise ParseError
     | App(op,args) -> 
 	begin
-	  try 
-	    (assoc_const   op rconst_assoc) (rconstant args.(0)) (rconstant args.(1))
+	  try
+            (* the evaluation order is important in the following *)
+            let f = assoc_const op rconst_assoc in
+            let a = rconstant args.(0) in
+            let b = rconstant args.(1) in
+            f a b
 	  with
 	      ParseError -> 
 		match op with
@@ -1009,10 +1015,12 @@ struct
     if debug
     then (Pp.pp_flush ();
           Pp.pp (Pp.str "rconstant: ");
-          Pp.pp (Printer.prterm  term); Pp.pp_flush ());
+          Pp.pp (Printer.prterm  term);
+          Pp.pp (Pp.str "\n");
+          Pp.pp_flush ());
     let res = rconstant term in
       if debug then 
-	(Printf.printf "rconstant -> %a" pp_Rcst res ; flush stdout) ; 
+	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
       res
 
 
@@ -1052,6 +1060,7 @@ struct
    then (Pp.pp_flush ();
          Pp.pp (Pp.str "parse_arith: ");
          Pp.pp (Printer.prterm  cstr);
+         Pp.pp (Pp.str "\n");
          Pp.pp_flush ());
    match kind_of_term cstr with
     | App(op,args) ->
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index e48643b4..a317307e 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -474,7 +474,7 @@ let remove_zeros zero lci =
 	done;
 	!lcr)
       lr in
-  info ("unuseful spolynomials: "
+  info ("useless spolynomials: "
 	^string_of_int (m-List.length lr)^"\n");
   info ("useful spolynomials: "
 	^string_of_int (List.length lr)^"\n");
diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
index 04cbdccb..787995ed 100644
--- a/plugins/pluginsbyte.itarget
+++ b/plugins/pluginsbyte.itarget
@@ -8,7 +8,6 @@ fourier/fourier_plugin.cma
 romega/romega_plugin.cma
 omega/omega_plugin.cma
 micromega/micromega_plugin.cma
-dp/dp_plugin.cma
 xml/xml_plugin.cma
 subtac/subtac_plugin.cma
 ring/ring_plugin.cma
diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget
index bbadfe69..bd3cec01 100644
--- a/plugins/pluginsdyn.itarget
+++ b/plugins/pluginsdyn.itarget
@@ -8,7 +8,6 @@ fourier/fourier_plugin.cmxs
 romega/romega_plugin.cmxs
 omega/omega_plugin.cmxs
 micromega/micromega_plugin.cmxs
-dp/dp_plugin.cmxs
 xml/xml_plugin.cmxs
 subtac/subtac_plugin.cmxs
 ring/ring_plugin.cmxs
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index 74b3f527..5264ba37 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -8,7 +8,6 @@ fourier/fourier_plugin.cmxa
 romega/romega_plugin.cmxa
 omega/omega_plugin.cmxa
 micromega/micromega_plugin.cmxa
-dp/dp_plugin.cmxa
 xml/xml_plugin.cmxa
 subtac/subtac_plugin.cmxa
 ring/ring_plugin.cmxa
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index db56534c..bab15ad0 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -1,4 +1,3 @@
-dp/vo.otarget
 field/vo.otarget
 fourier/vo.otarget
 funind/vo.otarget
@@ -10,4 +9,4 @@ ring/vo.otarget
 romega/vo.otarget
 rtauto/vo.otarget
 setoid_ring/vo.otarget
-extraction/vo.otarget
\ No newline at end of file
+extraction/vo.otarget
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d773b153..576f7d4e 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -509,8 +509,8 @@ let pp_gl gl= cut () ++
 
 let pp =
   function
-      Incomplete(gl,ctx) -> msgnl (pp_gl gl)
-    | _ -> msg (str "<complete>")
+      Incomplete(gl,ctx) -> pp_gl gl ++ fnl ()
+    | _ -> str "<complete>"
 
 let pp_info () =
   let count_info =
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index b236aa72..275e94cd 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -38,7 +38,7 @@ val branching: state -> state list
 
 val success: state -> bool
 
-val pp: state -> unit
+val pp: state -> Pp.std_ppcmds
 
 val pr_form : form -> unit
 
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 5ed335d0..f4d8b769 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -132,18 +132,29 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let evar_dependencies evm ev =
+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
-	Intset.union (Evarutil.evars_of_evar_info evi) s)
+      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 ev)
+  in aux (Intset.singleton oev)
       
 let move_after (id, ev, deps as obl) l = 
   let rec aux restdeps = function
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ca1240e5..6a131d39 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -75,14 +75,14 @@ type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstra
 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"
+  Genarg.create_arg None "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"
+  Genarg.create_arg None "subtac_withtac"
 
 VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 710149ae..d626396f 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -82,11 +82,9 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
       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 ()
+  Vernacentries.print_subgoals ()
 
 let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
 
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 368d8bac..16d4e21e 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1845,7 +1845,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 			 refl_arg :: refl_args,
 			 pred slift,
 			 (Name id, b, t) :: argsign'))
-		   (env, 0, [], [], slift, []) args argsign
+		   (env, neqs, [], [], slift, []) args argsign
 	       in
 	       let eq = mk_JMeq
 		 (lift (nargeqs + slift) appt)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index c08dd16d..6b3fe718 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -52,7 +52,7 @@ let type_ctx_instance evars env ctx inst subst =
 	| 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;
+       evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
        let d = na, Some c', t' in
 	aux (c' :: subst, d :: instctx) l ctx
     | [] -> subst
@@ -107,9 +107,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	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 := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~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
-  evars := Evarutil.nf_evar_map !evars;
-  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
   let props =
@@ -157,6 +158,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	    Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
   in	  
   evars := Evarutil.nf_evar_map !evars;
+  evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
+  evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env !evars;
   let term, termtype =
     match subst with
     | Inl subst ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 74f31a90..eb29bd04 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -27,6 +27,9 @@ open Subtac_errors
 open Eterm
 open Pp
 
+let app_opt env evars f t =
+  whd_betaiota !evars (app_opt f t)
+
 let pair_of_array a = (a.(0), a.(1))
 let make_name s = Name (id_of_string s)
 
@@ -80,7 +83,8 @@ module Coercion = struct
       | Type _, Prop Null -> Prop Null
       | _, Type _ -> s2
 
-  let hnf env isevars c = whd_betadeltaiota env ( !isevars) c
+  let hnf env isevars c = whd_betadeltaiota env isevars c
+  let hnf_nodelta env evars c = whd_betaiota evars c
 
   let lift_args n sign =
     let rec liftrec k = function
@@ -90,15 +94,16 @@ module Coercion = struct
       liftrec (List.length sign) sign
 
   let rec mu env isevars t =
-    let isevars = ref isevars in
     let rec aux v =
-      let v = hnf env isevars v in
+      let v = hnf env !isevars v in
       match disc_subset v with
 	  Some (u, p) ->
 	    let f, ct = aux u in
+	    let p = hnf env !isevars p in
 	      (Some (fun x ->
-		       app_opt f (mkApp ((delayed_force sig_).proj1,
-					 [| u; p; x |]))),
+		     app_opt env isevars 
+		     f (mkApp ((delayed_force sig_).proj1,
+			       [| u; p; x |]))),
 	       ct)
 	| None -> (None, v)
     in aux t
@@ -106,9 +111,8 @@ module Coercion = struct
   and coerce loc env isevars (x : Term.constr) (y : Term.constr)
       : (Term.constr -> Term.constr) option
       =
-    let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
     let rec coerce_unify env x y =
-      let x = hnf env isevars x and y = hnf env isevars y in
+      let x = hnf env !isevars x and y = hnf env !isevars y in
 	try
 	  isevars := the_conv_x_leq env x y !isevars;
 	  None
@@ -167,7 +171,7 @@ module Coercion = struct
 	      let env' = push_rel (name', None, a') env in
 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 		(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
-	      let coec1 = app_opt c1 (mkRel 1) in
+	      let coec1 = app_opt env' isevars c1 (mkRel 1) in
 		(* env, x : a' |- c1[x] : lift 1 a *)
 	      let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
 		(* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
@@ -177,7 +181,7 @@ module Coercion = struct
 		    Some
 		      (fun f ->
 			mkLambda (name', a',
-				 app_opt c2
+				 app_opt env' isevars c2
 				   (mkApp (Term.lift 1 f, [| coec1 |])))))
 
 	  | App (c, l), App (c', l') ->
@@ -220,9 +224,9 @@ module Coercion = struct
 				     Some
 				       (fun x ->
 					  let x, y =
-					    app_opt c1 (mkApp (existS.proj1,
+					    app_opt env' isevars c1 (mkApp (existS.proj1,
 							       [| a; pb; x |])),
-					    app_opt c2 (mkApp (existS.proj2,
+					    app_opt env' isevars c2 (mkApp (existS.proj2,
 							       [| a; pb; x |]))
 					  in
 					    mkApp (existS.intro, [| a'; pb'; x ; y |]))
@@ -240,9 +244,9 @@ module Coercion = struct
 				     Some
 				       (fun x ->
 					  let x, y =
-					    app_opt c1 (mkApp (prod.proj1,
+					    app_opt env isevars c1 (mkApp (prod.proj1,
 							       [| a; b; x |])),
-					    app_opt c2 (mkApp (prod.proj2,
+					    app_opt env isevars c2 (mkApp (prod.proj2,
 							       [| a; b; x |]))
 					  in
 					    mkApp (prod.intro, [| a'; b'; x ; y |]))
@@ -276,7 +280,7 @@ module Coercion = struct
 	  Some (u, p) ->
 	    let c = coerce_unify env u y in
 	    let f x =
-	      app_opt c (mkApp ((delayed_force sig_).proj1,
+	      app_opt env isevars c (mkApp ((delayed_force sig_).proj1,
 				[| u; p; x |]))
 	    in Some f
 	| None ->
@@ -285,7 +289,7 @@ module Coercion = struct
 		  let c = coerce_unify env x u in
 		    Some
 		      (fun x ->
-			 let cx = app_opt c x in
+			 let cx = app_opt env isevars c x in
 			 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
 			 in
 			   (mkApp
@@ -300,7 +304,8 @@ module Coercion = struct
   let coerce_itf loc env isevars v t c1 =
     let evars = ref isevars in
     let coercion = coerce loc env evars t c1 in
-      !evars, Option.map (app_opt coercion) v
+    let t = Option.map (app_opt env evars coercion) v in
+      !evars, t
 
   (* Taken from pretyping/coercion.ml *)
 
@@ -354,34 +359,36 @@ module Coercion = struct
     with _ -> anomaly "apply_coercion"
 
   let inh_app_fun env isevars j =
-    let t = whd_betadeltaiota env ( isevars) j.uj_type in
+    let isevars = ref isevars in
+    let t = hnf env !isevars j.uj_type in
       match kind_of_term t with
-	| Prod (_,_,_) -> (isevars,j)
-	| Evar ev when not (is_defined_evar isevars ev) ->
-	    let (isevars',t) = define_evar_as_product isevars ev in
+	| Prod (_,_,_) -> (!isevars,j)
+	| Evar ev when not (is_defined_evar !isevars ev) ->
+	    let (isevars',t) = define_evar_as_product !isevars ev in
 	      (isevars',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
       	       let t,p =
-		 lookup_path_to_fun_from env ( isevars) j.uj_type in
-		 (isevars,apply_coercion env ( isevars) p j t)
+		 lookup_path_to_fun_from env !isevars j.uj_type in
+		 (!isevars,apply_coercion env !isevars p j t)
 	     with Not_found ->
 	       try
 		 let coercef, t = mu env isevars t in
-		   (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
+		 let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in
+		   (!isevars, res)
 	       with NoSubtacCoercion | NoCoercion ->
-		 (isevars,j))
+		 (!isevars,j))
 
   let inh_tosort_force loc env isevars j =
     try
       let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
       let j1 = apply_coercion env ( isevars) p j t in
-	(isevars,type_judgment env (j_nf_evar ( isevars) j1))
+	(isevars, type_judgment env (j_nf_evar ( isevars) j1))
     with Not_found ->
       error_not_a_type_loc loc env ( isevars) j
 
   let inh_coerce_to_sort loc env isevars j =
-    let typ = whd_betadeltaiota env ( isevars) j.uj_type in
+    let typ = hnf env isevars j.uj_type in
       match kind_of_term typ with
 	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
 	| Evar ev when not (is_defined_evar isevars ev) ->
@@ -391,15 +398,19 @@ module Coercion = struct
 	    inh_tosort_force loc env isevars j
 
   let inh_coerce_to_base loc env isevars j =
-    let typ = whd_betadeltaiota env ( isevars) j.uj_type in
+    let isevars = ref isevars in
+    let typ = hnf env !isevars j.uj_type in
     let ct, typ' = mu env isevars typ in
-      isevars, { uj_val = app_opt ct j.uj_val;
-		 uj_type = typ' }
+    let res =
+      { uj_val = app_opt env isevars ct j.uj_val;
+	uj_type = typ' }
+    in !isevars, res
 
   let inh_coerce_to_prod loc env isevars t =
-    let typ = whd_betadeltaiota env ( isevars) (snd t) in
+    let isevars = ref isevars in
+    let typ = hnf env !isevars (snd t) in
     let _, typ' = mu env isevars typ in
-      isevars, (fst t, typ')
+      !isevars, (fst t, typ')
 
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
@@ -452,23 +463,23 @@ module Coercion = struct
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
     match n with
-	None ->
-	  let (evd', val') =
-	    try
-	      inh_conv_coerce_to_fail loc env evd rigidonly
-		(Some (nf_evar evd cj.uj_val))
-		(nf_evar evd cj.uj_type) (nf_evar evd t)
-	    with NoCoercion ->
-	      let sigma =  evd in
-		try
-		  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
-		with NoSubtacCoercion ->
-		  error_actual_type_loc loc env sigma cj t
-	  in
-	  let val' = match val' with Some v -> v | None -> assert(false) in
-	    (evd',{ uj_val = val'; uj_type = t })
-      | Some (init, cur) ->
-	  (evd, cj)
+    | None ->
+      let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } 
+      and t = hnf_nodelta env evd t in
+      let (evd', val') =
+	try
+	  inh_conv_coerce_to_fail loc env evd rigidonly
+	  (Some cj.uj_val) cj.uj_type t
+	with NoCoercion ->
+	(try
+	   coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
+	 with NoSubtacCoercion ->
+	   error_actual_type_loc loc env evd cj t)
+      in
+      let val' = match val' with Some v -> v | None -> assert(false) in
+	(evd',{ uj_val = val'; uj_type = t })
+    | Some (init, cur) ->
+      (evd, cj)
 
   let inh_conv_coerce_to = inh_conv_coerce_to_gen false
   let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index ecae6759..ced390aa 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -458,7 +458,7 @@ let interp_recursive fixkind l =
   (* 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
+    ~filter:Typeclasses.no_goals ~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
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 64d9f72c..6a5878b3 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -445,12 +445,12 @@ let deps_remaining obls deps =
       else x :: acc)
     deps []
 
-let has_dependencies obls n =
-  let res = ref false in
+let dependencies obls n =
+  let res = ref Intset.empty in
     Array.iteri
       (fun i obl ->
 	if i <> n && Intset.mem n obl.obl_deps then
-	  res := true)
+	  res := Intset.add i !res)
       obls;
     !res
 
@@ -502,8 +502,9 @@ let rec solve_obligation prg num tac =
 		in
 		  match res with
 		  | Remain n when n > 0 ->
-		      if has_dependencies obls num then
-			ignore(auto_solve_obligations (Some prg.prg_name) None)
+		      let deps = dependencies obls num in
+			if deps <> Intset.empty then
+			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
 		  | _ -> ());
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
@@ -553,14 +554,18 @@ and solve_obligation_by_tac prg obls i tac =
 	| Util.Anomaly _ as e -> raise e
 	| e -> false
 
-and solve_prg_obligations prg tac =
+and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
   let obls' = Array.copy obls in
+  let p = match oblset with
+    | None -> (fun _ -> true)
+    | Some s -> (fun i -> Intset.mem i s)
+  in
   let _ =
     Array.iteri (fun i x ->
-		   if solve_obligation_by_tac prg obls' i tac then
-		     decr rem)
+		 if p i && solve_obligation_by_tac prg obls' i tac then
+		   decr rem)
       obls'
   in
     update_obls prg obls' !rem
@@ -582,9 +587,9 @@ and try_solve_obligation n prg tac =
 and try_solve_obligations n tac =
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
-and auto_solve_obligations n tac : progress =
+and auto_solve_obligations n ?oblset tac : progress =
   Flags.if_verbose msgnl (str "Solving obligations automatically...");
-  try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
+  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
 
 open Pp
 let show_obligations_of_prg ?(msg=true) prg =
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 7c0d1232..e56fa4f5 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -67,8 +67,8 @@ let interp env isevars c tycon =
   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 unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~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
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index d5d427c7..9a4e1883 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -88,7 +88,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env evdref j = function
-    | None -> j_nf_evar !evdref j
+    | None -> j
     | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
 
   let push_rels vars env = List.fold_right push_rel vars env
@@ -323,7 +323,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
  	    else tycon
 	  in
 	    match ty with
-	    | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
+	    | Some (_, t) ->
+	      if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty
+	      else None
 	    | _ -> None
 	in
 	let fj = pretype ftycon env evdref lvar f in
@@ -340,13 +342,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
 		      let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
 		      evdref := evd;
-		      let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in
+		      let hj = pretype (mk_tycon c1) env evdref lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
-		      let typ' = nf_evar !evdref typ in
 			apply_rec env (n+1)
-			  { uj_val = nf_evar !evdref value;
-			    uj_type = nf_evar !evdref typ' }
-			  (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest
+			{ uj_val = value;
+			  uj_type = typ }
+			  (Option.map (fun (abs, c) -> abs, c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
@@ -354,9 +355,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (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 = apply_rec env 1 fj ftycon args in
 	let resj =
-	  match kind_of_term resj.uj_val with
+	  match kind_of_term (whd_evar !evdref resj.uj_val) with
 	  | App (f,args) when isInd f or isConst f ->
 	      let sigma =  !evdref in
 	      let c = mkApp (f,Array.map (whd_evar sigma) args) in
@@ -508,10 +509,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  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
-	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
-	    let pi = lift n pred in (* liftn n 2 pred ? *)
+	    let pi = lift n pred in
 	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
 	    let csgn =
 	      if not !allow_anonymous_refs then
@@ -525,7 +525,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		cs.cs_args
 	    in
 	    let env_c = push_rels csgn env in
-(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
 	    let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	  let b1 = f cstrs.(0) b1 in
@@ -551,8 +550,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env evdref lvar t in
 		let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
-		  (* User Casts are for helping pretyping, experimentally not to be kept*)
-		  (* ... except for Correctness *)
 		let v = mkCast (cj.uj_val, k, tj.utj_val) in
 		  { uj_val = v; uj_type = tj.utj_val }
 	in
@@ -600,9 +597,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     in
       if resolve_classes then
 	(try 
-	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+	   evdref := Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations
 	     ~split:true ~fail:true env !evdref;
-	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+	   evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
 	     ~split:true ~fail:false env !evdref
 	 with e -> if fail_evar then raise e else ());
       evdref := consider_remaining_unif_problems env !evdref;
@@ -647,8 +644,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_type sigma env c =
     snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)
 
-  let understand_ltac expand_evar sigma env lvar kind c =
-    ise_pretype_gen expand_evar false true sigma env lvar kind c
+  let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
     ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 28bbdd35..fbb44811 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -161,12 +161,11 @@ 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
+  Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c
+
+let no_goals_or_obligations = function
+  | GoalEvar | QuestionMark _ -> false
+  | _ -> true
 
 let make_existential_expr loc env c =
   let key = Evarutil.new_untyped_evar () in
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index de96cc60..112b1795 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -82,6 +82,7 @@ val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
 val make_existential : loc -> ?opaque:obligation_definition_status ->
   env -> evar_map ref -> types -> constr
+val no_goals_or_obligations : Typeclasses.evar_filter
 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
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 3c3e54fa..56ce7ef2 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -107,7 +107,7 @@ let pr_context_xml env =
 
 let pr_subgoal_metas_xml metas env=
   let pr_one (meta, typ) =
-    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++
+    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++
       str "\"/>"
   in
   List.fold_left (++) (mt ()) (List.map pr_one metas)
@@ -117,7 +117,7 @@ let pr_goal_xml sigma g =
   let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
   if Decl_mode.try_get_info sigma g = None then
     (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
-    xmlstream (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) ++
+    xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++
     str "\"/>" ++
     (pr_context_xml env)) ++
     fnl () ++ str "</goal>")