Here comes the commit, announced long ago, of the new tactic engine.

This is a fairly large commit (around 140 files and 7000 lines of code
impacted), it will cause some troubles for sure (I've listed the know
regressions below, there is bound to be more).
At this state of developpement it brings few features to the user, as
the old tactics were
ported with no change. Changes are on the side of the developer mostly.

Here comes a list of the major changes. I will stay brief, but the code
is hopefully well documented so that it is reasonably easy to infer the
details from it.

Feature developer-side:
* Primitives for a "real" refine tactic (generating a goal for each
evar).
* Abstract type of tactics, goals and proofs
* Tactics can act on several goals (formally all the focused goals). An
interesting consequence of this is that the tactical (. ; [ . | ... ])
can be separated in two
tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for
this particular syntax). We can also imagine a tactic to reorder the
goals.
* Possibility for a tactic to pass a value to following tactics (a
typical example is
an intro function which tells the following tactics which name it
introduced).
* backtracking primitives for tactics (it is now possible to implement a
tactical '+'
  with (a+b);c equivalent to (a;c+b;c) (itself equivalent to
(a;c||b;c)). This is a valuable
  tool to implement tactics like "auto" without nowing of the
implementation of tactics.
* A notion of proof modes, which allows to dynamically change the parser
for tactics. It is controlled at user level with the keywords Set
Default Proof Mode (this is the proof mode which is loaded at the start
of each proof) and Proof Mode (switches the proof mode of the current
proof) to control them.
* A new primitive Evd.fold_undefined which operates like an Evd.fold,
except it only goes through the evars whose body is Evar_empty. This is
a common operation throughout the code,
some of the fold-and-test-if-empty occurences have been replaced by
fold_undefined. For now,
it is only implemented as a fold-and-test, but we expect to have some
optimisations coming some day, as there can be a lot of evars in an
evar_map with this new implementation (I've observed a couple of
thousands), whereas there are rarely more than a dozen undefined ones.
Folding being a linear operation, this might result in a significant
speed-up.
* The declarative mode has been moved into the plugins. This is made
possible by the proof mode feature. I tried to document it so that it
can serve as a tutorial for a tactic mode plugin.

Features user-side:
* Unfocus does not go back to the root of the proof if several Focus-s
have been performed.
  It only goes back to the point where it was last focused.
* experimental (non-documented) support of keywords
BeginSubproof/EndSubproof:
  BeginSubproof focuses on first goal, one can unfocus only with
EndSubproof, and only
  if the proof is completed for that goal.
* experimental (non-documented) support for bullets ('+', '-' and '*')
  they act as hierarchical BeginSubproof/EndSubproof:
  First time one uses '+' (for instance) it focuses on first goal, when
the subproof is
  completed, one can use '+' again which unfocuses and focuses on next
first goal.
  Meanwhile, one cas use '*' (for instance) to focus more deeply.

Known regressions:
* The xml plugin had some functions related to proof trees. As the
structure of proof changed significantly, they do not work anymore.
* I do not know how to implement info or show script in this new engine.
Actually I don't even know what they were suppose to actually mean in
earlier versions either. I wager they would require some calm thinking
before going back to work.
* Declarative mode not entirely working (in particular proofs by
induction need to be restored).
* A bug in the inversion tactic (observed in some contributions)
* A bug in Program (observed in some contributions)
* Minor change in the 'old' type of tactics causing some contributions
to fail.
* Compilation time takes about 10-15% longer for unknown reasons (I
suspect it might be linked to the fact that I don't perform any
reduction at QED-s, and also to some linear operations on evar_map-s
(see Evd.fold_undefined above)).


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

30 files changed, 3262 insertions, 1709 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
new file mode 100644
index 000000000..35db5e6ed
--- /dev/null
+++ b/proofs/clenv.ml
@@ -0,0 +1,488 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Namegen
+open Sign
+open Environ
+open Evd
+open Reduction
+open Reductionops
+open Rawterm
+open Pattern
+open Tacred
+open Pretype_errors
+open Evarutil
+open Unification
+open Mod_subst
+open Coercion.Default
+
+(* Abbreviations *)
+
+let pf_env = Refiner.pf_env
+let pf_hyps = Refiner.pf_hyps
+let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
+let pf_concl = Tacmach.pf_concl
+
+(******************************************************************)
+(* Clausal environments *)
+
+type clausenv = {
+  env      : env;
+  evd      : evar_map;
+  templval : constr freelisted;
+  templtyp : constr freelisted }
+
+let cl_env ce = ce.env
+let cl_sigma ce =  ce.evd
+
+let subst_clenv sub clenv =
+  { templval = map_fl (subst_mps sub) clenv.templval;
+    templtyp = map_fl (subst_mps sub) clenv.templtyp;
+    evd = subst_evar_defs_light sub clenv.evd;
+    env = clenv.env }
+
+let clenv_nf_meta clenv c = nf_meta clenv.evd c
+let clenv_term clenv c = meta_instance clenv.evd c
+let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
+let clenv_value clenv = meta_instance clenv.evd clenv.templval
+let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
+
+
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
+
+let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
+
+exception NotExtensibleClause
+
+let clenv_push_prod cl =
+  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let rec clrec typ = match kind_of_term typ with
+    | Cast (t,_,_) -> clrec t
+    | Prod (na,t,u) ->
+	let mv = new_meta () in
+	let dep = dependent (mkRel 1) u in
+	let na' = if dep then na else Anonymous in
+	let e' = meta_declare mv t ~name:na' cl.evd in
+	let concl = if dep then subst1 (mkMeta mv) u else u in
+	let def = applist (cl.templval.rebus,[mkMeta mv]) in
+	{ templval = mk_freelisted def;
+	  templtyp = mk_freelisted concl;
+	  evd = e';
+	  env = cl.env }
+    | _ -> raise NotExtensibleClause
+  in clrec typ
+
+(* Instantiate the first [bound] products of [t] with metas (all products if
+   [bound] is [None]; unfold local defs *)
+
+let clenv_environments evd bound t =
+  let rec clrec (e,metas) n t =
+    match n, kind_of_term t with
+      | (Some 0, _) -> (e, List.rev metas, t)
+      | (n, Cast (t,_,_)) -> clrec (e,metas) n t
+      | (n, Prod (na,t1,t2)) ->
+	  let mv = new_meta () in
+	  let dep = dependent (mkRel 1) t2 in
+	  let na' = if dep then na else Anonymous in
+	  let e' = meta_declare mv t1 ~name:na' e in
+	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
+	    (if dep then (subst1 (mkMeta mv) t2) else t2)
+      | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
+      | (n, _) -> (e, List.rev metas, t)
+  in
+  clrec (evd,[]) bound t
+
+(* Instantiate the first [bound] products of [t] with evars (all products if
+   [bound] is [None]; unfold local defs *)
+
+let clenv_environments_evars env evd bound t =
+  let rec clrec (e,ts) n t =
+    match n, kind_of_term t with
+      | (Some 0, _) -> (e, List.rev ts, t)
+      | (n, Cast (t,_,_)) -> clrec (e,ts) n t
+      | (n, Prod (na,t1,t2)) ->
+          let e',constr = Evarutil.new_evar e env t1 in
+	  let dep = dependent (mkRel 1) t2 in
+	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
+	    (if dep then (subst1 constr t2) else t2)
+      | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
+      | (n, _) -> (e, List.rev ts, t)
+  in
+  clrec (evd,[]) bound t
+
+let clenv_conv_leq env sigma t c bound =
+  let ty = Retyping.get_type_of env sigma c in
+  let evd = Evd.create_goal_evar_defs sigma in
+  let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
+  let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
+  let evars = Evarconv.consider_remaining_unif_problems env evars in
+  let args = List.map (whd_evar evars) args in
+  check_evars env sigma evars (applist (c,args));
+  args
+
+let mk_clenv_from_env environ sigma n (c,cty) =
+  let evd = create_goal_evar_defs sigma in
+  let (evd,args,concl) = clenv_environments evd n cty in
+  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
+    templtyp = mk_freelisted concl;
+    evd = evd;
+    env = environ }
+
+let mk_clenv_from_n gls n (c,cty) =
+  mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+
+let mk_clenv_from gls = mk_clenv_from_n gls None
+
+let mk_clenv_rename_from_n gls n (c,t) =
+  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
+
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+
+(******************************************************************)
+
+(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
+ * mv0, or if one of the free vars on mv1's freelist mentions
+ * mv0 *)
+
+let mentions clenv mv0 =
+  let rec menrec mv1 =
+    mv0 = mv1 ||
+    let mlist =
+      try match meta_opt_fvalue clenv.evd mv1 with
+      | Some (b,_) -> b.freemetas
+      | None -> Metaset.empty
+      with Not_found -> Metaset.empty in
+    meta_exists menrec mlist
+  in menrec
+
+let error_incompatible_inst clenv mv  =
+  let na = meta_name clenv.evd mv in
+  match na with
+      Name id ->
+        errorlabstrm "clenv_assign"
+          (str "An incompatible instantiation has already been found for " ++
+           pr_id id)
+    | _ ->
+        anomaly "clenv_assign: non dependent metavar already assigned"
+
+(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
+let clenv_assign mv rhs clenv =
+  let rhs_fls = mk_freelisted rhs in
+  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
+    error "clenv_assign: circularity in unification";
+  try
+    if meta_defined clenv.evd mv then
+      if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+        error_incompatible_inst clenv mv
+      else
+	clenv
+    else
+      let st = (ConvUpToEta 0,TypeNotProcessed) in
+      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+  with Not_found ->
+    error "clenv_assign: undefined meta"
+
+
+
+(* [clenv_dependent hyps_only clenv]
+ * returns a list of the metavars which appear in the template of clenv,
+ * and which are dependent, This is computed by taking the metavars in cval,
+ * in right-to-left order, and collecting the metavars which appear
+ * in their types, and adding in all the metavars appearing in the
+ * type of clenv.
+ * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
+
+(* [clenv_metavars clenv mv]
+ * returns a list of the metavars which appear in the type of
+ * the metavar mv.  The list is unordered. *)
+
+let clenv_metavars evd mv =
+  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+
+let dependent_metas clenv mvs conclmetas =
+  List.fold_right
+    (fun mv deps ->
+       Metaset.union deps (clenv_metavars clenv.evd mv))
+    mvs conclmetas
+
+let duplicated_metas c =
+  let rec collrec (one,more as acc) c =
+    match kind_of_term c with
+    | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
+    | _       -> fold_constr collrec acc c
+  in
+  snd (collrec ([],[]) c)
+
+let clenv_dependent hyps_only clenv =
+  let mvs = undefined_metas clenv.evd in
+  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  let nonlinear = duplicated_metas (clenv_value clenv) in
+  (* Make the assumption that duplicated metas have internal dependencies *)
+  List.filter
+    (fun mv -> if Metaset.mem mv deps
+               then not (hyps_only && Metaset.mem mv ctyp_mvs)
+               else List.mem mv nonlinear)
+    mvs
+
+let clenv_missing ce = clenv_dependent true ce
+
+(******************************************************************)
+
+let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+  { clenv with
+      evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd }
+
+let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
+  { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
+
+let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
+  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
+    clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) concl
+      (clenv_unify_meta_types ~flags:flags clenv)
+  else
+    clenv_unify allow_K CUMUL ~flags:flags
+      (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
+
+(* [clenv_pose_metas_as_evars clenv dep_mvs]
+ * For each dependent evar in the clause-env which does not have a value,
+ * pose a value for it by constructing a fresh evar.  We do this in
+ * left-to-right order, so that every evar's type is always closed w.r.t.
+ * metas.
+
+ * Node added 14/4/08 [HH]: before this date, evars were collected in
+   clenv_dependent by collect_metas in the fold_constr order which is
+   (almost) the left-to-right order of dependencies in term. However,
+   due to K-redexes, collect_metas was sometimes missing some metas.
+   The call to collect_metas has been replaced by a call to
+   undefined_metas, but then the order was the one of definition of
+   the metas (numbers in increasing order) which is _not_ the
+   dependency order when a clenv_fchain occurs (because clenv_fchain
+   plugs a term with a list of consecutive metas in place of a - a priori -
+   arbitrary metavariable belonging to another sequence of consecutive metas:
+   e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of
+   (nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2).
+   To ensure the dependency order, we check that the type of each meta
+   to pose is already meta-free, otherwise we postpone the transformation,
+   hoping that no cycle may happen.
+
+   Another approach could have been to use decimal numbers for metas so that
+   in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2)
+   then making the numeric order match the dependency order.
+*)
+
+let clenv_pose_metas_as_evars clenv dep_mvs =
+  let rec fold clenv = function
+  | [] -> clenv
+  | mv::mvs ->
+      let ty = clenv_meta_type clenv mv in
+      (* Postpone the evar-ization if dependent on another meta *)
+      (* This assumes no cycle in the dependencies - is it correct ? *)
+      if occur_meta ty then fold clenv (mvs@[mv])
+      else
+	let (evd,evar) =
+	  new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
+	let clenv = clenv_assign mv evar {clenv with evd=evd} in
+	fold clenv mvs in
+  fold clenv dep_mvs
+
+let evar_clenv_unique_resolver = clenv_unique_resolver
+
+(******************************************************************)
+
+let connect_clenv gls clenv =
+  let evd = Evd.fold begin fun ev evi acc -> 
+                        if evi.evar_body = Evar_empty then
+			  acc
+			else
+			  Evd.add acc ev evi
+                  end
+                  clenv.evd gls.sigma
+  in
+  let evd = evars_reset_evd evd clenv.evd in
+  { clenv with
+    evd = evd ;
+    env = Goal.V82.env evd (sig_it gls) }
+
+(* [clenv_fchain mv clenv clenv']
+ *
+ * Resolves the value of "mv" (which must be undefined) in clenv to be
+ * the template of clenv' be the value "c", applied to "n" fresh
+ * metavars, whose types are chosen by destructing "clf", which should
+ * be a clausale forme generated from the type of "c".  The process of
+ * resolution can cause unification of already-existing metavars, and
+ * of the fresh ones which get created.  This operation is a composite
+ * of operations which pose new metavars, perform unification on
+ * terms, and make bindings.
+
+   Otherwise said, from
+
+     [clenv] = [env;sigma;metas |- c:T]
+     [clenv'] = [env';sigma';metas' |- d:U]
+     [mv] = [mi] of type [Ti] in [metas]
+
+   then, if the unification of [Ti] and [U] produces map [rho], the
+   chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
+   [rho'] being [rho;mi:=d].
+
+   In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
+*)
+let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv =
+  (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
+  let clenv' =
+    { templval = clenv.templval;
+      templtyp = clenv.templtyp;
+      evd =
+        evar_merge (meta_merge clenv.evd nextclenv.evd) clenv.evd;
+      env = nextclenv.env } in
+  (* unify the type of the template of [nextclenv] with the type of [mv] *)
+  let clenv'' =
+    clenv_unify allow_K ~flags:flags CUMUL
+      (clenv_term clenv' nextclenv.templtyp)
+      (clenv_meta_type clenv' mv)
+      clenv' in
+  (* assign the metavar *)
+  let clenv''' =
+    clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv''
+  in
+  clenv'''
+
+(***************************************************************)
+(* Bindings *)
+
+type arg_bindings = constr explicit_bindings
+
+(* [clenv_independent clenv]
+ * returns a list of metavariables which appear in the term cval,
+ * and which are not dependent.  That is, they do not appear in
+ * the types of other metavars which are in cval, nor in the type
+ * of cval, ctyp. *)
+
+let clenv_independent clenv =
+  let mvs = collect_metas (clenv_value clenv) in
+  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
+
+let check_bindings bl =
+  match list_duplicates (List.map pi2 bl) with
+    | NamedHyp s :: _ ->
+	errorlabstrm ""
+	  (str "The variable " ++ pr_id s ++
+	   str " occurs more than once in binding list.");
+    | AnonHyp n :: _ ->
+	errorlabstrm ""
+	  (str "The position " ++ int n ++
+	   str " occurs more than once in binding list.")
+    | [] -> ()
+
+let meta_of_binder clause loc mvs = function
+  | NamedHyp s -> meta_with_name clause.evd s
+  | AnonHyp n ->
+      try List.nth mvs (n-1)
+      with (Failure _|Invalid_argument _) ->
+        errorlabstrm "" (str "No such binder.")
+
+let error_already_defined b =
+  match b with
+    | NamedHyp id ->
+        errorlabstrm ""
+          (str "Binder name \"" ++ pr_id id ++
+           str"\" already defined with incompatible value.")
+    | AnonHyp n ->
+        anomalylabstrm ""
+          (str "Position " ++ int n ++ str" already defined.")
+
+let clenv_unify_binding_type clenv c t u =
+  if isMeta (fst (whd_stack clenv.evd u)) then
+    (* Not enough information to know if some subtyping is needed *)
+    CoerceToType, clenv, c
+  else
+    (* Enough information so as to try a coercion now *)
+    try
+      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
+      TypeProcessed, { clenv with evd = evd }, c
+    with 
+      | PretypeError (_,NotClean _) as e -> raise e
+      | e when precatchable_exception e ->
+	  TypeNotProcessed, clenv, c
+
+let clenv_assign_binding clenv k c =
+  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+  let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+  let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
+  { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd }
+
+let clenv_match_args bl clenv =
+  if bl = [] then
+    clenv
+  else
+    let mvs = clenv_independent clenv in
+    check_bindings bl;
+    List.fold_left
+      (fun clenv (loc,b,c) ->
+	let k = meta_of_binder clenv loc mvs b in
+        if meta_defined clenv.evd k then
+          if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+          else error_already_defined b
+        else
+	  clenv_assign_binding clenv k c)
+      clenv bl
+
+let clenv_constrain_last_binding c clenv =
+  let all_mvs = collect_metas clenv.templval.rebus in
+  let k =
+    try list_last all_mvs
+    with Failure _ -> anomaly "clenv_constrain_with_bindings" in
+  clenv_assign_binding clenv k c
+
+let clenv_constrain_dep_args hyps_only bl clenv =
+  if bl = [] then
+    clenv
+  else
+    let occlist = clenv_dependent hyps_only clenv in
+    if List.length occlist = List.length bl then
+      List.fold_left2 clenv_assign_binding clenv occlist bl
+    else
+      errorlabstrm ""
+	(strbrk "Not the right number of missing arguments (expected " ++
+	 int (List.length occlist) ++ str ").")
+
+(****************************************************************)
+(* Clausal environment for an application *)
+
+let make_clenv_binding_gen hyps_only n gls (c,t) = function
+  | ImplicitBindings largs ->
+      let clause = mk_clenv_from_n gls n (c,t) in
+      clenv_constrain_dep_args hyps_only largs clause
+  | ExplicitBindings lbind ->
+      let clause = mk_clenv_rename_from_n gls n (c,t) in
+      clenv_match_args lbind clause
+  | NoBindings ->
+      mk_clenv_from_n gls n (c,t)
+
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
+let make_clenv_binding = make_clenv_binding_gen false None
+
+(****************************************************************)
+(* Pretty-print *)
+
+let pr_clenv clenv =
+  h 0
+    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
+     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+     pr_evar_map clenv.evd)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
new file mode 100644
index 000000000..2533fc537
--- /dev/null
+++ b/proofs/clenv.mli
@@ -0,0 +1,143 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Environ
+open Evd
+open Evarutil
+open Mod_subst
+open Rawterm
+open Unification
+(*i*)
+
+(***************************************************************)
+(* The Type of Constructions clausale environments. *)
+
+(* [env] is the typing context
+ * [evd] is the mapping from metavar and evar numbers to their types
+ *       and values.
+ * [templval] is the template which we are trying to fill out.
+ * [templtyp] is its type.
+ *)
+type clausenv = {
+  env      : env;
+  evd      : evar_map;
+  templval : constr freelisted;
+  templtyp : constr freelisted }
+
+(* Substitution is not applied on templenv (because [subst_clenv] is
+   applied only on hints which typing env is overwritten by the
+   goal env) *)
+val subst_clenv : substitution -> clausenv -> clausenv
+
+(* subject of clenv (instantiated) *)
+val clenv_value     : clausenv -> constr
+(* type of clenv (instantiated) *)
+val clenv_type      : clausenv -> types
+(* substitute resolved metas *)
+val clenv_nf_meta   : clausenv -> constr -> constr
+(* type of a meta in clenv context *)
+val clenv_meta_type : clausenv -> metavariable -> types
+
+val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
+val mk_clenv_from_n :
+  Goal.goal sigma -> int option -> constr * types -> clausenv
+val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+
+(***************************************************************)
+(* linking of clenvs *)
+
+val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
+val clenv_fchain :
+  ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
+
+(***************************************************************)
+(* Unification with clenvs *)
+
+(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
+val clenv_unify :
+  bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
+
+(* unifies the concl of the goal with the type of the clenv *)
+val clenv_unique_resolver :
+  bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+
+(* same as above ([allow_K=false]) but replaces remaining metas
+   with fresh evars if [evars_flag] is [true] *)
+val evar_clenv_unique_resolver :
+  bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+
+val clenv_dependent : bool -> clausenv -> metavariable list
+
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+
+(***************************************************************)
+(* Bindings *)
+
+type arg_bindings = constr explicit_bindings
+
+(* bindings where the key is the position in the template of the
+   clenv (dependent or not). Positions can be negative meaning to
+   start from the rightmost argument of the template. *)
+val clenv_independent : clausenv -> metavariable list
+val clenv_missing : clausenv -> metavariable list
+
+val clenv_constrain_last_binding : constr -> clausenv -> clausenv
+
+(* defines metas corresponding to the name of the bindings *)
+val clenv_match_args : arg_bindings -> clausenv -> clausenv
+
+val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
+
+(* start with a clenv to refine with a given term with bindings *)
+
+(* the arity of the lemma is fixed *)
+(* the optional int tells how many prods of the lemma have to be used *)
+(* use all of them if None *)
+val make_clenv_binding_apply :
+  Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
+   clausenv
+val make_clenv_binding :
+  Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
+
+(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+   [lmetas] is a list of metas to be applied to a proof of [t] so that
+   it produces the unification pattern [ccl]; [sigma'] is [sigma]
+   extended with [lmetas]; if [n] is defined, it limits the size of
+   the list even if [ccl] is still a product; otherwise, it stops when
+   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
+   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
+   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
+   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
+val clenv_environments :
+ evar_map -> int option -> types -> evar_map * constr list * types
+
+(* [clenv_environments_evars env sigma n t] does the same but returns
+   a list of Evar's defined in [env] and extends [sigma] accordingly *)
+val clenv_environments_evars :
+ env -> evar_map -> int option -> types -> evar_map * constr list * types
+
+(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
+val clenv_conv_leq :
+ env -> evar_map -> types -> constr -> int -> constr list
+
+(* if the clause is a product, add an extra meta for this product *)
+exception NotExtensibleClause
+val clenv_push_prod : clausenv -> clausenv
+
+(***************************************************************)
+(* Pretty-print *)
+val pr_clenv : clausenv -> Pp.std_ppcmds
+
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 9bc818e86..f977768bd 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -20,7 +20,6 @@ open Evd
 open Evarutil
 open Proof_type
 open Refiner
-open Proof_trees
 open Logic
 open Reduction
 open Reductionops
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
deleted file mode 100644
index 20a95dabf..000000000
--- a/proofs/decl_expr.mli
+++ /dev/null
@@ -1,105 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id:$ *)
-
-open Names
-open Util
-open Tacexpr
-
-type 'it statement =
-    {st_label:name;
-     st_it:'it}
-
-type thesis_kind =
-    Plain
-  | For of identifier
-
-type 'this or_thesis =
-    This of 'this
-  | Thesis of thesis_kind
-
-type side = Lhs | Rhs
-
-type elim_type =
-    ET_Case_analysis
-  | ET_Induction
-
-type block_type =
-    B_proof
-  | B_claim
-  | B_focus
-  | B_elim of elim_type
-
-type ('it,'constr,'tac) cut =
-    {cut_stat: 'it;
-     cut_by: 'constr list option;
-     cut_using: 'tac option}
-
-type ('var,'constr) hyp =
-    Hvar of 'var
-  | Hprop of 'constr statement
-
-type ('constr,'tac) casee =
-    Real of 'constr
-  | Virtual of ('constr statement,'constr,'tac) cut
-
-type ('hyp,'constr,'pat,'tac) bare_proof_instr =
-  | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Pcut of ('constr or_thesis statement,'constr,'tac) cut
-  | Prew of side * ('constr statement,'constr,'tac) cut
-  | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
-  | Passume of ('hyp,'constr) hyp list
-  | Plet of ('hyp,'constr) hyp list
-  | Pgiven of ('hyp,'constr) hyp list
-  | Pconsider of 'constr*('hyp,'constr) hyp list
-  | Pclaim of 'constr statement
-  | Pfocus of 'constr statement
-  | Pdefine of identifier * 'hyp list * 'constr
-  | Pcast of identifier or_thesis * 'constr
-  | Psuppose of ('hyp,'constr) hyp list
-  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
-  | Ptake of 'constr list
-  | Pper of elim_type * ('constr,'tac) casee
-  | Pend of block_type
-  | Pescape
-
-type emphasis = int
-
-type ('hyp,'constr,'pat,'tac) gen_proof_instr=
-    {emph: emphasis;
-     instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
-
-
-type raw_proof_instr =
-    ((identifier*(Topconstr.constr_expr option)) located,
-     Topconstr.constr_expr,
-     Topconstr.cases_pattern_expr,
-     raw_tactic_expr) gen_proof_instr
-
-type glob_proof_instr =
-    ((identifier*(Genarg.rawconstr_and_expr option)) located,
-     Genarg.rawconstr_and_expr,
-     Topconstr.cases_pattern_expr,
-     Tacexpr.glob_tactic_expr) gen_proof_instr
-
-type proof_pattern =
-    {pat_vars: Term.types statement list;
-     pat_aliases: (Term.constr*Term.types) statement list;
-     pat_constr: Term.constr;
-     pat_typ: Term.types;
-     pat_pat: Rawterm.cases_pattern;
-     pat_expr: Topconstr.cases_pattern_expr}
-
-type proof_instr =
-    (Term.constr statement,
-     Term.constr,
-     proof_pattern,
-     Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
deleted file mode 100644
index ba675327c..000000000
--- a/proofs/decl_mode.ml
+++ /dev/null
@@ -1,127 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id:$ i*)
-
-open Names
-open Term
-open Evd
-open Util
-
-let daimon_flag = ref false
-
-let set_daimon_flag () = daimon_flag:=true
-let clear_daimon_flag () = daimon_flag:=false
-let get_daimon_flag () = !daimon_flag
-
-type command_mode =
-    Mode_tactic
-  | Mode_proof
-  | Mode_none
-
-let mode_of_pftreestate pts =
-  let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
-    if goal.evar_extra = None then
-      Mode_tactic
-    else
-      Mode_proof
-
-let get_current_mode () =
-  try
-    mode_of_pftreestate (Pfedit.get_pftreestate ())
-  with _ -> Mode_none
-
-let check_not_proof_mode str =
- if get_current_mode () = Mode_proof then
-   error str
-
-type split_tree=
-    Skip_patt of Idset.t * split_tree
-  | Split_patt of Idset.t * inductive *
-		(bool array * (Idset.t * split_tree) option) array
-  | Close_patt of split_tree
-  | End_patt of (identifier * (int * int))
-
-type elim_kind =
-    EK_dep of split_tree
-  | EK_nodep
-  | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
-    {per_casee:constr;
-     per_ctype:types;
-     per_ind:inductive;
-     per_pred:constr;
-     per_args:constr list;
-     per_params:constr list;
-     per_nparams:int;
-     per_wf:recpath}
-
-type stack_info =
-    Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
-  | Suppose_case
-  | Claim
-  | Focus_claim
-
-type pm_info =
-    { pm_stack : stack_info list}
-
-let pm_in,pm_out = Dyn.create "pm_info"
-
-let get_info gl=
-  match gl.evar_extra with
-      None ->  invalid_arg "get_info"
-    | Some extra ->
-	try pm_out extra with _ -> invalid_arg "get_info"
-
-let get_stack pts =
-  let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
-    info.pm_stack
-
-let get_top_stack pts =
-  let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
-    info.pm_stack
-
-let get_end_command pts =
-  match mode_of_pftreestate pts with
-      Mode_proof ->
-	Some
-	  begin
-	    match get_top_stack pts with
-		[] -> "\"end proof\""
-	      | Claim::_ -> "\"end claim\""
-	      | Focus_claim::_-> "\"end focus\""
-	      | (Suppose_case :: Per (et,_,_,_) :: _
-		| Per (et,_,_,_) :: _ ) ->
-		  begin
-		    match et with
-			Decl_expr.ET_Case_analysis ->
-			  "\"end cases\" or start a new case"
-		      | Decl_expr.ET_Induction ->
-			  "\"end induction\" or start a new case"
-		  end
-	      | _ -> anomaly "lonely suppose"
-	  end
-    | Mode_tactic ->
-	begin
-	  try
-	    ignore
-	      (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
-	    Some "\"return\""
-	  with Not_found -> None
-	end
-    | Mode_none ->
-        error "no proof in progress"
-
-let get_last env =
-  try
-    let (id,_,_) =  List.hd (Environ.named_context env) in id
-  with Invalid_argument _ -> error "no previous statement to use"
-
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
deleted file mode 100644
index 734dc0442..000000000
--- a/proofs/decl_mode.mli
+++ /dev/null
@@ -1,74 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id:$ *)
-
-open Names
-open Term
-open Evd
-open Tacmach
-
-val set_daimon_flag : unit -> unit
-val clear_daimon_flag : unit -> unit
-val get_daimon_flag : unit -> bool
-
-type command_mode =
-    Mode_tactic
-  | Mode_proof
-  | Mode_none
-
-val mode_of_pftreestate : pftreestate -> command_mode
-
-val get_current_mode : unit -> command_mode
-
-val check_not_proof_mode : string -> unit
-
-type split_tree=
-    Skip_patt of Idset.t * split_tree
-  | Split_patt of Idset.t * inductive *
-		(bool array * (Idset.t * split_tree) option) array
-  | Close_patt of split_tree
-  | End_patt of (identifier * (int * int))
-
-type elim_kind =
-    EK_dep of split_tree
-  | EK_nodep
-  | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
-    {per_casee:constr;
-     per_ctype:types;
-     per_ind:inductive;
-     per_pred:constr;
-     per_args:constr list;
-     per_params:constr list;
-     per_nparams:int;
-     per_wf:recpath}
-
-type stack_info =
-    Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
-  | Suppose_case
-  | Claim
-  | Focus_claim
-
-type pm_info =
-    {pm_stack : stack_info list }
-
-val pm_in : pm_info -> Dyn.t
-
-val get_info : Proof_type.goal -> pm_info
-
-val get_end_command : pftreestate -> string option
-
-val get_stack : pftreestate -> stack_info list
-
-val get_top_stack : pftreestate -> stack_info list
-
-val get_last:  Environ.env -> identifier
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e4fab3f2f..6dfbbdc12 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -14,7 +14,6 @@ open Term
 open Evd
 open Evarutil
 open Sign
-open Proof_trees
 open Refiner
 
 (******************************************)
@@ -55,19 +54,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
 
 (* vernac command Existential *)
 
-let instantiate_pf_com n com pfts =
-  let gls = top_goal_of_pftreestate pfts in
-  let sigma = gls.sigma in
-  let (evk,evi) =
-    let evl = Evarutil.non_instantiated sigma in
-      if (n <= 0) then
-	error "incorrect existential variable index"
-      else if List.length evl < n then
-	  error "not so many uninstantiated existential variables"
-      else
-	List.nth evl (n-1)
-  in
+(* Main component of vernac command Existential *)
+let instantiate_pf_com evk com sigma =
+  let evi = Evd.find sigma evk in
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in
   let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
-  change_constraints_pftreestate sigma' pfts
+  sigma'
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 0bd616809..28c79d11e 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -24,6 +24,6 @@ val w_refine : evar * evar_info ->
   (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map
 
 val instantiate_pf_com :
-  int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+  Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map
 
 (* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
new file mode 100644
index 000000000..a9202318d
--- /dev/null
+++ b/proofs/goal.ml
@@ -0,0 +1,572 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesscer General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Term
+
+(* This module implements the abstract interface to goals *)
+(* A general invariant of the module, is that a goal whose associated 
+   evar is defined in the current evar_map, should not be accessed. *)
+
+(* type of the goals *)
+type goal = {
+  content : Evd.evar;      (* Corresponding evar. Allows to retrieve
+			      logical information once put together
+			      with an evar_map. *)
+  tags : string list       (* Heriditary? tags to be displayed *)
+}
+(* spiwack: I don't deal with the tags, yet. It is a worthy discussion
+   whether we do want some tags displayed besides the goal or not. *)
+
+(* access primitive *)
+(* invariant : [e] must exist in [em] *)
+let content evars { content = e } = Evd.find evars e
+
+
+(* Builds a new (empty) goal with evar [e] *)
+let build e =
+  { content = e ;
+    tags = []
+  }
+
+(* Builds a new goal with content evar [e] and 
+   inheriting from goal [gl]*)
+let descendent gl e =
+  { gl with content = e}
+
+(* [advance sigma g] returns [Some g'] if [g'] is undefined and 
+    is the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially) solved. *)
+open Store.Field
+let rec advance sigma g =
+  let evi = Evd.find sigma g.content in
+  if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then
+    let v = 
+      match evi.Evd.evar_body with 
+      | Evd.Evar_defined c -> c
+      | _ -> Util.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
+    in
+    let (e,_) = Term.destEvar v in
+    let g' = { g with content = e } in
+    advance sigma g'
+  else
+    match evi.Evd.evar_body with
+    | Evd.Evar_defined _ -> None
+    | _ -> Some g
+
+(*** Goal tactics ***)
+
+
+(* Goal tactics are [subgoal sensitive]-s *)
+type subgoals = { subgoals: goal list }
+
+(* type of the base elements of the goal API.*)
+(* it has an extra evar_info with respect to what would be expected,
+   it is supposed to be the evar_info of the goal in the evar_map.
+   The idea is that it is computed by the [run] function as an 
+   optimisation, since it will generaly not change during the 
+   evaluation. *)
+type 'a sensitive = 
+    Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
+
+(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
+(* the evar_info corresponding to the goal is computed at once
+   as an optimisation (it shouldn't change during the evaluation). *)
+let eval t env defs gl =
+  let info = content defs gl in
+  let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
+  let rdefs = ref defs in
+  let r = t env rdefs gl info in
+  ( r , !rdefs )
+
+(* monadic bind on sensitive expressions *)
+let bind e f env rdefs goal info =
+  f (e env rdefs goal info) env rdefs goal info
+
+(* monadic return on sensitive expressions *)
+let return v _ _ _ _ = v
+
+(* interpretation of "open" constr *)
+(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. 
+    In an ideal world, this could/should be the other way round.
+    As of now, though, it seems at least quite useful to build tactics. *)
+let interp_constr cexpr env rdefs _ _ =
+  let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in
+  rdefs := defs ;
+  c
+
+(* Type of constr with holes used by refine. *)
+(* The list of evars doesn't necessarily contain all the evars in the constr, 
+    only those the constr has introduced. *)
+(* The variables in [myevars] are supposed to be stored
+   in decreasing order. Breaking this invariant might cause
+   many things to go wrong. *)
+type refinable = {
+  me: constr;
+  my_evars: Evd.evar list
+}
+
+module Refinable = struct
+  type t = refinable
+
+  type handle = Evd.evar list ref
+
+  let make t env rdefs gl info = 
+    let r = ref [] in
+    let me = t r env rdefs gl info in
+    { me = me;
+       my_evars = !r }
+  let make_with t env rdefs gl info =
+    let r = ref [] in
+    let (me,side) = t r env rdefs gl info in
+    { me = me ; my_evars = !r } , side
+
+  let mkEvar handle env typ _ rdefs _ _ =
+    let ev = Evarutil.e_new_evar rdefs env typ in
+    let (e,_) = Term.destEvar ev in
+    handle := e::!handle;
+    ev
+
+  (* [with_type c typ] constrains term [c] to have type [typ].  *)
+  let with_type t typ env rdefs _ _ = 
+    (* spiwack: this function assumes that no evars can be created during
+        this sort of coercion.
+        If it is not the case it could produce bugs. We would need to add a handle
+        and add the new evars to it. *)
+    let my_type = Retyping.get_type_of env !rdefs t in
+    let j = Environ.make_judge t my_type in
+    let tycon = Evarutil.mk_tycon_type typ in
+    let (new_defs,j') = 
+      Coercion.Default.inh_conv_coerce_to (Util.dummy_loc) env !rdefs j tycon 
+    in
+    rdefs := new_defs;
+    j'.Environ.uj_val 
+
+  (* spiwack: it is not very fine grain since it solves all typeclasses holes, 
+      not only those containing the current goal, or a given term. But it
+      seems to fit our needs so far. *)
+  let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
+    rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?split ~fail env !rdefs;
+    ()
+
+
+
+  (* a pessimistic (i.e : there won't be many positive answers) filter
+     over evar_maps *)
+  let evar_map_filter f evm =
+    Evd.fold (fun ev evi r -> 
+		if f ev evi then 
+		  Evd.add r ev evi 
+		else 
+		  r
+	     ) 
+      evm 
+      Evd.empty
+
+  (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
+  let rec fusion l1 l2 = match l1 , l2 with
+    | [] , _ -> l2
+    | _ , [] -> l1
+    | a::l1 , b::_ when a>b -> a::(fusion l1 l2)
+    | a::l1 , b::l2 when a=b -> a::(fusion l1 l2)
+    | _ , b::l2 -> b::(fusion l1 l2)
+
+  (* [constr_of_raw] is a pretyping function. The [check_type] argument
+      asks whether the term should have the same type as the conclusion.
+      [resolve_classes] is a flag on pretyping functions which, if set to true,
+      calls the typeclass resolver.
+      The principal argument is a [rawconstr] which is then pretyped in the
+      context of a term, the remaining evars are registered to the handle.
+      It is the main component of the toplevel refine tactic.*)
+  (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
+      a bit hackish. However it does not seem possible to move it out until
+      pretyping is defined as some proof procedure. *)
+  let constr_of_raw handle check_type resolve_classes rawc env rdefs gl info =
+    (* We need to keep trace of what [rdefs] was originally*)
+    let init_defs = !rdefs in
+    (* if [check_type] is true, then creates a type constraint for the 
+       proof-to-be *)
+    let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in
+    (* call to [understand_tcc_evars] returns a constr with undefined evars
+       these evars will be our new goals *)
+    let open_constr = 
+      Pretyping.Default.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
+    in
+    (* [!rdefs] contains the evar_map outputed by  [understand_...] *)
+    let post_defs = !rdefs in
+    (* [delta_evars] holds the evars that have been introduced by this
+       refinement (but not immediatly solved) *)
+    (* spiwack: this is the hackish part, don't know how to do any better though. *)
+    let delta_evars = evar_map_filter (fun ev evi ->
+					 evi.Evd.evar_body = Evd.Evar_empty &&
+                                         not (Evd.mem init_defs ev)
+				      )
+                                     post_defs
+    in
+    (* [delta_evars] in the shape of a list of [evar]-s*)
+    let delta_list = List.map fst (Evd.to_list delta_evars) in
+    (* The variables in [myevars] are supposed to be stored
+       in decreasing order. Breaking this invariant might cause
+       many things to go wrong. *)
+    handle := fusion delta_list !handle ; 
+    open_constr 
+
+end
+
+(* [refine t] takes a refinable term and use it as a partial proof for current
+    goal. *)
+let refine step env rdefs gl info =
+  (* subgoals to return *)
+  (* The evars in [my_evars] are stored in reverse order.
+     It is expectingly better however to display the goal
+     in increasing order. *)
+  rdefs := Evarconv.consider_remaining_unif_problems env !rdefs ;
+  let subgoals = List.map (descendent gl) (List.rev step.my_evars) in
+  (* creates the new [evar_map] by defining the evar of the current goal
+     as being [refine_step]. *)
+  let new_defs = Evd.define gl.content (step.me) !rdefs in
+  rdefs := new_defs;   
+  (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *)
+  let subgoals = 
+    Option.List.flatten (List.map (advance !rdefs) subgoals) 
+  in
+  { subgoals = subgoals }
+
+
+(*** Cleaning  goals ***)
+
+let clear ids env rdefs gl info =
+  let hyps = Evd.evar_hyps info in
+  let concl = Evd.evar_concl info in
+  let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in
+  let cleared_env = Environ.reset_with_named_context hyps env in
+  let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in
+  let (cleared_evar,_) = Term.destEvar cleared_concl in
+  let cleared_goal = descendent gl cleared_evar in
+  rdefs := Evd.define gl.content cleared_concl !rdefs;
+  { subgoals = [cleared_goal] }
+
+let wrap_apply_to_hyp_and_dependent_on sign id f g =
+  try Environ.apply_to_hyp_and_dependent_on sign id f g 
+  with Environ.Hyp_not_found -> 
+    Util.error "No such assumption" 
+
+let check_typability env sigma c =
+  let _ = Typing.type_of env sigma c in () 
+
+let recheck_typability (what,id) env sigma t =
+  try check_typability env sigma t
+  with _ ->
+    let s = match what with
+      | None -> "the conclusion"
+      | Some id -> "hypothesis "^(Names.string_of_id id) in
+    Util.error
+      ("The correctness of "^s^" relies on the body of "^(Names.string_of_id id))
+
+let remove_hyp_body env sigma id =
+  let sign =
+    wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id
+      (fun (_,c,t) _ ->
+	match c with
+	| None -> Util.error ((Names.string_of_id id)^" is not a local definition")
+	| Some c ->(id,None,t))
+      (fun (id',c,t as d) sign ->
+	(
+	  begin 
+	    let env = Environ.reset_with_named_context sign env in
+	    match c with
+	    | None ->  recheck_typability (Some id',id) env sigma t
+	    | Some b ->
+		let b' = mkCast (b,DEFAULTcast, t) in
+		recheck_typability (Some id',id) env sigma b'
+	  end;d))
+  in
+  Environ.reset_with_named_context sign env 
+
+
+let clear_body idents env rdefs gl info =
+  let info = content !rdefs gl in
+  let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
+  let aux env id = 
+     let env' = remove_hyp_body env !rdefs id in
+       recheck_typability (None,id) env' !rdefs (Evd.evar_concl info);
+       env'
+  in
+  let new_env = 
+    List.fold_left aux full_env idents
+  in
+  let concl = Evd.evar_concl info in
+  let (defs',new_constr) = Evarutil.new_evar !rdefs new_env concl in
+  let (new_evar,_) = destEvar new_constr in
+  let new_goal = descendent gl new_evar in
+  rdefs := Evd.define gl.content new_constr defs';
+  { subgoals = [new_goal] }
+
+
+(*** Sensitive primitives ***)
+
+(* [concl] is the conclusion of the current goal *)
+let concl _ _ _ info =
+  Evd.evar_concl info
+
+(* [hyps] is the [named_context_val] representing the hypotheses
+   of the current goal *)
+let hyps _ _ _ info =
+  Evd.evar_hyps info
+
+(* [env] is the current [Environ.env] containing both the 
+   environment in which the proof is ran, and the goal hypotheses *)
+let env env _ _ _ = env
+
+(* [defs] is the [Evd.evar_map] at the current evaluation point *)
+let defs _ rdefs _ _ =
+  !rdefs
+
+(* Cf mli for more detailed comment.
+    [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
+    to communicate whether or not the value is defined in the particular context. *)
+exception UndefinedHere
+let null _ _ _ _ = raise UndefinedHere
+
+let plus s1 s2 env rdefs goal info =
+  try s1 env rdefs goal info
+  with UndefinedHere -> s2 env rdefs goal info
+
+(* Equality of two goals *)
+let equal { content = e1 } { content = e2 } = e1 = e2
+
+let here goal value _ _ goal' _ =
+  if equal goal goal' then
+    value
+  else 
+    raise UndefinedHere
+
+(* arnaud: voir à la passer dans Util ? *)
+let rec list_mem_with eq x = function
+  | y::_ when eq x y -> true
+  | _::l -> list_mem_with eq x l
+  | [] -> false
+
+let here_list goals value _ _ goal' _ =
+  if list_mem_with equal goal' goals then
+    value
+  else
+    raise UndefinedHere
+
+
+(*** Conversion in goals ***)
+
+let convert_hyp check (id,b,bt as d) env rdefs gl info =
+  let sigma = !rdefs in
+  (* This function substitutes the new type and body definitions
+     in the appropriate variable when used with {!Environ.apply_hyps}. *)
+  let replace_function =
+    (fun _ (_,c,ct) _ ->
+       if check && not (Reductionops.is_conv env sigma bt ct) then
+	 Util.error ("Incorrect change of the type of "^(Names.string_of_id id));
+       if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then
+	 Util.error ("Incorrect change of the body of "^(Names.string_of_id id));
+       d)
+  in
+  (* Modified named context. *)
+  let new_hyps = 
+    Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function
+  in  
+  let new_env = Environ.reset_with_named_context new_hyps env in
+  let new_constr = 
+    Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
+  in
+  let (new_evar,_) = Term.destEvar new_constr in
+  let new_goal = descendent gl new_evar in
+  rdefs := Evd.define gl.content new_constr !rdefs;
+  { subgoals = [new_goal] }
+  
+let convert_concl check cl' env rdefs gl info =
+  let sigma = !rdefs in
+  let cl = concl env rdefs gl info in
+  check_typability env sigma cl';
+  if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
+    let new_constr = 
+      Evarutil.e_new_evar rdefs env cl' 
+    in
+    let (new_evar,_) = Term.destEvar new_constr in
+    let new_goal = descendent gl new_evar in
+    rdefs := Evd.define gl.content new_constr !rdefs;
+    { subgoals = [new_goal] }
+  else
+    Util.error "convert-concl rule passed non-converting term"
+
+
+(*** Bureaucracy in hypotheses ***)  
+
+(* Renames a hypothesis. *)
+let rename_hyp_sign id1 id2 sign =
+  Environ.apply_to_hyp_and_dependent_on sign id1
+    (fun (_,b,t) _ -> (id2,b,t))
+    (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
+let rename_hyp id1 id2 env rdefs gl info = 
+  let hyps = hyps env rdefs gl info in
+  if id1 <> id2 &&
+    List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
+       Util.error ((Names.string_of_id id2)^" is already used.");
+  let new_hyps = rename_hyp_sign id1 id2 hyps in
+  let new_env = Environ.reset_with_named_context new_hyps env in
+  let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
+  let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
+  let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in
+  let (new_evar,_) = Term.destEvar new_subproof in
+  let new_goal = descendent gl new_evar in
+  rdefs := Evd.define gl.content new_subproof !rdefs;
+  { subgoals = [new_goal] }
+
+(*** Additional functions ***)
+
+(* emulates List.map for functions of type 
+   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
+   new evar_map to next definition. *)
+(*This sort of construction actually works with any monad (here the State monade
+   in Haskell). There is a generic construction in Haskell called mapM.
+*)
+let rec list_map f l s = 
+  match l with
+  | [] -> ([],s)
+  | a::l -> let (a,s) = f s a in
+               let (l,s) = list_map f l s in
+	       (a::l,s)
+
+
+(* Layer to implement v8.2 tactic engine ontop of the new architecture. 
+   Types are different from what they used to be due to a change of the
+   internal types. *)
+module V82 = struct
+
+  (* Old style env primitive *)
+  let env evars gl = 
+    let evi = content evars gl in
+    Evd.evar_env evi
+
+  (* For printing *)
+  let unfiltered_env evars gl = 
+    let evi = content evars gl in
+    Evd.evar_unfiltered_env evi
+
+  (* Old style hyps primitive *)
+  let hyps evars gl =
+    let evi = content evars gl in
+    evi.Evd.evar_hyps
+
+  (* Access to ".evar_concl" *)
+  let concl evars gl =
+    let evi = content evars gl in
+    evi.Evd.evar_concl
+
+  (* Access to ".evar_extra" *)
+  let extra evars gl =
+    let evi = content evars gl in
+    evi.Evd.evar_extra
+
+  (* Old style filtered_context primitive *)
+  let filtered_context evars gl =
+    let evi = content evars gl in
+    Evd.evar_filtered_context evi
+
+  (* Old style mk_goal primitive *)
+  let mk_goal evars hyps concl extra =
+    let evk = Evarutil.new_untyped_evar () in
+    let evi = { Evd.evar_hyps = hyps; 
+		     Evd.evar_concl = concl; 
+		     Evd.evar_filter = List.map (fun _ -> true) 
+	                                                        (Environ.named_context_of_val hyps);
+		     Evd.evar_body = Evd.Evar_empty; 
+		     Evd.evar_source = (Util.dummy_loc,Evd.GoalEvar);
+		     Evd.evar_extra = extra }
+    in
+    let evi = Typeclasses.mark_unresolvable evi in
+    let evars = Evd.add evars evk evi in
+    let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in
+    let inst = Array.of_list (List.map mkVar ids) in
+    let ev = Term.mkEvar (evk,inst) in
+    (build evk, ev, evars)
+
+  (* Equality function on goals *)
+  let equal evars gl1 gl2 =
+    let evi1 = content evars gl1 in
+    let evi2 = content evars gl2 in
+    Evd.eq_evar_info evi1 evi2
+
+  (* Creates a dummy [goal sigma] for use in auto *)
+  let dummy_goal =
+    (* This goal seems to be marshalled somewhere. Therefore it cannot be 
+       marked unresolvable for typeclasses, as non-empty Store.t-s happen
+       to have functional content. *)
+    let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
+    let evk = Evarutil.new_untyped_evar () in
+    let sigma = Evd.add Evd.empty evk evi in
+    { Evd.it = build evk ; Evd.sigma = sigma }
+
+  (* Makes a goal out of an evar *)
+  let build = build
+
+  (* Instantiates a goal with an open term *)
+  let partial_solution sigma { content=evk } c =
+    Evd.define evk c sigma
+   
+  (* Parts of the progress tactical *)
+  let same_goal evars1 gl1 evars2 gl2 =
+    let evi1 = content evars1 gl1 in
+    let evi2 = content evars2 gl2 in
+    Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+    Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
+      
+  let weak_progress glss gls =
+    match glss.Evd.it with
+    | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
+    | _ -> true
+
+  let progress glss gls =
+    weak_progress glss gls
+    (* spiwack: progress normally goes like this:
+    (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls) 
+       This is immensly slow in the current implementation. Maybe we could
+       reimplement progress_evar_map with restricted folds like "fold_undefined",
+       with a good implementation of them.
+    *)
+      
+  (* Used for congruence closure *)
+  let new_goal_with sigma gl new_hyps =
+    let evi = content sigma gl in
+    let new_evi = { evi with Evd.evar_hyps = new_hyps } in
+    let new_evi = Typeclasses.mark_unresolvable new_evi in
+    let evk = Evarutil.new_untyped_evar () in
+    let new_sigma = Evd.add Evd.empty evk new_evi in
+    { Evd.it = build evk ; sigma = new_sigma }
+
+  (* Used by the typeclasses *)
+  let nf_evar sigma gl =
+    let evi = content sigma gl in
+    let evi = Evarutil.nf_evar_info sigma evi in
+    let sigma = Evd.add sigma gl.content evi in
+    (gl,sigma)
+
+  (* Goal represented as a type, doesn't take into account section variables *)
+  let abstract_type sigma gl = 
+    let (gl,sigma) = nf_evar sigma gl in
+    let env = env sigma gl in
+    let genv = Global.env () in
+    let is_proof_var decl = 
+      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false 
+      with Not_found -> true in
+    Environ.fold_named_context_reverse (fun t decl ->
+					  if is_proof_var decl then
+					    mkNamedProd_or_LetIn decl t
+					  else
+					    t
+				       ) ~init:(concl sigma gl) env
+
+end
diff --git a/proofs/goal.mli b/proofs/goal.mli
new file mode 100644
index 000000000..49e3c9b1a
--- /dev/null
+++ b/proofs/goal.mli
@@ -0,0 +1,228 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: goal.mli aspiwack $ *)
+
+(* This module implements the abstract interface to goals *)
+
+type goal
+
+(* spiwack: this primitive is not extremely brilliant. It may be a good
+    idea to define goals and proof views in the same file to avoid this
+    sort of communication pipes. But I find it heavy. *)
+val build : Evd.evar -> goal 
+
+(* [advance sigma g] returns [Some g'] if [g'] is undefined and 
+    is the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially) solved. *)
+open Store.Field
+val advance : Evd.evar_map -> goal -> goal option
+
+
+(*** Goal tactics ***)
+
+
+(* Goal tactics are [subgoal sensitive]-s *)
+type subgoals = private { subgoals: goal list }
+
+(* Goal sensitive values *)
+type +'a sensitive
+
+(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
+val eval : 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> 'a * Evd.evar_map
+
+(* monadic bind on sensitive expressions *)
+val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive
+
+(* monadic return on sensitive expressions *)
+val return : 'a -> 'a sensitive
+
+
+(* interpretation of "open" constr *)
+(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. 
+    In an ideal world, this could/should be the other way round.
+    As of now, though, it seems at least quite useful to build tactics. *)
+val interp_constr : Topconstr.constr_expr -> Term.constr sensitive
+
+(* Type of constr with holes used by refine. *)
+type refinable
+
+module Refinable : sig
+  type t = refinable 
+  type handle
+
+  val make : (handle -> Term.constr sensitive) -> refinable sensitive
+  val make_with : (handle -> (Term.constr*'a) sensitive) -> (refinable*'a) sensitive
+
+  val mkEvar : handle -> Environ.env -> Term.types -> Term.constr sensitive
+
+  (* [with_type c typ] constrains term [c] to have type [typ].  *)
+  val with_type : Term.constr -> Term.types -> Term.constr sensitive
+
+  val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
+
+
+  (* [constr_of_raw h check_type resolve_classes] is a pretyping function.
+      The [check_type] argument asks whether the term should have the same
+      type as the conclusion. [resolve_classes] is a flag on pretyping functions
+      which, if set to true, calls the typeclass resolver.
+      The principal argument is a [rawconstr] which is then pretyped in the
+      context of a term, the remaining evars are registered to the handle.
+      It is the main component of the toplevel refine tactic.*)
+  val constr_of_raw : 
+    handle -> bool -> bool -> Rawterm.rawconstr -> Term.constr sensitive
+
+end
+
+(* [refine t] takes a refinable term and use it as a partial proof for current
+    goal. *)
+val refine : refinable -> subgoals sensitive
+
+
+(*** Cleaning  goals ***)
+
+(* Implements the [clear] tactic *)
+val clear : Names.identifier list -> subgoals sensitive
+
+(* Implements the [clearbody] tactic *)
+val clear_body : Names.identifier list -> subgoals sensitive
+
+
+(*** Conversion in goals ***)
+
+(* Changes an hypothesis of the goal with a convertible type and body.
+   Checks convertibility if the boolean argument is true. *)
+val convert_hyp : bool -> Term.named_declaration -> subgoals sensitive
+
+(* Changes the conclusion of the goal with a convertible type and body.
+   Checks convertibility if the boolean argument is true. *)
+val convert_concl : bool -> Term.constr -> subgoals sensitive
+
+(*** Bureaucracy in hypotheses ***)
+
+(* Renames a hypothesis. *)
+val rename_hyp : Names.identifier -> Names.identifier -> subgoals sensitive
+
+(*** Sensitive primitives ***)
+
+(* [concl] is the conclusion of the current goal *)
+val concl : Term.constr sensitive
+
+(* [hyps] is the [named_context_val] representing the hypotheses
+   of the current goal *)
+val hyps : Environ.named_context_val sensitive
+
+(* [env] is the current [Environ.env] containing both the 
+   environment in which the proof is ran, and the goal hypotheses *)
+val env : Environ.env sensitive
+
+(* [defs] is the [Evd.evar_map] at the current evaluation point *)
+val defs : Evd.evar_map sensitive
+
+(* These four functions serve as foundation for the goal sensitive part
+    of the tactic monad (see Proofview).
+    [here] is a special sort of [return]: [here g a] is the value [a], but
+    does not have any value (it raises an exception) if evaluated in
+    any other goal than [g].
+    [here_list] is the same, except with a list of goals rather than a single one.
+    [plus a b] is the same as [a] if [a] is defined in the current goal, otherwise
+    it is [b]. Effectively it's defined in the goals where [a] and [b] are defined.
+    [null] is defined in no goal. (it is a neutral element for [plus]). *)
+(* spiwack: these primitives are a bit hackish, but I couldn't find another way
+    to pass information between goals, like for an intro tactic which gives to
+    each goal the name of the variable it introduce.
+    In pratice, in my experience, the primitives given in Proofview (in terms of
+    [here] and [plus]) are sufficient to define any tactics, hence these might
+    be another example of communication primitives between Goal and Proofview.
+    Still, I can't see a way to prevent using the Proofview primitive to read
+    a goal sensitive value out of its valid context. *)
+val null : 'a sensitive
+
+val plus : 'a sensitive -> 'a sensitive -> 'a sensitive 
+
+val here : goal -> 'a -> 'a sensitive 
+
+val here_list : goal list -> 'a -> 'a sensitive 
+
+(*** Additional functions ***)
+
+(* emulates List.map for functions of type 
+   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
+   new evar_map to next definition *)
+val list_map : (Evd.evar_map -> 'a -> 'b * Evd.evar_map) -> 
+                        'a list -> 
+                        Evd.evar_map -> 
+                        'b list *Evd.evar_map
+
+(* Layer to implement v8.2 tactic engine ontop of the new architecture. 
+   Types are different from what they used to be due to a change of the
+   internal types. *)
+module V82 : sig
+
+  (* Old style env primitive *)
+  val env : Evd.evar_map -> goal -> Environ.env
+
+  (* For printing *)
+  val unfiltered_env : Evd.evar_map -> goal -> Environ.env
+
+  (* Old style hyps primitive *)
+  val hyps : Evd.evar_map -> goal -> Environ.named_context_val
+
+  (* Access to ".evar_concl" *)
+  val concl : Evd.evar_map -> goal -> Term.constr
+
+  (* Access to ".evar_extra" *)
+  val extra : Evd.evar_map -> goal -> Store.t
+
+  (* Old style filtered_context primitive *)
+  val filtered_context : Evd.evar_map -> goal -> Sign.named_context
+
+  (* Old style mk_goal primitive, returns a new goal with corresponding 
+       hypotheses and conclusion, together with a term which is precisely
+       the evar corresponding to the goal, and an updated evar_map. *)
+  val mk_goal : Evd.evar_map -> 
+                         Environ.named_context_val ->
+                         Term.constr ->
+                         Store.t ->
+                         goal * Term.constr * Evd.evar_map
+
+  (* Equality function on goals *)
+  val equal : Evd.evar_map -> goal -> goal -> bool
+
+  (* Creates a dummy [goal sigma] for use in auto *)
+  val dummy_goal : goal Evd.sigma
+
+  (* Makes a goal out of an evar *)
+  (* spiwack: used by [Proofview.init], not entirely clean probably, but it is
+      the only way I could think of to preserve compatibility with previous Coq
+      stuff. *)
+  val build : Evd.evar -> goal 
+
+
+  (* Instantiates a goal with an open term *)
+  val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+   
+  (* Principal part of the weak-progress tactical *)
+  val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
+   
+  (* Principal part of the progress tactical *)
+  val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
+    
+ (* Principal part of tclNOTSAMEGOAL *)
+  val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
+
+ (* Used for congruence closure *)
+  val new_goal_with : Evd.evar_map -> goal ->  Environ.named_context_val -> goal Evd.sigma 
+
+  (* Used by the typeclasses *)
+  val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
+
+  (* Goal represented as a type, doesn't take into account section variables *)
+  val abstract_type : Evd.evar_map -> goal -> Term.types 
+
+end
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 11155d369..7c092bb66 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -21,7 +21,6 @@ open Reductionops
 open Inductive
 open Inductiveops
 open Typing
-open Proof_trees
 open Proof_type
 open Typeops
 open Type_errors
@@ -326,22 +325,18 @@ let goal_type_of env sigma c =
   (if !check then type_of else Retyping.get_type_of ~refresh:true) env sigma c
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
-  let env = evar_env goal in
-  let hyps = goal.evar_hyps in
-  let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
-(*
-   if  not (occur_meta trm) then
-    let t'ty = (unsafe_machine env sigma trm).uj_type in
-    let _ = conv_leq_goal env sigma trm t'ty conclty in
-      (goalacc,t'ty)
-  else
-*)
+  let env = Goal.V82.env sigma goal in
+  let hyps = Goal.V82.hyps sigma goal in
+  let mk_goal hyps concl =
+    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
+  in
   match kind_of_term trm with
     | Meta _ ->
 	let conclty = nf_betaiota sigma conclty in
 	  if !check && occur_meta conclty then
 	    raise (RefinerError (MetaInType conclty));
-	  (mk_goal hyps conclty)::goalacc, conclty
+	  let (gl,ev,sigma) = mk_goal hyps conclty in
+	  gl::goalacc, conclty, sigma, ev
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
@@ -349,30 +344,32 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-	let (acc',hdty) =
+	let (acc',hdty,sigma,applicand) =
 	  match kind_of_term f with
 	    | Ind _ | Const _
 		when (isInd f or has_polymorphic_type (destConst f)) ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc,
-                type_of_global_reference_knowing_conclusion env sigma f conclty
+                type_of_global_reference_knowing_conclusion env sigma f conclty,
+		sigma, f
 	    | _ ->
 		mk_hdgoals sigma goal goalacc f
 	in
-	let (acc'',conclty') =
+	let (acc'',conclty',sigma, args) =
 	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
 	check_conv_leq_goal env sigma trm conclty' conclty;
-        (acc'',conclty')
+        (acc'',conclty',sigma, Term.mkApp (applicand, Array.of_list args))
 
-    | Case (_,p,c,lf) ->
-	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
+    | Case (ci,p,c,lf) ->
+	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
 	check_conv_leq_goal env sigma trm conclty' conclty;
-	let acc'' =
+	let (acc'',sigma, rbranches) =
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
-            acc' lbrty lf
+            (fun (lacc,sigma,bacc) ty fi ->
+	       let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
+            (acc',sigma,[]) lbrty lf
 	in
-	(acc'',conclty')
+	(acc'',conclty',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches)))
 
     | _ ->
 	if occur_meta trm then
@@ -380,70 +377,77 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
-        (goalacc,t'ty)
+        (goalacc,t'ty,sigma, trm)
 
-(* Same as mkREFGOALS but without knowing te type of the term. Therefore,
+(* Same as mkREFGOALS but without knowing the type of the term. Therefore,
  * Metas should be casted. *)
 
 and mk_hdgoals sigma goal goalacc trm =
-  let env = evar_env goal in
-  let hyps = goal.evar_hyps in
-  let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
+  let env = Goal.V82.env sigma goal in
+  let hyps = Goal.V82.hyps sigma goal in
+  let mk_goal hyps concl = 
+    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	(mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
+	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in
+	gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
 	mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-	let (acc',hdty) =
+	let (acc',hdty,sigma,applicand) =
 	  if isInd f or isConst f
 	     & not (array_exists occur_meta l) (* we could be finer *)
 	  then
-	    (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
+	   (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f)
 	  else mk_hdgoals sigma goal goalacc f
 	in
-	mk_arggoals sigma goal acc' hdty (Array.to_list l)
+	let (acc'',conclty',sigma, args) =
+	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
+	(acc'',conclty',sigma, Term.mkApp (applicand, Array.of_list args))
 
-    | Case (_,p,c,lf) ->
-	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
-	let acc'' =
+    | Case (ci,p,c,lf) ->
+	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
+	let (acc'',sigma,rbranches) =
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
-            acc' lbrty lf
+            (fun (lacc,sigma,bacc) ty fi ->
+	       let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
+            (acc',sigma,[]) lbrty lf
 	in
-	(acc'',conclty')
+	(acc'',conclty',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches)))
 
     | _ ->
 	if !check && occur_meta trm then
 	  anomaly "refine called with a dependent meta";
-	goalacc, goal_type_of env sigma trm
+	goalacc, goal_type_of env sigma trm, sigma, trm
 
 and mk_arggoals sigma goal goalacc funty = function
-  | [] -> goalacc,funty
+  | [] -> goalacc,funty,sigma, []
   | harg::tlargs as allargs ->
-      let t = whd_betadeltaiota (evar_env goal) sigma funty in
+      let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
       match kind_of_term t with
 	| Prod (_,c1,b) ->
-	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
-	    mk_arggoals sigma goal acc' (subst1 harg b) tlargs
+	    let (acc',hargty,sigma,arg') = mk_refgoals sigma goal goalacc c1 harg in
+	    let (acc'',fty, sigma', args) =
+	      mk_arggoals sigma goal acc' (subst1 harg b) tlargs in
+	    (acc'',fty,sigma',arg'::args)
 	| LetIn (_,c1,_,b) ->
 	    mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
 	| _ -> raise (RefinerError (CannotApply (t,harg)))
 
 and mk_casegoals sigma goal goalacc p c =
-  let env = evar_env goal in
-  let (acc',ct) = mk_hdgoals sigma goal goalacc c in
-  let (acc'',pt) = mk_hdgoals sigma goal acc' p in
+  let env = Goal.V82.env sigma goal in
+  let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+  let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
   let indspec =
     try find_mrectype env sigma ct
     with Not_found -> anomaly "mk_casegoals" in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec p c in
-  (acc'',lbrty,conclty)
+  (acc'',lbrty,conclty,sigma,p',c')
 
 
 let convert_hyp sign sigma (id,b,bt as d) =
@@ -461,18 +465,6 @@ let convert_hyp sign sigma (id,b,bt as d) =
        d) in
   reorder_val_context env sign' !reorder
 
-(* Normalizing evars in a goal. Called by tactic Local_constraints
-   (i.e. when the sigma of the proof tree changes). Detect if the
-   goal is unchanged *)
-let norm_goal sigma gl =
-  let red_fun = Evarutil.nf_evar sigma in
-  let ncl = red_fun gl.evar_concl in
-  let ngl =
-    { gl with
-	evar_concl = ncl;
-	evar_hyps = map_named_val red_fun gl.evar_hyps } in
-    if Evd.eq_evar_info ngl gl then None else Some ngl
-
 
 
 (************************************************************************)
@@ -480,10 +472,12 @@ let norm_goal sigma gl =
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
-  let env = evar_env goal in
-  let sign = goal.evar_hyps in
-  let cl = goal.evar_concl in
-  let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
+  let env = Goal.V82.env sigma goal in
+  let sign = Goal.V82.hyps sigma goal in
+  let cl = Goal.V82.concl sigma goal in
+  let mk_goal hyps concl = 
+    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) 
+  in
   match r with
     (* Logical rules *)
     | Intro id ->
@@ -491,19 +485,23 @@ let prim_refiner r sigma goal =
 	  error "New variable is already declared";
         (match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,c1,b) ->
-	       let sg = mk_goal (push_named_context_val (id,None,c1) sign)
+	       let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
+               let sigma = 
+		 Goal.V82.partial_solution sigma goal (mkNamedLambda id c1 ev) in
 	       ([sg], sigma)
 	   | LetIn (_,c1,t1,b) ->
-	       let sg =
+	       let (sg,ev,sigma) =
 		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
+	       let sigma = 
+		 Goal.V82.partial_solution sigma goal (mkNamedLetIn id c1 t1 ev) in
 	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
 
     | Cut (b,replace,id,t) ->
-        let sg1 = mk_goal sign (nf_betaiota sigma t) in
+        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
 	let sign,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
@@ -515,7 +513,10 @@ let prim_refiner r sigma goal =
             (if !check && mem_named_context id (named_context_of_val sign) then
                 error "New variable is already declared";
 	     push_named_context_val (id,None,t) sign,cl,sigma) in
-        let sg2 = mk_goal sign cl in
+        let (sg2,ev2,sigma) = 
+	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
+	let oterm = Term.mkApp (Term.mkNamedLambda id t ev2 , [| ev1 |]) in
+	let sigma = Goal.V82.partial_solution sigma goal oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
     | FixRule (f,n,rest,j) ->
@@ -545,9 +546,24 @@ let prim_refiner r sigma goal =
 		  ("Name "^string_of_id f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
-	      List.map (fun (_,_,c) -> mk_goal sign c) all
+	      Goal.list_map (fun sigma (_,_,c) ->
+				                   let (gl,ev,sig')=
+				                     Goal.V82.mk_goal sigma sign c
+						             (Goal.V82.extra sigma goal)
+						   in ((gl,ev),sig'))
+		                              all sigma
 	in
-	  (mk_sign sign all, sigma)
+	let (gls_evs,sigma) =  mk_sign sign all in
+	let (gls,evs) = List.split gls_evs in
+	let ids = List.map pi1 all in
+	let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+	let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
+	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+	let typarray = Array.of_list (List.map pi3 all) in
+	let bodies = Array.of_list evs in
+	let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
+	let sigma = Goal.V82.partial_solution sigma goal oterm in
+	(gls,sigma)
 
     | Cofix (f,others,j) ->
      	let rec check_is_coind env cl =
@@ -572,32 +588,55 @@ let prim_refiner r sigma goal =
               with
               |	Not_found ->
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
-	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
+	  | [] -> Goal.list_map (fun sigma(_,c) ->
+				                       let (gl,ev,sigma) =
+				                         Goal.V82.mk_goal sigma sign c
+							   (Goal.V82.extra sigma goal)
+						       in
+				                       ((gl,ev),sigma))
+	                                             all sigma                                      
      	in
-	  (mk_sign sign all, sigma)
+	let (gls_evs,sigma) =  mk_sign sign all in
+	let (gls,evs) = List.split gls_evs in
+	let (ids,types) = List.split all in
+	let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+	let typarray = Array.of_list types in
+	let bodies = Array.of_list evs in
+	let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in
+	let sigma = Goal.V82.partial_solution sigma goal oterm in
+        (gls,sigma)
 
     | Refine c ->
 	check_meta_variables c;
-	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
+	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
+	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
 
     (* Conversion rules *)
     | Convert_concl (cl',_) ->
 	check_typability env sigma cl';
 	if (not !check) || is_conv_leq env sigma cl' cl then
-          let sg = mk_goal sign cl' in
+          let (sg,ev,sigma) = mk_goal sign cl' in
+	  let sigma = Goal.V82.partial_solution sigma goal ev in
           ([sg], sigma)
 	else
 	  error "convert-concl rule passed non-converting term"
 
     | Convert_hyp (id,copt,ty) ->
-	([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
+	let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
+	let sigma = Goal.V82.partial_solution sigma goal ev in
+	([gl], sigma)
 
     (* And now the structural rules *)
     | Thin ids ->
 	let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
-	  ([mk_goal hyps concl], nsigma)
+	let (gl,ev,sigma) =
+	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
+	in
+	let sigma = Goal.V82.partial_solution sigma goal ev in
+	  ([gl], sigma)
 
     | ThinBody ids ->
 	let clear_aux env id =
@@ -606,7 +645,8 @@ let prim_refiner r sigma goal =
             env'
 	in
 	let sign' = named_context_val (List.fold_left clear_aux env ids) in
-     	let sg = mk_goal sign' cl in
+     	let (sg,ev,sigma) = mk_goal sign' cl in
+	let sigma = Goal.V82.partial_solution sigma goal ev in
      	  ([sg], sigma)
 
     | Move (withdep, hfrom, hto) ->
@@ -614,11 +654,15 @@ let prim_refiner r sigma goal =
 	  split_sign hfrom hto (named_context_of_val sign) in
   	let hyps' =
 	  move_hyp withdep toleft (left,declfrom,right) hto in
-  	  ([mk_goal hyps' cl], sigma)
+	let (gl,ev,sigma) = mk_goal hyps' cl in
+	let sigma = Goal.V82.partial_solution sigma goal ev in
+  	  ([gl], sigma)
 
     | Order ord ->
         let hyps' = reorder_val_context env sign ord in
-        ([mk_goal hyps' cl], sigma)
+	let (gl,ev,sigma) = mk_goal hyps' cl in
+	let sigma = Goal.V82.partial_solution sigma goal ev in
+        ([gl], sigma)
 
     | Rename (id1,id2) ->
         if !check & id1 <> id2 &&
@@ -626,12 +670,19 @@ let prim_refiner r sigma goal =
           error ((string_of_id id2)^" is already used.");
         let sign' = rename_hyp id1 id2 sign in
         let cl' = replace_vars [id1,mkVar id2] cl in
-          ([mk_goal sign' cl'], sigma)
+	let (gl,ev,sigma) = mk_goal sign' cl' in
+	let ev = Term.replace_vars [(id2,mkVar id1)] ev in
+	let sigma = Goal.V82.partial_solution sigma goal ev in
+          ([gl], sigma)
 
     | Change_evars ->
-        match norm_goal sigma goal with
-	    Some ngl -> ([ngl],sigma)
-          | None -> ([goal], sigma)
+	(* spiwack: a priori [Change_evars] is now devoid of operational content.
+	    The new proof engine keeping the evar_map up to date at all time.
+	    As a compatibility mesure I leave the rule. 
+	    It is possible that my assumption is wrong and some uses of 
+	    [Change_evars] are not subsumed by the new engine. In which
+	    case something has to be done here. (Feb. 2010) *)
+	([goal],sigma)
 
 (************************************************************************)
 (************************************************************************)
@@ -671,77 +722,3 @@ let proof_variable_index x =
     | [] -> raise Not_found
   in
   aux 1
-
-let prim_extractor subfun vl pft =
-  let cl = pft.goal.evar_concl in
-    match pft.ref with
-      | Some (Prim (Intro id), [spf]) ->
-	  (match kind_of_term (strip_outer_cast cl) with
-	    | Prod (_,ty,_) ->
-		let cty = subst_proof_vars vl ty in
-		  mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
-	    | LetIn (_,b,ty,_) ->
-		let cb = subst_proof_vars vl b in
-		let cty = subst_proof_vars vl ty in
-		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	    | _ -> error "Incomplete proof!")
-
-      | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) ->
-          let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
-	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
-                    subfun (add_proof_var id vl) spf2)
-
-      | Some (Prim (FixRule (f,n,others,j)),spfl) ->
-	  let firsts,lasts = list_chop j others in
-	  let all = Array.of_list (firsts@(f,n,cl)::lasts) in
-	  let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
-	  let names = Array.map (fun (f,_,_) -> Name f) all in
-	  let vn = Array.map (fun (_,n,_) -> n-1) all in
-	  let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
-            (add_proof_var f vl) others in
-	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkFix ((vn,j),(names,lcty,lfix))
-
-      | Some (Prim (Cofix (f,others,j)),spfl) ->
-	  let firsts,lasts = list_chop j others in
-	  let all = Array.of_list (firsts@(f,cl)::lasts) in
-	  let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
-	  let names  = Array.map (fun (f,_) -> Name f) all in
-	  let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
-            (add_proof_var f vl) others in
-	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkCoFix (j,(names,lcty,lfix))
-
-      | Some (Prim (Refine c),spfl) ->
-	  let mvl = collect_meta_variables c in
-	  let metamap = List.combine mvl (List.map (subfun vl) spfl) in
-	  let cc = subst_proof_vars vl c in
-	    plain_instance metamap cc
-
-      (* Structural and conversion rules do not produce any proof *)
-      | Some (Prim (Convert_concl (t,k)),[pf]) ->
-	  if k = DEFAULTcast then subfun vl pf
-	  else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
-      | Some (Prim (Convert_hyp _),[pf]) ->
-	  subfun vl pf
-
-      | Some (Prim (Thin _),[pf]) ->
-	  (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
-	  subfun vl pf
-
-      | Some (Prim (ThinBody _),[pf]) ->
-	  subfun vl pf
-
-      | Some (Prim (Move _|Order _),[pf]) ->
-	  subfun vl pf
-
-      | Some (Prim (Rename (id1,id2)),[pf]) ->
-	  subfun (rebind id1 id2 vl) pf
-
-      | Some (Prim Change_evars, [pf]) ->
-	  subfun vl pf
-
-      | Some _ -> anomaly "prim_extractor"
-
-      | None-> error "prim_extractor handed incomplete proof"
-
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0d56da382..560e57736 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -38,9 +38,6 @@ val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
 type proof_variable
 
-val prim_extractor :
-  (proof_variable list -> proof_tree -> constr)
-  -> proof_variable list -> proof_tree -> constr
 
 val proof_variable_index : identifier -> proof_variable list -> int
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f3658ad4b..6da73c2f6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -20,322 +20,115 @@ open Environ
 open Evd
 open Typing
 open Refiner
-open Proof_trees
 open Tacexpr
 open Proof_type
 open Lib
 open Safe_typing
 
-(*********************************************************************)
-(* Managing the proofs state                                         *)
-(* Mainly contributed by C. Murthy                                   *)
-(*********************************************************************)
+let refining = Proof_global.there_are_pending_proofs
+let check_no_pending_proofs = Proof_global.check_no_pending_proof
 
-type lemma_possible_guards = int list list
+let get_current_proof_name = Proof_global.get_current_proof_name
+let get_all_proof_names = Proof_global.get_all_proof_names
 
-type proof_topstate = {
-  mutable top_end_tac : tactic option;
-  top_init_tac : tactic option;
-  top_compute_guard : lemma_possible_guards;
-  top_goal : goal;
-  top_strength : Decl_kinds.goal_kind;
-  top_hook : declaration_hook }
+type lemma_possible_guards = Proof_global.lemma_possible_guards
 
-let proof_edits =
-  (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)
+let delete_proof = Proof_global.discard
+let delete_current_proof = Proof_global.discard_current
+let delete_all_proofs = Proof_global.discard_all
 
-let get_all_proof_names () = Edit.dom proof_edits
+let undo n = 
+  let p = Proof_global.give_me_the_proof () in
+  for i = 1 to n do
+    Proof.undo p
+  done
 
-let msg_proofs use_resume =
-  match Edit.dom proof_edits with
-    | [] -> (spc () ++ str"(No proof-editing in progress).")
-    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++
-	       str"." ++
-               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
-              	else (mt ()))
-)
-
-let undo_default = 50
-let undo_limit = ref undo_default
-
-(*********************************************************************)
-(*    Functions for decomposing and modifying the proof state        *)
-(*********************************************************************)
-
-let get_state () =
-  match Edit.read proof_edits with
-    | None -> errorlabstrm "Pfedit.get_state"
-          (str"No focused proof" ++ msg_proofs true)
-    | Some(_,pfs,ts) -> (pfs,ts)
-
-let get_topstate ()    = snd(get_state())
-let get_pftreestate () = fst(get_state())
-
-let get_end_tac () = let ts = get_topstate () in ts.top_end_tac
-
-let get_goal_context n =
-  let pftree = get_pftreestate () in
-  let goal = nth_goal_of_pftreestate n pftree in
-  (project goal, pf_env goal)
-
-let get_current_goal_context () = get_goal_context 1
-
-let set_current_proof = Edit.focus proof_edits
-
-let resume_proof (loc,id) =
+let current_proof_depth () =
   try
-    Edit.focus proof_edits id
-  with Invalid_argument "Edit.focus" ->
-    user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
+    let p = Proof_global.give_me_the_proof () in
+    Proof.V82.depth p
+  with Proof_global.NoCurrentProof -> -1
 
-let suspend_proof () =
+(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
+   is the depth of the focus stack). *)
+let undo_todepth n =
   try
-    Edit.unfocus proof_edits
-  with Invalid_argument "Edit.unfocus" ->
-    errorlabstrm "Pfedit.suspend_current_proof"
-      (str"No active proof" ++ (msg_proofs true))
-
-let resume_last_proof () =
-  match (Edit.last_focused proof_edits) with
-    | None ->
-        errorlabstrm "resume_last" (str"No proof-editing in progress.")
-    | Some p ->
-	Edit.focus proof_edits p
+    undo ((current_proof_depth ()) - n )
+  with Proof_global.NoCurrentProof  when n=0 -> ()
 
-let get_current_proof_name () =
-  match Edit.read proof_edits with
-    | None ->
-        errorlabstrm "Pfedit.get_proof"
-          (str"No focused proof" ++ msg_proofs true)
-    | Some(na,_,_) -> na
+let set_undo _ = ()
+let get_undo _ = None
 
-let add_proof (na,pfs,ts) =
-  Edit.create proof_edits (na,pfs,ts,!undo_limit+1)
 
-let delete_proof_gen = Edit.delete proof_edits
-
-let delete_proof (loc,id) =
-  try
-    delete_proof_gen id
-  with (UserError ("Edit.delete",_)) ->
-    user_err_loc
-      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
-
-let mutate f =
-  try
-    Edit.mutate proof_edits (fun _ pfs -> f pfs)
-  with Invalid_argument "Edit.mutate" ->
-    errorlabstrm "Pfedit.mutate"
-      (str"No focused proof" ++ msg_proofs true)
-
-let start (na,ts) =
-  let pfs = mk_pftreestate ts.top_goal in
-  let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
-  add_proof(na,pfs,ts)
+let start_proof id str hyps c ?init_tac ?compute_guard hook = 
+  let goals = [ (Global.env_of_context hyps , c) ] in
+  let init_tac = Option.map Proofview.V82.tactic init_tac in
+  Proof_global.start_proof id str goals ?compute_guard hook;
+  Option.iter Proof_global.run_tactic init_tac
 
 let restart_proof () =
-  match Edit.read proof_edits with
-    | None ->
-	errorlabstrm "Pfedit.restart"
-          (str"No focused proof to restart" ++ msg_proofs true)
-    | Some(na,_,ts) ->
-	delete_proof_gen na;
-        start (na,ts);
-        set_current_proof na
-
-let proof_term () =
-  extract_pftreestate (get_pftreestate())
-
-(* Detect is one has completed a subtree of the initial goal *)
-let subtree_solved () =
-  let pts = get_pftreestate () in
-  is_complete_proof (proof_of_pftreestate pts) &
-  not (is_top_pftreestate pts)
-
-let tree_solved () =
-  let pts = get_pftreestate () in
-  is_complete_proof (proof_of_pftreestate pts)
-
-let top_tree_solved () =
-  let pts = get_pftreestate () in
-  is_complete_proof (proof_of_pftreestate (top_of_tree pts))
-
-(*********************************************************************)
-(*                 Undo functions                                    *)
-(*********************************************************************)
-
-let set_undo = function
-  | None -> undo_limit := undo_default
-  | Some n ->
-      if n>=0 then
-	undo_limit := n
-      else
-	error "Cannot set a negative undo limit"
-
-let get_undo () = Some !undo_limit
-
-let undo n =
-  try
-    Edit.undo proof_edits n;
-       (* needed because the resolution of a subtree is done in 2 steps
-       then a sequence of undo can lead to a focus on a completely solved
-       subtree - this solution only works properly if undoing one step *)
-    if subtree_solved() then  Edit.undo proof_edits 1
-  with (Invalid_argument "Edit.undo") ->
-    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
-
-(* Undo current focused proof to reach depth [n]. This is used in
-   [vernac_backtrack]. *)
-let undo_todepth n =
-  try
-    Edit.undo_todepth proof_edits n
-  with (Invalid_argument "Edit.undo") ->
-    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
-
-(* Return the depth of the current focused proof stack, this is used
-   to put informations in coq prompt (in emacs mode). *)
-let current_proof_depth() =
-  try
-    Edit.depth proof_edits
-  with (Invalid_argument "Edit.depth") -> -1
-
-(*********************************************************************)
-(*                  Proof cooking                                    *)
-(*********************************************************************)
+  let p = Proof_global.give_me_the_proof () in
+  try while true do
+    Proof.undo p
+  done with Proof.EmptyUndoStack -> ()
+
+let resume_last_proof () = Proof_global.resume_last ()
+let resume_proof (_,id) = Proof_global.resume id
+let suspend_proof ()  =  Proof_global.suspend ()
+
+let cook_proof hook =
+  let prf = Proof_global.give_me_the_proof () in
+  hook prf;
+  match Proof_global.close_proof () with
+  | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
+  | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term."
 
 let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
 
-let cook_proof k =
-  let (pfs,ts) = get_state()
-  and ident = get_current_proof_name () in
-  let {evar_concl=concl} = ts.top_goal
-  and strength = ts.top_strength in
-  let pfterm = extract_pftreestate pfs in
-  !xml_cook_proof (strength,pfs);
-  k pfs;
-  (ident,
-   ({ const_entry_body = pfterm;
-      const_entry_type = Some concl;
-      const_entry_opaque = true;
-      const_entry_boxed = false},
-    ts.top_compute_guard, strength, ts.top_hook))
-
-let current_proof_statement () =
-  let ts = get_topstate() in
-  (get_current_proof_name (), ts.top_strength,
-   ts.top_goal.evar_concl, ts.top_hook)
-
-(*********************************************************************)
-(*              Abort   functions                                    *)
-(*********************************************************************)
-
-let refining () = [] <> (Edit.dom proof_edits)
-
-let check_no_pending_proofs () =
-  if refining () then
-    errorlabstrm "check_no_pending_proofs"
-      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
-         str"Use \"Abort All\" first or complete proof(s).")
+let get_pftreestate () =
+  Proof_global.give_me_the_proof ()
 
-let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
-
-let delete_all_proofs () = Edit.clear proof_edits
-
-(*********************************************************************)
-(*   Modifying the end tactic of the current profftree               *)
-(*********************************************************************)
 let set_end_tac tac =
-  let top = get_topstate () in
-  top.top_end_tac <- Some tac
-
-(*********************************************************************)
-(*              Modifying the current prooftree                      *)
-(*********************************************************************)
-
-let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook =
-  let top_goal = mk_goal sign concl None in
-  let ts = {
-    top_end_tac = None;
-    top_init_tac = init_tac;
-    top_compute_guard = compute_guard;
-    top_goal = top_goal;
-    top_strength = str;
-    top_hook = hook}
-  in
-  start(na,ts);
-  set_current_proof na
-
-let solve_nth k tac =
-  let pft = get_pftreestate () in
-  if not (List.mem (-1) (cursor_of_pftreestate pft)) then
-    mutate (solve_nth_pftreestate k tac)
-  else
-    error "cannot apply a tactic when we are descended behind a tactic-node"
-
-let by tac = mutate (solve_pftreestate tac)
-
-let instantiate_nth_evar_com n c =
-  mutate (Evar_refiner.instantiate_pf_com n c)
+  let tac = Proofview.V82.tactic tac in
+  Proof_global.set_endline_tactic tac
 
-let traverse n = mutate (traverse n)
-
-(* [traverse_to path]
-
-   Traverses the current proof to get to the location specified by
-   [path].
-
-   ALGORITHM: The algorithm works on reversed paths. One just has to remove
-   the common part on the reversed paths.
-
-*)
-
-let common_ancestor l1 l2 =
-  let rec common_aux l1 l2 =
-    match l1, l2 with
-      | a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2'
-      | _, _ -> List.rev l1, List.length l2
-  in
-  common_aux (List.rev l1) (List.rev l2)
-
-let rec traverse_up = function
-  | 0 -> (function pf -> pf)
-  | n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf))
-
-let rec traverse_down = function
-  | [] -> (function pf -> pf)
-  | n::l -> (function pf -> Refiner.traverse n (traverse_down l pf))
-
-let traverse_to path =
-  let up_and_down path pfs =
-    let cursor = cursor_of_pftreestate pfs in
-    let down_list, up_count = common_ancestor path cursor in
-    traverse_down down_list (traverse_up up_count pfs)
-  in
-  mutate (up_and_down path)
-
-(* traverse the proof tree until it reach the nth subgoal *)
-let traverse_nth_goal n = mutate (nth_unproven n)
-
-let traverse_prev_unproven () = mutate prev_unproven
-
-let traverse_next_unproven () = mutate next_unproven
+let get_goal_context i =
+  try
+    let p = Proof_global.give_me_the_proof () in
+    let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in
+    let goal = List.nth goals (i-1) in
+    (sigma, Refiner.pf_env { it=goal ; sigma=sigma })
+  with Proof_global.NoCurrentProof -> Util.error "No focused proof."
 
-(* The goal focused on *)
-let focus_n = ref 0
-let make_focus n = focus_n := n
-let focus () = !focus_n
-let focused_goal () = let n = !focus_n in if n=0 then 1 else n
+let get_current_goal_context () = get_goal_context 1
 
-let reset_top_of_tree () =
-  mutate top_of_tree
+let current_proof_statement () =
+  match Proof_global.V82.get_current_initial_conclusions () with
+    | (id,([concl],strength,hook)) -> id,strength,concl,hook
+    | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement"
+
+let solve_nth ?(with_end_tac=false) gi tac = 
+  try 
+    let tac = Proofview.V82.tactic tac in
+    let tac = if with_end_tac then 
+                Proof_global.with_end_tac tac
+              else
+		tac
+    in
+    Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) 
+  with 
+    | Proof_global.NoCurrentProof  -> Util.error "No focused proof"
+    | Proofview.IndexOutOfRange | Failure "list_chop" -> 
+	let msg = str "No such goal: " ++ int gi ++ str "." in
+	Util.errorlabstrm "" msg
+
+let by = solve_nth 1
+
+let instantiate_nth_evar_com n com = 
+  let pf = Proof_global.give_me_the_proof () in
+  Proof.V82.instantiate_evar n com pf
 
-let reset_top_of_script () =
-  mutate (fun pts ->
-	try
-	 up_until_matching_rule is_proof_instr pts
-	with Not_found -> top_of_tree pts)
 
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index acb852471..9e24061d3 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -20,6 +20,7 @@ open Tacmach
 open Tacexpr
 (*i*)
 
+
 (*s Several proofs can be opened simultaneously but at most one is
    focused at some time. The following functions work by side-effect
    on current set of open proofs. In this module, ``proofs'' means an
@@ -57,17 +58,16 @@ val delete_all_proofs : unit -> unit
 
 val undo : int -> unit
 
-(* Same as undo, but undoes the current proof stack to reach depth
-   [n]. This is used in [vernac_backtrack]. *)
-val undo_todepth : int -> unit
+(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
+   is the depth of the undo stack). *)
+val undo_todepth : int -> unit 
 
 (* Returns the depth of the current focused proof stack, this is used
    to put informations in coq prompt (in emacs mode). *)
 val current_proof_depth: unit -> int
 
-(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
-   sets the size to the default value (12) *)
-
+(* [set_undo (Some n)] used to set the size of the ``undo'' stack. 
+    These function now do nothing and will disapear. *)
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
@@ -78,7 +78,7 @@ val get_undo : unit -> int option
     systematically apply at initialization time (e.g. to start the
     proof of mutually dependent theorems) *)
 
-type lemma_possible_guards = int list list
+type lemma_possible_guards = Proof_global.lemma_possible_guards
 
 val start_proof :
   identifier -> goal_kind -> named_context_val -> constr ->
@@ -110,22 +110,18 @@ val suspend_proof : unit -> unit
     it fails if there is no current proof of if it is not completed;
     it also tells if the guardness condition has to be inferred. *)
 
-val cook_proof : (Refiner.pftreestate -> unit) ->
+val cook_proof : (Proof.proof -> unit) ->
   identifier *
-  (Entries.definition_entry * lemma_possible_guards * goal_kind * 
-   declaration_hook)
+    (Entries.definition_entry * lemma_possible_guards * goal_kind *
+     declaration_hook)
 
 (* To export completed proofs to xml *)
-val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
+val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
 
-(*s [get_pftreestate ()] returns the current focused pending proof or
+(*s [get_Proof.proof ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
 
-val get_pftreestate : unit -> pftreestate
-
-(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
-
-val get_end_tac : unit -> tactic option
+val get_pftreestate : unit -> Proof.proof
 
 (* [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
@@ -160,7 +156,7 @@ val set_end_tac : tactic -> unit
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
 
-val solve_nth : int -> tactic -> unit
+val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit
 
 (* [by tac] applies tactic [tac] to the 1st subgoal of the current
    focused proof or raises a UserError if there is no focused proof or
@@ -175,31 +171,6 @@ val by : tactic -> unit
 
 val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
 
-(*s To deal with subgoal focus *)
-
-val make_focus : int -> unit
-val focus : unit -> int
-val focused_goal : unit -> int
-val subtree_solved : unit -> bool
-val tree_solved : unit -> bool
-val top_tree_solved : unit -> bool
-
-val reset_top_of_tree : unit -> unit
-val reset_top_of_script : unit -> unit
-
-val traverse : int -> unit
-val traverse_nth_goal : int -> unit
-val traverse_next_unproven : unit -> unit
-val traverse_prev_unproven : unit -> unit
-
-
-(* These two functions make it possible to implement more elaborate
-   proof and goal management, as it is done, for instance in pcoq *)
-
-val traverse_to : int list -> unit
-val mutate : (pftreestate -> pftreestate) -> unit
-
-
 (* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
 val build_constant_by_tactic : named_context_val -> types -> tactic ->
diff --git a/proofs/proof.ml b/proofs/proof.ml
new file mode 100644
index 000000000..0c298cc63
--- /dev/null
+++ b/proofs/proof.ml
@@ -0,0 +1,294 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* Module defining the last essential tiles of interactive proofs.
+   The features of the Proof module are undoing and focusing.
+   A proof is a mutable object, it contains a proofview, and some information
+   to be able to undo actions, and to unfocus the current view. All three
+   of these being meant to evolve.
+   - Proofview: a proof is primarily the data of the current view.
+     That which is shown to the user (as a remainder, a proofview
+     is mainly the logical state of the proof, together with the
+     currently focused goals).
+   - Focus: a proof has a focus stack: the top of the stack contains
+     the context in which to unfocus the current view to a view focused
+     with the rest of the stack.
+     In addition, this contains, for each of the focus context,  a 
+     "focus kind" and a "focus condition" (in practice, and for modularity,
+     the focus kind is actually stored inside the condition). To unfocus, one
+     needs to know the focus kind, and the condition (for instance "no condition" or
+     the proof under focused must be complete) must be met.
+   - Undo: since proofviews and focus stacks are immutable objects, 
+     it could suffice to hold the previous states, to allow to return to the past.
+     However, we also allow other modules to do actions that can be undone.
+     Therefore the undo stack stores action to be ran to undo.
+*)
+
+open Term
+
+type focus_kind = int
+type focus_condition = focus_kind -> Proofview.proofview -> bool
+
+let next_kind = ref 0
+let new_focus_kind () =
+  let r = !next_kind in
+  incr next_kind;
+  r
+
+(* To be authorized to unfocus one must meet the condition prescribed by
+    the action which focused.*)
+(* spiwack: we could consider having a list of authorized focus_kind instead
+    of just one, if anyone needs it *)
+(* [no_cond] only checks that the unfocusing command uses the right
+    [focus_kind]. *)
+let no_cond k0 k _ = k0 = k
+(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
+    and that the focused proofview is complete. *)
+let done_cond k0 k p = k0 = k && Proofview.finished p
+
+
+(* Subpart of the type of proofs. It contains the parts of the proof which
+   are under control of the undo mechanism *)
+type proof_state = {
+  (* Current focused proofview *)
+  proofview: Proofview.proofview;
+  (* History of the focusings, provides information on how
+     to unfocus the proof.
+     The list is empty when the proof is fully unfocused. *)
+  focus_stack: (focus_condition*Proofview.focus_context) list;
+  (* Extra information which can be freely used to create new behaviours. *)
+  intel: Store.t
+}
+
+type proof_info = {
+  mutable endline_tactic : unit Proofview.tactic ;
+  initial_conclusions : Term.types list
+}
+
+type undo_action = 
+  | State of proof_state
+  | Effect of (unit -> unit)
+
+type proof = { (* current proof_state *)
+               mutable state : proof_state;
+               (* The undo stack *)
+               mutable undo_stack : undo_action list;
+	       info : proof_info
+             }
+
+
+(*** General proof functions ***)
+
+let start goals =
+  { state = { proofview = Proofview.init goals ;
+	             focus_stack = [] ;
+	             intel = Store.empty} ;
+      undo_stack = [] ;
+      info = { endline_tactic = Proofview.tclUNIT ();
+	            initial_conclusions = List.map snd goals }
+  }
+
+let rec unroll_focus pv = function
+  | (_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
+  | [] -> pv
+
+(* spiwack: a proof is considered completed even if its still focused, if the focus
+                   doesn't hide any goal. *)
+let is_done p =
+  Proofview.finished p.state.proofview && 
+  Proofview.finished (unroll_focus p.state.proofview p.state.focus_stack)
+
+(* spiwack: for compatibility with <= 8.2 proof engine *)
+let has_unresolved_evar p =
+  Proofview.V82.has_unresolved_evar p.state.proofview
+
+(* Returns the list of partial proofs to initial goals *)
+let partial_proof p =
+  List.map fst (Proofview.return p.state.proofview)
+
+exception UnfinishedProof
+exception HasUnresolvedEvar
+let return p =
+  if not (is_done p) then
+    raise UnfinishedProof
+  else if has_unresolved_evar p then 
+    (* spiwack: for compatibility with <= 8.2 proof engine *)
+    raise HasUnresolvedEvar
+  else
+    Proofview.return p.state.proofview
+
+(*** The following functions implement the basic internal mechanisms
+     of proofs, they are not meant to be exported in the .mli ***)
+
+(* An auxiliary function to push a {!focus_context} on the focus stack. *)
+let push_focus kind context pr =
+  pr.state <- { pr.state with focus_stack = (kind,context)::pr.state.focus_stack }
+
+exception FullyUnfocused
+
+(* An auxiliary function to read the kind of the next focusing step *)
+let cond_of_focus pr =
+  match pr.state.focus_stack with
+  | (cond,_)::_ -> cond
+  | _ -> raise FullyUnfocused
+
+(* An auxiliary function to pop and read the last {!Proofview.focus_context} 
+   on the focus stack. *)
+let pop_focus pr =
+  match pr.state.focus_stack with
+  | focus::other_focuses -> 
+      pr.state <- { pr.state with focus_stack = other_focuses }; focus
+  | _ -> 
+      raise FullyUnfocused
+
+(* Auxiliary function to push a [proof_state] onto the undo stack. *)
+let push_undo save ({ undo_stack = stack } as pr) =
+  pr.undo_stack <- save::stack
+
+(* Auxiliary function to pop and read a [save_state] from the undo stack. *)
+exception EmptyUndoStack
+let pop_undo pr = 
+  match pr.undo_stack with
+  | state::stack -> pr.undo_stack <- stack; state
+  | _ -> raise EmptyUndoStack
+
+
+(* This function focuses the proof [pr] between indices [i] and [j] *)
+let _focus cond i j pr =
+  let (focused,context) = Proofview.focus i j pr.state.proofview in
+  push_focus cond context pr;
+  pr.state <- { pr.state with proofview = focused }
+
+(* This function unfocuses the proof [pr], it raises [CannotUnfocus],
+   if the proof is already fully unfocused.
+   This function does not care about the condition of the current focus. *)
+let _unfocus pr =
+  let (_,fc) = pop_focus pr in
+  pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
+
+
+(*** Endline tactic ***)
+
+(* spiwack this is an information about the UI, it might be a good idea to move
+   it to the Proof_global module *)
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac p =
+ p.info.endline_tactic <- tac
+
+let with_end_tac pr tac =
+  Proofview.tclTHEN tac pr.info.endline_tactic
+
+(*** The following functions define the safety mechanism of the
+     proof system, they may be unsafe if not used carefully. There is
+     currently no reason to export them in the .mli ***)
+
+(* This functions saves the current state into a [proof_state]. *)
+let save_state { state = ps } = State ps
+
+(* This function stores the current proof state in the undo stack. *)
+let save pr =
+  push_undo (save_state pr) pr
+
+(* This function restores a state, presumably from the top of the undo stack. *)
+let restore_state save pr = 
+  match save with
+  | State save -> pr.state <- save
+  | Effect undo -> undo ()
+
+(* Interpretes the Undo command. *)
+let undo pr = 
+  (* On a single line, since the effects commute *)
+  restore_state (pop_undo pr) pr
+
+(* Adds an undo effect to the undo stack. Use it with care, errors here might result
+    in inconsistent states. *)
+let add_undo effect pr =
+  push_undo (Effect effect) pr
+
+(* Focus command (focuses on the [i]th subgoal) *)
+(* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
+   a need for it? *)
+let focus cond i pr =
+  save pr;
+  _focus cond i i pr
+
+(* Unfocus command.
+   Fails if the proof is not focused. *)
+let unfocus kind pr =
+  let starting_point = save_state pr in
+  try
+    let cond = cond_of_focus pr in
+    if cond kind pr.state.proofview then
+      (_unfocus pr;
+       push_undo starting_point pr)
+    else
+      Util.error "This proof is focused, but cannot be unfocused this way"
+  with FullyUnfocused -> 
+    Util.error "This proof is not focused"
+
+let no_focused_goal p =
+  Proofview.finished p.state.proofview
+
+(*** Function manipulation proof extra informations ***)
+
+let get_proof_info pr =
+  pr.state.intel
+
+let set_proof_info info pr =
+  save pr;
+  pr.state <- { pr.state with intel=info }
+
+
+(*** Tactics ***)
+
+let run_tactic env tac pr =
+  let starting_point = save_state pr in
+  let sp = pr.state.proofview in
+  try
+    let tacticced_proofview = Proofview.apply env tac sp in
+    pr.state <- { pr.state with proofview = tacticced_proofview };
+    push_undo starting_point pr
+  with e -> 
+    restore_state starting_point pr;
+    raise e
+  
+
+
+(*** Compatibility layer with <=v8.2 ***)
+module V82 = struct
+  let subgoals p =
+    Proofview.V82.goals p.state.proofview
+
+  let background_subgoals p =
+    Proofview.V82.goals (unroll_focus p.state.proofview p.state.focus_stack)
+
+  let get_initial_conclusions p = 
+    p.info.initial_conclusions
+
+  let depth p = List.length p.undo_stack
+
+  let top_goal p = 
+    let { Evd.it=gls ; sigma=sigma } = 
+	Proofview.V82.top_goals p.state.proofview
+    in
+    { Evd.it=List.hd gls ; sigma=sigma }
+
+  let instantiate_evar n com pr =
+    let starting_point = save_state pr in
+    let sp = pr.state.proofview in
+    try
+      let new_proofview = Proofview.V82.instantiate_evar n com sp in
+      pr.state <- { pr.state with proofview = new_proofview };
+      push_undo starting_point pr
+    with e -> 
+      restore_state starting_point pr;
+      raise e
+end
diff --git a/proofs/proof.mli b/proofs/proof.mli
new file mode 100644
index 000000000..2b1c3f5c2
--- /dev/null
+++ b/proofs/proof.mli
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: proof.mli aspiwack $ *)
+
+(* Module defining the last essential tiles of interactive proofs.
+   The features of the Proof module are undoing and focusing.
+   A proof is a mutable object, it contains a proofview, and some information
+   to be able to undo actions, and to unfocus the current view. All three
+   of these being meant to evolve.
+   - Proofview: a proof is primarily the data of the current view.
+     That which is shown to the user (as a remainder, a proofview
+     is mainly the logical state of the proof, together with the
+     currently focused goals).
+   - Focus: a proof has a focus stack: the top of the stack contains
+     the context in which to unfocus the current view to a view focused
+     with the rest of the stack.
+     In addition, this contains, for each of the focus context,  a 
+     "focus kind" and a "focus condition" (in practice, and for modularity,
+     the focus kind is actually stored inside the condition). To unfocus, one
+     needs to know the focus kind, and the condition (for instance "no condition" or
+     the proof under focused must be complete) must be met.
+   - Undo: since proofviews and focus stacks are immutable objects, 
+     it could suffice to hold the previous states, to allow to return to the past.
+     However, we also allow other modules to do actions that can be undone.
+     Therefore the undo stack stores action to be ran to undo.
+*)
+
+open Term
+
+(* Type of a proof. *)
+type proof
+
+
+(*** General proof functions ***)
+
+val start : (Environ.env * Term.types) list -> proof
+
+(* Returns [true] is the considered proof is completed, that is if no goal remain
+    to be considered (this does not require that all evars have been solved). *)
+val is_done : proof -> bool
+
+(* Returns the list of partial proofs to initial goals. *)
+val partial_proof : proof -> Term.constr list
+
+(* Returns the proofs (with their type) of the initial goals.
+    Raises [UnfinishedProof] is some goals remain to be considered.
+    Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
+exception UnfinishedProof
+exception HasUnresolvedEvar
+val return : proof -> (Term.constr * Term.types) list
+
+(* Interpretes the Undo command. Raises [EmptyUndoStack] if 
+    the undo stack is empty. *)
+exception EmptyUndoStack
+val undo : proof -> unit
+
+(* Adds an undo effect to the undo stack. Use it with care, errors here might result
+    in inconsistent states. *)
+val add_undo : (unit -> unit) -> proof -> unit
+
+(*** Focusing actions ***)
+
+(* [focus_kind] is the type used by focusing and unfocusing
+    commands to synchronise. Focusing and unfocusing commands use
+    a particular focus_kind, and if they don't match, the unfocusing command
+    will fail. *)
+type focus_kind
+val new_focus_kind : unit -> focus_kind
+
+(* To be authorized to unfocus one must meet the condition prescribed by
+    the action which focused.*)
+type focus_condition 
+(* [no_cond] only checks that the unfocusing command uses the right
+    [focus_kind]. *)
+val no_cond : focus_kind -> focus_condition
+(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
+    and that the focused proofview is complete. *)
+val done_cond : focus_kind -> focus_condition
+
+(* focus command (focuses on the [i]th subgoal) *)
+(* there could also, easily be a focus-on-a-range tactic, is there 
+   a need for it? *)
+val focus : focus_condition -> int -> proof -> unit
+
+exception FullyUnfocused
+(* Unfocusing command.
+   Raises [FullyUnfocused] if the proof is not focused. *)
+val unfocus : focus_kind -> proof -> unit
+
+(* returns [true] if there is no goal under focus. *)
+val no_focused_goal : proof -> bool
+
+(*** Function manipulation proof extra informations ***)
+
+val get_proof_info : proof -> Store.t
+
+val set_proof_info : Store.t -> proof -> unit
+
+
+(*** Endline tactic ***)
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+val set_endline_tactic : unit Proofview.tactic -> proof -> unit
+
+val with_end_tac : proof -> unit Proofview.tactic -> unit Proofview.tactic
+
+(*** Tactics ***)
+
+val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
+
+
+(*** Compatibility layer with <=v8.2 ***)
+module V82 : sig
+  val subgoals : proof -> Goal.goal list Evd.sigma
+
+  (* All the subgoals of the proof, including those which are not focused. *)
+  val background_subgoals : proof -> Goal.goal list Evd.sigma
+
+  val get_initial_conclusions : proof -> Term.types list 
+
+  val depth : proof -> int 
+
+  val top_goal : proof -> Goal.goal Evd.sigma
+
+  (* Implements the Existential command *)
+  val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
+end
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
new file mode 100644
index 000000000..420ff8432
--- /dev/null
+++ b/proofs/proof_global.ml
@@ -0,0 +1,295 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(*      This module defines the global proof environment               *)
+(*      In particular it keeps tracks of whether or not there is          *)
+(*      a proof which is currently being edited.                       *)
+(*                                                                     *)
+(***********************************************************************)
+
+open Pp
+open Names
+
+(*** Proof Modes ***)
+
+(* Type of proof modes :
+    - A function [set] to set it *from standard mode*
+    - A function [reset] to reset the *standard mode* from it *)
+type proof_mode = {
+  name : string ;
+  set : unit -> unit ;
+  reset : unit -> unit
+}
+
+let proof_modes = Hashtbl.create 6
+let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m
+(* initial mode: standard mode *)
+let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
+let _ = register_proof_mode standard
+
+(* Default proof mode, to be set at the beginning of proofs. *)
+let default_proof_mode = ref standard
+
+let set_default_proof_mode = 
+  Goptions.declare_string_option {Goptions.
+    optsync = true ;
+    optname = "default proof mode" ;
+    optkey = ["Default";"Proof";"Mode"] ;
+    optread = begin fun () -> 
+                               let { name = name } = !default_proof_mode in name 
+                     end;
+    optwrite = begin fun n -> 
+                                default_proof_mode := Hashtbl.find proof_modes n
+                      end
+  }
+
+(*** Proof Global Environment ***)
+
+(* local shorthand *)
+type nproof = identifier*Proof.proof
+
+(* Extra info on proofs. *)
+type lemma_possible_guards = int list list
+type proof_info = { 
+  strength : Decl_kinds.goal_kind ;
+  compute_guard :  lemma_possible_guards; 
+  hook :Tacexpr.declaration_hook ;
+  mode : proof_mode
+}
+
+(* Invariant: a proof is at most in one of current_proof and suspended. And the 
+   domain of proof_info is the union of that of current_proof and suspended.*)
+(* The head of [!current_proof] is the actual current proof, the other ones are to
+    be resumed when the current proof is closed, aborted or suspended. *)
+let current_proof = ref ([]:nproof list)
+let suspended = ref ([] : nproof list)
+let proof_info = ref (Idmap.empty : proof_info Idmap.t)
+
+(* Current proof_mode, for bookkeeping *)
+let current_proof_mode = ref !default_proof_mode
+
+(* combinators for proof modes *)
+let update_proof_mode () = 
+  match !current_proof with
+  | (id,_)::_ ->  
+      let { mode = m } = Idmap.find id !proof_info in
+      !current_proof_mode.reset ();
+      current_proof_mode := m;
+      !current_proof_mode.set ()
+  | _ -> 
+      !current_proof_mode.reset (); 
+      current_proof_mode := standard
+
+(* combinators for the current_proof and suspended lists *)
+let push a l = l := a::!l;
+  update_proof_mode ()
+
+exception NoSuchProof
+let rec extract id l = 
+  let rec aux = function
+    | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
+    | np::l -> let (np', l) = aux l in (np' , np::l)
+    | [] -> raise NoSuchProof
+  in
+  let (np,l') = aux !l in
+  l := l';
+  update_proof_mode ();
+  np
+
+exception NoCurrentProof
+let extract_top l =
+  match !l with
+  | np::l' -> l := l' ; update_proof_mode (); np
+  | [] -> raise NoCurrentProof	
+let find_top l =
+  match !l with
+  | np::_ -> np
+  | [] -> raise NoCurrentProof
+
+let rotate_top l1 l2 =
+  let np = extract_top l1 in
+  push np l2
+
+let rotate_find id l1 l2 =
+  let np = extract id l1 in
+  push np l2
+  
+
+(* combinators for the proof_info map *)
+let add id info m =
+  m := Idmap.add id info !m
+let remove id m =
+  m := Idmap.remove id !m
+
+(*** Proof Global manipulation ***)
+
+let get_all_proof_names () =
+    List.map fst !current_proof @
+    List.map fst !suspended
+
+let give_me_the_proof () = 
+  snd (find_top current_proof)
+
+let get_current_proof_name () =
+  fst (find_top current_proof)
+
+(* spiwack: it might be considered to move error messages away.
+    Or else to remove special exceptions from Proof_global.
+    Arguments for the former: there is no reason Proof_global is only
+    accessed directly through vernacular commands. Error message should be 
+   pushed to external layers, and so we should be able to have a finer
+   control on error message on complex actions. *)
+let msg_proofs use_resume =
+  match get_all_proof_names () with
+    | [] -> (spc () ++ str"(No proof-editing in progress).")
+    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
+               (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++
+	       str"." ++
+               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
+              	else (mt ()))
+	    )
+
+
+let there_is_a_proof () = !current_proof <> []
+let there_are_suspended_proofs () = !suspended <> []
+let there_are_pending_proofs () = 
+  there_is_a_proof () || 
+  there_are_suspended_proofs ()
+let check_no_pending_proof () = 
+  if not (there_are_pending_proofs ()) then
+    ()
+  else begin
+    pp_with Format.str_formatter
+      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+       str"Use \"Abort All\" first or complete proof(s).")   ;
+    Util.error (Format.flush_str_formatter ())
+  end
+
+
+let suspend () =
+  rotate_top current_proof suspended
+
+let resume_last () =
+  rotate_top suspended current_proof
+
+let resume id =
+  rotate_find id suspended current_proof
+
+let discard_gen id =
+  try 
+    ignore (extract id current_proof);
+    remove id proof_info
+  with NoSuchProof -> ignore (extract id suspended)
+
+let discard (loc,id) = 
+  try
+    discard_gen id
+  with NoSuchProof ->
+    Util.user_err_loc
+      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+
+let discard_current () =
+  let (id,_) = extract_top current_proof in
+  remove id proof_info
+ 
+let discard_all () =
+  current_proof := []; 
+  suspended := [];
+  proof_info := Idmap.empty
+
+(* [set_proof_mode] sets the proof mode to be used after it's called. It is
+    typically called by the Proof Mode command. *)
+(* Core component.
+    No undo handling.
+    Applies to proof [id], and proof mode [m]. *)
+let set_proof_mode m id = 
+  let info = Idmap.find id !proof_info in
+  let info = { info with mode = m } in
+  proof_info := Idmap.add id info !proof_info;
+  update_proof_mode ()
+(* Complete function.
+    Handles undo.
+    Applies to current proof, and proof mode name [mn]. *)
+let set_proof_mode mn =
+  let m = Hashtbl.find proof_modes mn in
+  let id = get_current_proof_name () in
+  let pr = give_me_the_proof () in
+  Proof.add_undo begin let curr = !current_proof_mode in fun () ->
+    set_proof_mode curr id ; update_proof_mode ()
+  end pr ;
+  set_proof_mode m id
+
+(* [start_proof s str env t hook tac] starts a proof of name [s] and
+    conclusion [t]; [hook] is optionally a function to be applied at
+    proof end (e.g. to declare the built constructions as a coercion
+    or a setoid morphism); init_tac is possibly a tactic to
+    systematically apply at initialization time (e.g. to start the
+    proof of mutually dependent theorems).
+    It raises exception [ProofInProgress] if there is a proof being
+    currently edited. *)
+let start_proof  id str goals ?(compute_guard=[]) hook =
+  (* arnaud: ajouter une vérification pour la présence de id dans le proof_global *)
+  let p = Proof.start goals in
+  add id { strength=str ; 
+	        compute_guard=compute_guard ; 
+		hook=hook ;
+	        mode = ! default_proof_mode } proof_info ;
+  push (id,p) current_proof
+
+(* arnaud: à enlever *)
+let run_tactic tac = 
+  let p = give_me_the_proof () in
+  let env = Global.env () in
+  Proof.run_tactic env tac p
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac =
+  let p = give_me_the_proof () in
+  Proof.set_endline_tactic tac p
+
+let with_end_tac tac =
+  let p = give_me_the_proof () in
+  Proof.with_end_tac p tac
+
+let close_proof () =
+  (* spiwack: for now close_proof doesn't actually discard the proof, it is done
+      by [Command.save]. *)
+  try 
+    let id = get_current_proof_name () in
+    let p = give_me_the_proof () in
+    let proofs_and_types = Proof.return p in
+    let entries = List.map (fun (c,t) -> { Entries.const_entry_body = c ;
+                                    					   const_entry_type  = Some t;
+									   const_entry_opaque = true ;
+									   const_entry_boxed = false } )
+                                         proofs_and_types 
+    in
+    let { compute_guard=cg ; strength=str ; hook=hook } =
+      Idmap.find id !proof_info
+    in
+    (id, (entries,cg,str,hook))
+  with 
+    |  Proof.UnfinishedProof ->
+	 Util.error "Attempt to save an incomplete proof"
+    | Proof.HasUnresolvedEvar ->
+	Util.error "Attempt to save a proof with existential variables still non-instantiated"
+
+module V82 = struct
+  let get_current_initial_conclusions () =
+    let p = give_me_the_proof () in
+    let id = get_current_proof_name () in
+    let { strength=str ; hook=hook } = 
+      Idmap.find id !proof_info
+    in
+    (id,(Proof.V82.get_initial_conclusions p, str, hook))
+end
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
new file mode 100644
index 000000000..84a61c755
--- /dev/null
+++ b/proofs/proof_global.mli
@@ -0,0 +1,89 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(***********************************************************************)
+(*                                                                     *)
+(*      This module defines the global proof environment               *)
+(*      Especially it keeps tracks of whether or not there is          *)
+(*      a proof which is currently being edited.                       *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Type of proof modes :
+    - A name
+    - A function [set] to set it *from standard mode*
+    - A function [reset] to reset the *standard mode* from it *)
+type proof_mode = {
+  name : string ;
+  set : unit -> unit ;
+  reset : unit -> unit
+}
+(* Registers a new proof mode which can then be adressed by name
+    in [set_default_proof_mode].
+    One mode is already registered - the standard mode - named "No",
+    It corresponds to Coq default setting are they are set when coqtop starts. *)
+val register_proof_mode : proof_mode -> unit
+
+val there_is_a_proof : unit -> bool
+val there_are_pending_proofs : unit -> bool
+val check_no_pending_proof : unit -> unit
+
+val get_current_proof_name : unit -> Names.identifier
+val get_all_proof_names : unit -> Names.identifier list
+
+val discard : Names.identifier Util.located -> unit
+val discard_current : unit -> unit
+val discard_all : unit -> unit
+
+(* [set_proof_mode] sets the proof mode to be used after it's called. It is
+    typically called by the Proof Mode command. *)
+val set_proof_mode : string -> unit
+
+exception NoCurrentProof
+val give_me_the_proof : unit -> Proof.proof
+
+
+(* [start_proof s str goals ~init_tac ~compute_guard hook] starts 
+    a proof of name [s] and
+    conclusion [t]; [hook] is optionally a function to be applied at
+    proof end (e.g. to declare the built constructions as a coercion
+    or a setoid morphism). *)
+type lemma_possible_guards = int list list
+val start_proof : Names.identifier -> 
+                          Decl_kinds.goal_kind ->
+                          (Environ.env * Term.types) list  ->
+                          ?compute_guard:lemma_possible_guards -> 
+                          Tacexpr.declaration_hook -> 
+                          unit
+
+val close_proof : unit -> 
+                           Names.identifier * 
+                          (Entries.definition_entry list * 
+			    lemma_possible_guards * 
+			    Decl_kinds.goal_kind * 
+			    Tacexpr.declaration_hook)
+
+val suspend : unit -> unit
+val resume_last : unit -> unit
+val resume : Names.identifier -> unit
+
+(* Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
+   no current proof. *)
+val run_tactic : unit Proofview.tactic -> unit
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+val set_endline_tactic : unit Proofview.tactic -> unit
+
+(* Appends the endline tactic of the current proof to a tactic. *)
+val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
+
+module V82 : sig
+  val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
+end
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
deleted file mode 100644
index a5bd073a3..000000000
--- a/proofs/proof_trees.ml
+++ /dev/null
@@ -1,107 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Closure
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Sign
-open Evd
-open Environ
-open Evarutil
-open Decl_expr
-open Proof_type
-open Tacred
-open Typing
-open Libnames
-open Nametab
-
-(*
-let is_bind = function
-  | Tacexpr.Cbindings _ -> true
-  | _ -> false
-*)
-
-(* Functions on goals *)
-
-let mk_goal hyps cl extra =
-  { evar_hyps = hyps; evar_concl = cl;
-    evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
-    evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar); 
-    evar_extra = extra }
-
-(* Functions on proof trees *)
-
-let ref_of_proof pf =
-  match pf.ref with
-    | None -> failwith "rule_of_proof"
-    | Some r -> r
-
-let rule_of_proof pf =
-  let (r,_) = ref_of_proof pf in r
-
-let children_of_proof pf =
-  let (_,cl) = ref_of_proof pf in cl
-
-let goal_of_proof pf = pf.goal
-
-let subproof_of_proof pf = match pf.ref with
-  | Some (Nested (_,pf), _) -> pf
-  | _ -> failwith "subproof_of_proof"
-
-let status_of_proof pf = pf.open_subgoals
-
-let is_complete_proof pf = pf.open_subgoals = 0
-
-let is_leaf_proof pf = (pf.ref = None)
-
-let is_tactic_proof pf = match pf.ref with
-  | Some (Nested (Tactic _,_),_) -> true
-  | _ -> false
-
-
-let pf_lookup_name_as_displayed env ccl s =
-  Detyping.lookup_name_as_displayed env ccl s
-
-let pf_lookup_index_as_renamed env ccl n =
-  Detyping.lookup_index_as_renamed env ccl n
-
-(* Functions on rules (Proof mode) *)
-
-let is_dem_rule  = function
-    Decl_proof _  -> true
-  | _ -> false
-
-let is_proof_instr = function
-    Nested(Proof_instr (_,_),_) -> true
-  | _ -> false
-
-let is_focussing_command = function
-    Decl_proof b -> b
-  | Nested (Proof_instr (b,_),_) -> b
-  | _ -> false
-
-
-(*********************************************************************)
-(*                  Pretty printing functions                        *)
-(*********************************************************************)
-
-open Pp
-
-let db_pr_goal g =
-  let env = evar_env g in
-  let penv = print_named_context env in
-  let pc = print_constr_env env g.evar_concl in
-  str"  " ++ hv 0 (penv ++ fnl () ++
-                   str "============================" ++ fnl ()  ++
-                   str" "  ++ pc) ++ fnl ()
-
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
deleted file mode 100644
index 6d1fc143d..000000000
--- a/proofs/proof_trees.mli
+++ /dev/null
@@ -1,48 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Util
-open Names
-open Term
-open Sign
-open Evd
-open Environ
-open Proof_type
-(*i*)
-
-(* This module declares readable constraints, and a few utilities on
-   constraints and proof trees *)
-
-val mk_goal : named_context_val -> constr -> Dyn.t option -> goal
-
-val rule_of_proof     : proof_tree -> rule
-val ref_of_proof      : proof_tree -> (rule * proof_tree list)
-val children_of_proof : proof_tree -> proof_tree list
-val goal_of_proof     : proof_tree -> goal
-val subproof_of_proof : proof_tree -> proof_tree
-val status_of_proof   : proof_tree -> int
-val is_complete_proof : proof_tree -> bool
-val is_leaf_proof     : proof_tree -> bool
-val is_tactic_proof   : proof_tree -> bool
-
-val pf_lookup_name_as_displayed  : env -> constr -> identifier -> int option
-val pf_lookup_index_as_renamed : env -> constr -> int -> int option
-
-val is_proof_instr : rule -> bool
-val is_focussing_command : rule -> bool
-
-(*s Pretty printing functions. *)
-
-(*i*)
-open Pp
-(*i*)
-
-val db_pr_goal : goal -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index bc2953408..2fffa3952 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -16,7 +16,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
-open Decl_expr
+(* open Decl_expr *)
 open Rawterm
 open Genarg
 open Nametab
@@ -26,6 +26,10 @@ open Pattern
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
+type goal = Goal.goal
+
+type tactic = goal sigma -> goal list sigma 
+
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
@@ -54,13 +58,6 @@ and rule =
 
 and compound_rule=
   | Tactic of tactic_expr * bool
-  | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
-
-and goal = evar_info
-
-and tactic = goal sigma -> (goal list sigma * validation)
-
-and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b5c4a234d..9692f19bc 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -16,7 +16,6 @@ open Libnames
 open Term
 open Util
 open Tacexpr
-open Decl_expr
 open Rawterm
 open Genarg
 open Nametab
@@ -26,6 +25,10 @@ open Pattern
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
 
+type goal = Goal.goal
+
+type tactic = goal sigma -> goal list sigma
+
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
@@ -89,13 +92,6 @@ and rule =
 and compound_rule=
   (* the boolean of Tactic tells if the default tactic is used *)
   | Tactic of tactic_expr * bool
-  | Proof_instr of bool * proof_instr
-
-and goal = evar_info
-
-and tactic = goal sigma -> (goal list sigma * validation)
-
-and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 05b86b1a0..66001e77a 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,12 +1,15 @@
+Goal
+Evar_refiner
+Proofview
+Proof
+Proof_global
 Tacexpr
 Proof_type
 Redexpr
-Proof_trees
 Logic
 Refiner
-Evar_refiner
 Tacmach
 Pfedit
 Tactic_debug
+Clenv
 Clenvtac
-Decl_mode
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
new file mode 100644
index 000000000..a08941df0
--- /dev/null
+++ b/proofs/proofview.ml
@@ -0,0 +1,491 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* The proofview datastructure is a pure datastructure underlying the notion
+   of proof (namely, a proof is a proofview which can evolve and has safety
+   mechanisms attached).
+   The general idea of the structure is that it is composed of a chemical
+   solution: an unstructured bag of stuff which has some relations with 
+   one another, which represents the various subnodes of the proof, together
+   with a comb: a datastructure that gives order to some of these nodes, 
+   namely the open goals. 
+   The natural candidate for the solution is an {!Evd.evar_map}, that is
+   a calculus of evars. The comb is then a list of goals (evars wrapped 
+   with some extra information, like possible name anotations).
+   There is also need of a list of the evars which initialised the proofview
+   to be able to return information about the proofview. *)
+
+(* Type of proofviews. *)
+type proofview = {
+     initial : (Term.constr * Term.types) list;
+     solution : Evd.evar_map;
+     comb : Goal.goal list
+     }
+
+(* Initialises a proofview, the argument is a list of environement, 
+   conclusion types, and optional names, creating that many initial goals. *)
+let init = 
+  let rec aux = function
+  | [] ->  { initial = [] ; 
+	     solution = Evd.empty ;
+	     comb = []
+	   }
+  | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
+                           aux l
+                         in
+                         let ( new_defs , econstr ) = 
+			   Evarutil.new_evar sol env typ
+			 in
+			 let (e,_) = Term.destEvar econstr in
+			 let gl = Goal.build e in
+			 { initial = (econstr,typ)::ret;
+			   solution = new_defs ;
+			   comb = gl::comb }
+  in
+  fun l -> let v = aux l in
+    (* Marks all the goal unresolvable for typeclasses. *)
+    { v with solution = Typeclasses.mark_unresolvables v.solution }
+
+(* Returns whether this proofview is finished or not. That is,
+   if it has empty subgoals in the comb. There could still be unsolved
+   subgoaled, but they would then be out of the view, focused out. *)
+let finished = function
+  | {comb = []} -> true
+  | _  -> false
+
+(* Returns the current value of the proofview partial proofs. *)
+let return { initial=init; solution=defs }  =
+  List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init
+
+(* spiwack: this function should probably go in the Util section,
+    but I'd rather have Util (or a separate module for lists)
+    raise proper exceptions before *)
+(* [IndexOutOfRange] occurs in case of malformed indices
+   with respect to list lengths. *)
+exception IndexOutOfRange
+
+(* [list_goto i l] returns a pair of lists [c,t] where
+   [c] has length [i] and is the reversed of the [i] first
+   elements of [l], and [t] is the rest of the list.
+   The idea is to navigate through the list, [c] is then
+   seen as the context of the current position. 
+   Raises [IndexOutOfRange] if [i > length l]*)
+let list_goto = 
+  let rec aux acc index = function
+    | l when index = 0-> (acc,l)
+    | [] -> raise IndexOutOfRange
+    | a::q -> aux (a::acc) (index-1) q
+  in
+  fun i l ->
+    if i < 0 then
+      raise IndexOutOfRange
+    else
+      aux [] i l
+
+(* Type of the object which allow to unfocus a view.*)
+(* First component is a reverse list of what comes before
+   and second component is what goes after (in the expected
+   order) *)
+type focus_context = Goal.goal list * Goal.goal list
+
+(* This (internal) function extracts a sublist between two indices, and
+   returns this sublist together with its context:
+   if it returns [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the
+   original list.
+   The focused list has lenght [j-i-1] and contains the goals from
+   number [i] to number [j] (both included) the first goal of the list
+   being numbered [1].
+   [focus_sublist i j l] raises [IndexOutOfRange] if
+   [i > length l], or [j > length l] or [ j < i ].  *)
+let focus_sublist i j l =
+  let (left,sub_right) = list_goto (i-1) l in
+  let (sub, right) = 
+    try 
+      Util.list_chop (j-i+1) sub_right 
+    with Failure "list_chop" -> 
+      Util.errorlabstrm "nth_unproven" (Pp.str"Not such unproven subgoal")
+  in
+  (sub, (left,right))
+
+(* Inverse operation to the previous one. *)
+let unfocus_sublist (left,right) s =
+  List.rev_append left (s@right)
+
+
+(* [focus i j] focuses a proofview on the goals from index [i] to index [j] 
+   (inclusive). (i.e. goals number [i] to [j] become the only goals of the
+   returned proofview).
+   It returns the focus proof, and a context for the focus trace. *)
+let focus i j sp =
+  let (new_comb, context) = focus_sublist i j sp.comb in
+  ( { sp with comb = new_comb } , context )
+
+(* Unfocuses a proofview with respect to a context. *)
+let undefined defs l =
+  Option.List.flatten (List.map (Goal.advance defs) l)
+let unfocus c sp =
+  { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
+
+
+(* The tactic monad:
+   - Tactics are objects which apply a transformation to all
+     the subgoals of the current view at the same time. By opposed
+     to the old vision of applying it to a single goal. It mostly 
+     allows to consider tactic like [reorder] to reorder the goals
+     in the current view (which might be useful for the tactic designer)
+     (* spiwack: the ordering of goals, though, is perhaps a bit
+        brittle. It would be much more interesting to find a more
+        robust way to adress goals, I have no idea at this time 
+        though*) 
+     or global automation tactic for dependent subgoals (instantiating
+     an evar has influences on the other goals of the proof in progress,
+     not being able to take that into account causes the current eauto
+     tactic to fail on some instances where it could succeed).
+   - Tactics are a monad ['a tactic], in a sense a tactic can be 
+     seens as a function (without argument) which returns a value
+     of type 'a and modifies the environement (in our case: the view).
+     Tactics of course have arguments, but these are given at the 
+     meta-level as OCaml functions.
+     Most tactics, in the sense we are used to, return [ () ], that is
+     no really interesting values. But some might pass information 
+     around; the [(>>--)] and [(>>==)] bind-like construction are the
+     main ingredients of this information passing. 
+     (* spiwack: I don't know how much all this relates to F. Kirchner and 
+        C. Muñoz. I wasn't able to understand how they used the monad
+        structure in there developpement.
+     *)
+     The tactics seen in Coq's Ltac are (for now at least) only 
+     [unit tactic], the return values are kept for the OCaml toolkit.
+     The operation or the monad are [Proofview.tclUNIT] (which is the 
+     "return" of the tactic monad) [Proofview.tclBIND] (which is
+     the "bind", also noted [(>=)]) and [Proofview.tclTHEN] (which is a
+     specialized bind on unit-returning tactics).
+*)
+
+(* type of tactics *)
+(* spiwack: double-continuation backtracking monads are reasonable
+    folklore for "search" implementations (including Tac interactive prover's
+    tactics). Yet it's quite hard to wrap your head around these.
+    I recommand reading a few times the "Backtracking, Interleaving, and Terminating
+    Monad Transformers" paper by O. Kiselyov, C. Chen, D. Fridman.  
+    The peculiar shape of the monadic type is reminiscent of that of the continuation
+    monad transformer.
+    A good way to get a feel of what's happening is to look at what happens when
+    executing [apply (tclUNIT ())]. 
+    The disjunction function is unlike that of the LogicT paper, because we want and 
+    need to backtrack over state as well as values. Therefore we cannot be
+    polymorphic over the inner monad. *)
+type proof_step = { goals : Goal.goal list ; defs : Evd.evar_map }
+type +'a result = { proof_step : proof_step ;
+		                content : 'a }
+
+(* nb=non-backtracking *)
+type +'a nb_tactic  = proof_step -> 'a result
+
+(* double-continutation backtracking *)
+(* "sk" stands for "success continuation", "fk" for "failure continuation" *)
+type 'r fk = exn -> 'r
+type (-'a,'r) sk = 'a -> 'r fk -> 'r
+type +'a tactic0 = { go : 'r. ('a, 'r nb_tactic) sk -> 'r nb_tactic fk -> 'r nb_tactic }
+
+(* We obtain a tactic by parametrizing with an environment *)
+(* spiwack: alternatively the environment could be part of the "nb_tactic" state
+    monad. As long as we do not intend to change the environment during a tactic,
+    it's probably better here. *)
+type +'a tactic = Environ.env -> 'a tactic0
+
+(* unit of [nb_tactic] *)
+let nb_tac_unit a step = { proof_step = step ; content = a }
+
+(* Applies a tactic to the current proofview. *)
+let apply env t sp  = 
+  let start = { goals = sp.comb ; defs = sp.solution } in
+  let res = (t env).go (fun a _ step -> nb_tac_unit a step) (fun e _ -> raise e) start in
+  let next = res.proof_step in
+  {sp with
+     solution = next.defs ;
+     comb = next.goals
+  }
+
+(*** tacticals ***)
+
+
+(* Unit of the tactic monad *)
+let tclUNIT a _ = { go = fun sk fk step -> sk a fk step }
+
+(* Bind operation of the tactic monad *)
+let tclBIND t k env = { go = fun sk fk step ->
+  (t env).go (fun a fk -> (k a env).go sk fk) fk step
+}
+
+(* Interpretes the ";" (semicolon) of Ltac.
+   As a monadic operation, it's a specialized "bind"
+   on unit-returning tactic (meaning "there is no value to bind") *)
+let tclTHEN t1 t2 env = { go = fun sk fk step ->
+  (t1 env).go (fun () fk -> (t2 env).go sk fk) fk step
+}
+
+(* [tclIGNORE t] has the same operational content as [t],
+   but drops the value at the end. *)
+let tclIGNORE tac env = { go = fun sk fk step ->
+  (tac env).go (fun _ fk -> sk () fk) fk step
+}
+
+(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t1 fails. 
+    No interleaving for the moment. *)
+(* spiwack: compared to the LogicT paper, we backtrack at the same state
+    where [t1] has been called, not the state where [t1] failed. *)
+let tclOR t1 t2 env = { go = fun sk fk step ->
+  (t1 env).go sk (fun _ _ -> (t2 env).go sk fk step) step
+}
+
+(* [tclZERO e] always fails with error message [e]*)
+let tclZERO e env = { go = fun _ fk step -> fk e step }
+
+
+(* Focusing operation on proof_steps. *)
+let focus_proof_step i j ps =
+  let (new_subgoals, context) = focus_sublist i j ps.goals in
+  ( { ps with goals = new_subgoals } , context )
+
+(* Unfocusing operation of proof_steps. *)
+let unfocus_proof_step c ps =
+  { ps with 
+     goals = undefined ps.defs (unfocus_sublist c ps.goals) 
+  }
+
+(* Focuses a tactic at a range of subgoals, found by their indices. *)
+(* arnaud: bug if 0 goals ! *)
+let tclFOCUS i j t env = { go = fun sk fk step ->
+  let (focused,context) = focus_proof_step i j step in
+  (t env).go (fun a fk step -> sk a fk (unfocus_proof_step context step)) fk focused
+}
+
+(* Dispatch tacticals are used to apply a different tactic to each goal under
+    consideration. They come in two flavours:
+    [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
+    [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
+    and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
+    corresponds to that of the tactic which created [g].
+    It is to be noted that the return value of [tclDISPATCHS ts] makes only
+    sense in the goals immediatly built by it, and would cause an anomaly
+    is used otherwise. *)
+exception SizeMismatch
+(* spiwack: we use an parametrised function to generate the dispatch tacticals.
+    [tclDISPATCHGEN] takes a [null] argument to generate the return value
+    if there are no goal under focus, and a [join] argument to explain how
+    the return value at two given lists of subgoals are combined when
+    both lists are being concatenated.
+    [join] and [null] need be some sort of comutative monoid. *)
+let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
+  match tacs,step.goals with
+  | [] , [] -> (tclUNIT null env).go sk fk step
+  | t::tacs , first::goals -> 
+      (tclDISPATCHGEN null join tacs env).go
+	begin fun x fk step -> 
+	  match Goal.advance step.defs first with
+	  | None -> sk x fk step
+	  | Some first ->
+	    (t env).go 
+	      begin fun y fk step' -> 
+		sk (join x y) fk { step' with 
+			                   goals = step'.goals@step.goals
+				         }
+	      end 
+	      fk 
+	      { step with goals = [first] }
+	end
+	fk
+	{ step with goals = goals }
+  | _ -> raise SizeMismatch
+}
+
+(* takes a tactic which can raise exception and makes it pure by *failing* 
+    on with these exceptions. Does not catch anomalies. *)
+let purify t = 
+  let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
+     	                                                     with Util.Anomaly _ as e -> raise e
+							           | e -> sk (Util.Inr e) fk step
+	       }
+  in
+  tclBIND t' begin function
+    | Util.Inl x -> tclUNIT x
+    | Util.Inr e -> tclZERO e
+  end
+let tclDISPATCHGEN null join tacs = purify (tclDISPATCHGEN null join tacs)
+
+let unitK () () = ()
+let tclDISPATCH = tclDISPATCHGEN () unitK
+
+let extend_to_list =
+  let rec copy n x l =
+    if n < 0 then raise SizeMismatch
+    else if n = 0 then l
+    else copy (n-1) x (x::l)
+  in
+  fun startxs rx endxs l ->
+    let ns = List.length startxs in
+    let ne = List.length endxs in
+    let n = List.length l in
+    startxs@(copy (n-ne-ns) rx endxs)
+let tclEXTEND tacs1 rtac tacs2 env = { go = fun sk fk step -> 
+  let tacs = extend_to_list tacs1 rtac tacs2 step.goals in
+  (tclDISPATCH tacs env).go sk fk step
+}
+
+(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a
+    [Goal.sensitive] as a first argument, the tactic then acts on each goal separately.
+    Allows backtracking between goals. *)
+let list_of_sensitive s k env step =
+  Goal.list_map begin fun defs g ->
+    let (a,defs) = Goal.eval s env defs g in
+    (k a) , defs
+  end step.goals step.defs
+(* In form of a tactic *)
+let list_of_sensitive s k env = { go = fun sk fk step ->
+  let (tacs,defs) = list_of_sensitive s k env step in
+  sk tacs fk { step with defs = defs } 
+}
+
+(* This is a helper function for the dispatching tactics (like [tclGOALBIND] and
+    [tclDISPATCHS]). It takes an ['a sensitive] value, and returns a tactic
+    whose return value is, again, ['a sensitive] but only has value in the
+    (unmodified) goals under focus. *)
+let here_s b env = { go = fun sk fk step ->
+  sk (Goal.bind (Goal.here_list step.goals b) (fun b -> b)) fk step
+}
+
+let rec tclGOALBIND s k = 
+  (* spiwack: the first line ensures that the value returned by the tactic [k] will
+      not "escape its scope". *)
+  let k a = tclBIND (k a) here_s in
+  purify begin 
+    tclBIND (list_of_sensitive s k) begin fun tacs ->
+      tclDISPATCHGEN Goal.null Goal.plus tacs
+    end 
+  end
+
+(* spiwack: this should probably be moved closer to the [tclDISPATCH] tactical. *)
+let tclDISPATCHS tacs = 
+  let tacs = 
+    List.map begin fun tac -> 
+      tclBIND tac here_s
+    end tacs 
+  in
+  purify begin 
+    tclDISPATCHGEN Goal.null Goal.plus tacs
+  end
+
+let rec tclGOALBINDU s k = 
+  purify begin 
+    tclBIND (list_of_sensitive s k) begin fun tacs ->
+      tclDISPATCHGEN () unitK tacs
+    end
+  end
+
+(* spiwack: up to a few details, same errors are in the Logic module.
+    this should be maintained synchronized, probably. *)
+open Pretype_errors
+let rec catchable_exception = function
+  | Stdpp.Exc_located(_,e) -> catchable_exception e
+  | Util.UserError _ | Type_errors.TypeError _ 
+  | Indrec.RecursionSchemeError _
+  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  (* unification errors *)
+  | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
+		   |CannotFindWellTypedAbstraction _
+		   |UnsolvableImplicit _)) -> true
+  | Typeclasses_errors.TypeClassError 
+      (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
+  | _ -> false
+
+(* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
+    everything is done in one step. *)
+let sensitive_on_step s env step =
+  let wrap g ((defs, partial_list) as partial_res) = 
+    match Goal.advance defs g with
+    | None ->partial_res
+    | Some g ->
+      let {Goal.subgoals = sg } , d' = Goal.eval s env defs g in
+      (d',sg::partial_list)
+  in
+  let ( new_defs , combed_subgoals ) = 
+    List.fold_right wrap step.goals (step.defs,[])
+  in
+  { defs = new_defs;
+     goals = List.flatten combed_subgoals }
+let tclSENSITIVE s =
+  purify begin
+    fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) }
+  end
+
+module Notations = struct
+  let (>-) = Goal.bind
+  let (>>-) = tclGOALBINDU
+  let (>>--) = tclGOALBIND
+  let (>=) = tclBIND
+  let (>>=) t k = t >= fun s -> s >>- k
+  let (>>==) t k = t >= fun s -> s >>-- k
+  let (<*>) = tclTHEN
+  let (<+>) = tclOR
+end
+
+(*** Compatibility layer with <= 8.2 tactics ***)
+module V82 = struct
+  type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+
+  let tactic tac _ = { go = fun sk fk ps ->
+    (* spiwack: we ignore the dependencies between goals here, expectingly
+         preserving the semantics of <= 8.2 tactics *)
+    let tac evd gl = 
+      let glsigma  = tac { Evd.it = gl ; Evd.sigma = evd }  in
+      let sigma = glsigma.Evd.sigma in
+      let g = glsigma.Evd.it in
+      ( g , sigma )
+    in
+    (* Old style tactics expect the goals normalized with respect to evars. *)
+    let (initgoals,initevd) = 
+      Goal.list_map Goal.V82.nf_evar ps.goals ps.defs
+    in
+    let (goalss,evd) = Goal.list_map tac initgoals initevd in
+    let sgs = List.flatten goalss in
+    sk () fk { defs = evd ; goals = sgs }
+}
+
+  let has_unresolved_evar pv =
+    let evd = pv.solution in
+    (* arnaud: essayer une procédure moins coûteuse *)
+    not ((Evarutil.non_instantiated evd) = [])
+
+  (* Returns the open goals of the proofview together with the evar_map to 
+     interprete them. *)
+  let goals { comb = comb ; solution = solution } = 
+    { Evd.it = comb ; sigma = solution}
+
+  let top_goals { initial=initial ; solution=solution } = 
+    let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
+    { Evd.it = goals ; sigma=solution }
+
+  let instantiate_evar n com pv =
+    let (evk,_) = 
+      let evl = Evarutil.non_instantiated pv.solution in
+     if (n <= 0) then
+	Util.error "incorrect existential variable index"
+      else if List.length evl < n then
+	  Util.error "not so many uninstantiated existential variables"
+      else
+	List.nth evl (n-1) 
+    in
+    { pv with
+	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
+
+  let purify = purify
+end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
new file mode 100644
index 000000000..cd5520d4e
--- /dev/null
+++ b/proofs/proofview.mli
@@ -0,0 +1,203 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: proofview.mli aspiwack $ *)
+
+(* The proofview datastructure is a pure datastructure underlying the notion
+   of proof (namely, a proof is a proofview which can evolve and has safety
+   mechanisms attached).
+   The general idea of the structure is that it is composed of a chemical
+   solution: an unstructured bag of stuff which has some relations with 
+   one another, which represents the various subnodes of the proof, together
+   with a comb: a datastructure that gives order to some of these nodes, 
+   namely the open goals. 
+   The natural candidate for the solution is an {!Evd.evar_map}, that is
+   a calculus of evars. The comb is then a list of goals (evars wrapped 
+   with some extra information, like possible name anotations).
+   There is also need of a list of the evars which initialised the proofview
+   to be able to return information about the proofview. *)
+
+open Term
+
+type proofview 
+
+(* Initialises a proofview, the argument is a list of environement, 
+   conclusion types, creating that many initial goals. *)
+val init : (Environ.env * Term.types) list -> proofview
+
+(* Returns whether this proofview is finished or not.That is,
+   if it has empty subgoals in the comb. There could still be unsolved
+   subgoaled, but they would then be out of the view, focused out. *)
+val finished : proofview -> bool
+
+(* Returns the current value of the proofview partial proofs. *)
+val return : proofview -> (constr*types) list
+
+
+(*** Focusing operations ***)
+
+(* [IndexOutOfRange] occurs in case of malformed indices
+   with respect to list lengths. *)
+exception IndexOutOfRange
+
+(* Type of the object which allow to unfocus a view.*)
+type focus_context
+
+(* [focus i j] focuses a proofview on the goals from index [i] to index [j] 
+   (inclusive). (i.e. goals number [i] to [j] become the only goals of the
+   returned proofview).
+   It returns the focus proof, and a context for the focus trace. *)
+val focus : int -> int -> proofview -> proofview * focus_context
+
+(* Unfocuses a proofview with respect to a context. *)
+val unfocus : focus_context -> proofview -> proofview
+
+(* The tactic monad:
+   - Tactics are objects which apply a transformation to all
+     the subgoals of the current view at the same time. By opposed
+     to the old vision of applying it to a single goal. It mostly 
+     allows to consider tactic like [reorder] to reorder the goals
+     in the current view (which might be useful for the tactic designer)
+     (* spiwack: the ordering of goals, though, is actually rather
+        brittle. It would be much more interesting to find a more
+        robust way to adress goals, I have no idea at this time 
+        though*) 
+     or global automation tactic for dependent subgoals (instantiating
+     an evar has influences on the other goals of the proof in progress,
+     not being able to take that into account causes the current eauto
+     tactic to fail on some instances where it could succeed).
+   - Tactics are a monad ['a tactic], in a sense a tactic can be 
+     seens as a function (without argument) which returns a value
+     of type 'a and modifies the environement (in our case: the view).
+     Tactics of course have arguments, but these are given at the 
+     meta-level as OCaml functions.
+     Most tactics in the sense we are used to return [ () ], that is
+     no really interesting values. But some might, to pass information 
+     around; for instance [Proofview.freeze] allows to store a certain
+     goal sensitive value "at the present time" (which means, considering the
+     structure of the dynamics of proofs, [Proofview.freeze s] will have,
+     for every current goal [gl], and for any of its descendent [g'] in 
+     the future the same value in [g'] that in [gl]). 
+     (* spiwack: I don't know how much all this relates to F. Kirchner and 
+        C. Muñoz. I wasn't able to understand how they used the monad
+        structure in there developpement.
+     *)
+     The tactics seen in Coq's Ltac are (for now at least) only 
+     [unit tactic], the return values are kept for the OCaml toolkit.
+     The operation or the monad are [Proofview.tclIDTAC] (which is the 
+     "return" of the tactic monad) [Proofview.tclBIND] (which is
+     the "bind") and [Proofview.tclTHEN] (which is a specialized
+     bind on unit-returning tactics).
+*)
+
+
+type +'a tactic 
+
+(* Applies a tactic to the current proofview. *)
+val apply : Environ.env -> 'a tactic -> proofview -> proofview
+
+(*** tacticals ***)
+
+(* Unit of the tactic monad *)
+val tclUNIT : 'a -> 'a tactic
+
+(* Bind operation of the tactic monad *)
+val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
+(* Interpetes the ";" (semicolon) of Ltac.
+   As a monadic operation, it's a specialized "bind"
+   on unit-returning tactic (meaning "there is no value to bind") *)
+val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
+
+(* [tclIGNORE t] has the same operational content as [t],
+   but drops the value at the end. *)
+val tclIGNORE : 'a tactic -> unit tactic
+
+(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t2 fails. 
+    No interleaving at this point. *)
+val tclOR : 'a tactic -> 'a tactic -> 'a tactic
+
+(* [tclZERO] always fails *)
+val tclZERO : exn -> 'a tactic
+
+(* Focuses a tactic at a range of subgoals, found by their indices. *)
+val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
+
+(* Dispatch tacticals are used to apply a different tactic to each goal under
+    consideration. They come in two flavours:
+    [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
+    [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
+    and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
+    corresponds to that of the tactic which created [g].
+    It is to be noted that the return value of [tclDISPATCHS ts] makes only
+    sense in the goals immediatly built by it, and would cause an anomaly
+    is used otherwise. *)
+val tclDISPATCH : unit tactic list -> unit tactic
+val tclDISPATCHS : 'a Goal.sensitive tactic list -> 'a Goal.sensitive tactic
+
+(* [tclEXTEND b r e] is a variant to [tclDISPATCH], where the [r] tactic
+    is "repeated" enough time such that every goal has a tactic assigned to it
+    ([b] is the list of tactics applied to the first goals, [e] to the last goals, and [r]
+    is applied to every goal in between. *)
+val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
+
+(* A sort of bind which takes a [Goal.sensitive] as a first argument, 
+    the tactic then acts on each goal separately.
+    Allows backtracking between goals. *)
+val tclGOALBIND : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
+
+(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
+val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic 
+
+(* Notations for building tactics. *)
+module Notations : sig
+  (* Goal.bind *)
+  val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
+  (* tclGOALBINDU *)
+  val (>>-) : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
+  (* tclGOALBIND *)
+  val (>>--) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+
+  (* tclBIND *)
+  val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
+  (* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
+      tactic monad and the goal-sensitive monad.
+      It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
+      needs a bind, since it usually avoids to delay the interpretation of the
+      goal sensitive value to a location where it does not make sense anymore. *)
+  val (>>=) : 'a Goal.sensitive tactic -> ('a -> unit tactic) -> unit tactic
+  val (>>==) : 'a Goal.sensitive tactic -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+
+  (* tclTHEN *)
+  val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+  (* tclOR *)
+  val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
+end
+
+(*** Compatibility layer with <= 8.2 tactics ***)
+module V82 : sig
+  type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma 
+  val tactic : tac -> unit tactic
+
+  val has_unresolved_evar : proofview -> bool
+
+  (* Returns the open goals of the proofview together with the evar_map to 
+     interprete them. *)
+  val goals : proofview -> Goal.goal list Evd.sigma
+
+  val top_goals : proofview -> Goal.goal list Evd.sigma
+    
+  (* Implements the Existential command *)
+  val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview
+
+  (* spiwack: [purify] might be useful while writing tactics manipulating exception 
+     explicitely or from the [V82] submodule (neither being advised, though *)
+  val purify : 'a tactic -> 'a tactic
+end
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a320b67cd..ffb18f265 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -18,53 +18,20 @@ open Sign
 open Environ
 open Reductionops
 open Type_errors
-open Proof_trees
 open Proof_type
 open Logic
 
-type transformation_tactic = proof_tree -> (goal list * validation)
-
-let hypotheses gl = gl.evar_hyps
-let conclusion gl = gl.evar_concl
 
 let sig_it x = x.it
 let project x = x.sigma
 
-let pf_status pf = pf.open_subgoals
-
-let is_complete pf = (0 = (pf_status pf))
-
-let on_open_proofs f pf = if is_complete pf then pf else f pf
 
 let and_status = List.fold_left (+) 0
 
 (* Getting env *)
 
-let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
-let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
-
-
-let descend n p =
-  match p.ref with
-    | None        -> error "It is a leaf."
-    | Some(r,pfl) ->
-    	if List.length pfl >= n then
-	  (match list_chop (n-1) pfl with
-	     | left,(wanted::right) ->
-		 (wanted,
-		  (fun pfl' ->
-		    if false (* debug *) then assert
-		      (List.length pfl'=1 & (List.hd pfl').goal = wanted.goal);
-                    let pf'       = List.hd pfl' in
-                    let spfl      = left@(pf'::right) in
-                    let newstatus = and_status (List.map pf_status spfl) in
-                    { p with
-			open_subgoals = newstatus;
-			ref           = Some(r,spfl) }))
-	     | _ -> assert false)
-    	else
-	  error "Too few subproofs"
-
+let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
+let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
    gives
@@ -80,121 +47,9 @@ let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
 	let m,l = list_chop h l in
 	(List.hd fl m) :: (mapshape t (List.tl fl) l)
 
-(* [frontier : proof_tree -> goal list * validation]
-   given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals
-   to be solved to complete the proof, and [v] is the corresponding
-   validation *)
-
-let rec frontier p =
-  match p.ref with
-    | None ->
-	([p.goal],
-	 (fun lp' ->
-	    let p' = List.hd lp' in
-            if Evd.eq_evar_info p'.goal p.goal then
-	      p'
-            else
-	      errorlabstrm "Refiner.frontier"
-                (str"frontier was handed back a ill-formed proof.")))
-    | Some(r,pfl) ->
-    	let gll,vl = List.split(List.map frontier pfl) in
-    	(List.flatten gll,
-         (fun retpfl ->
-            let pfl' = mapshape (List.map List.length gll) vl retpfl in
-              { p with
-		  open_subgoals = and_status (List.map pf_status pfl');
-		  ref = Some(r,pfl')}))
-
-(* TODO LEM: I might have to make sure that these hooks are called
-   only when called from solve_nth_pftreestate; I can build the hook
-   call into the "f", then.
- *)
-let solve_hook = ref ignore
-let set_solve_hook = (:=) solve_hook
-
-let rec frontier_map_rec f n p =
-  if n < 1 || n > p.open_subgoals then p else
-  match p.ref with
-    | None ->
-        let p' = f p in
-        if Evd.eq_evar_info p'.goal p.goal then
-	  begin
-	    !solve_hook p';
-	    p'
-	  end
-        else
-	  errorlabstrm "Refiner.frontier_map"
-            (str"frontier_map was handed back a ill-formed proof.")
-    | Some(r,pfl) ->
-        let (_,rpfl') =
-          List.fold_left
-            (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
-            (n,[]) pfl in
-        let pfl' = List.rev rpfl' in
-        { p with
-	    open_subgoals = and_status (List.map pf_status pfl');
-            ref = Some(r,pfl')}
-
-let frontier_map f n p =
-  let nmax = p.open_subgoals in
-  let n = if n < 0 then nmax + n + 1 else n in
-  if n < 1 || n > nmax then
-    errorlabstrm "Refiner.frontier_map" (str "No such subgoal");
-  frontier_map_rec f n p
-
-let rec frontier_mapi_rec f i p =
-  if p.open_subgoals = 0 then p else
-  match p.ref with
-    | None ->
-        let p' = f i p in
-        if Evd.eq_evar_info p'.goal p.goal then
-	  begin
-	    !solve_hook p';
-	    p'
-	  end
-        else
-	  errorlabstrm "Refiner.frontier_mapi"
-            (str"frontier_mapi was handed back a ill-formed proof.")
-    | Some(r,pfl) ->
-        let (_,rpfl') =
-          List.fold_left
-            (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
-            (i,[]) pfl in
-        let pfl' = List.rev rpfl' in
-        { p with
-	    open_subgoals = and_status (List.map pf_status pfl');
-            ref = Some(r,pfl')}
-
-let frontier_mapi f p = frontier_mapi_rec f 1 p
-
-(* [list_pf p] is the lists of goals to be solved in order to complete the
-   proof [p] *)
-
-let list_pf p = fst (frontier p)
-
-let rec nb_unsolved_goals pf = pf.open_subgoals
-
-(* leaf g is the canonical incomplete proof of a goal g *)
-
-let leaf g =
-  { open_subgoals = 1;
-    goal = g;
-    ref = None }
-
-(* refiner r is a tactic applying the rule r *)
-
-let check_subproof_connection gl spfl =
-  list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
-
-let abstract_operation syntax semantics gls =
-  let (sgl_sigma,validation) = semantics gls in
-  let hidden_proof = validation (List.map leaf sgl_sigma.it) in
-  (sgl_sigma,
-  fun spfl ->
-    assert (check_subproof_connection sgl_sigma.it spfl);
-    { open_subgoals = and_status (List.map pf_status spfl);
-      goal = gls.it;
-      ref = Some(Nested(syntax,hidden_proof),spfl)})
+
+let abstract_operation syntax semantics =
+  semantics
 
 let abstract_tactic_expr ?(dflt=false) te tacfun gls =
   abstract_operation (Tactic(te,dflt)) tacfun gls
@@ -207,16 +62,11 @@ let abstract_extended_tactic ?(dflt=false) s args =
   abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
 
 let refiner = function
-  | Prim pr as r ->
+  | Prim pr ->
       let prim_fun = prim_refiner pr in
 	(fun goal_sigma ->
           let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
-	    ({it=sgl; sigma = sigma'},
-            (fun spfl ->
-	      assert (check_subproof_connection sgl spfl);
-              { open_subgoals = and_status (List.map pf_status spfl);
-		goal = goal_sigma.it;
-		ref = Some(r,spfl) })))
+	  {it=sgl; sigma = sigma'})
 
 
   | Nested (_,_) | Decl_proof _ ->
@@ -226,83 +76,15 @@ let refiner = function
 
   | Daimon ->
       fun gls ->
-	({it=[];sigma=gls.sigma},
-	 fun spfl ->
-	   assert (spfl=[]);
-	   { open_subgoals = 0;
-             goal = gls.it;
-             ref = Some(Daimon,[])})
+	{it=[];sigma=gls.sigma}
 
 
 let norm_evar_tac gl = refiner (Prim Change_evars) gl
 
-let norm_evar_proof sigma pf =
-  let nf_subgoal i sgl =
-    let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
-      v (List.map leaf gll.it) in
-    frontier_mapi nf_subgoal pf
-
-(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
-   takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
-   where pfterm is the constr corresponding to the proof
-   and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
-   where the mi are metavariables numbers, and ci are their types.
-   Their proof should be completed in order to complete the initial proof *)
-
-let extract_open_proof sigma pf =
-  let next_meta =
-    let meta_cnt = ref 0 in
-    let rec f () =
-      incr meta_cnt;
-      if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
-      else !meta_cnt
-    in f
-  in
-  let open_obligations = ref [] in
-  let rec proof_extractor vl = function
-    | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
-
-    | {ref=Some(Nested(_,hidden_proof),spfl)} ->
-	let sgl,v = frontier hidden_proof in
-	let flat_proof = v spfl in
-	proof_extractor vl flat_proof
-
-    | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
-
-    | {ref=(None|Some(Daimon,[]));goal=goal} ->
-	let visible_rels =
-          map_succeed
-            (fun id ->
-               try let n = proof_variable_index id vl in (n,id)
-	       with Not_found -> failwith "caught")
-            (ids_of_named_context (named_context_of_val goal.evar_hyps)) in
-	let sorted_rels =
-	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
-        let sorted_env =
-          List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps))
-            sorted_rels in
-	let abs_concl =
-          List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
-            sorted_env goal.evar_concl	in
-        let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
-        let meta = next_meta () in
-	open_obligations := (meta,abs_concl):: !open_obligations;
-	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
-
-    | _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
-  in
-  let pfterm = proof_extractor [] pf in
-  (pfterm, List.rev !open_obligations)
-
 (*********************)
 (*   Tacticals       *)
 (*********************)
 
-(* unTAC : tactic -> goal sigma -> proof sigma *)
-
-let unTAC tac g =
-  let (gl_sigma,v) = tac g in
-  { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
 
 let unpackage glsig = (ref (glsig.sigma)),glsig.it
 
@@ -310,13 +92,9 @@ let repackage r v = {it=v;sigma = !r}
 
 let apply_sig_tac r tac g =
   check_for_interrupt (); (* Breakpoint *)
-  let glsigma,v = tac (repackage r g) in
+  let glsigma = tac (repackage r g) in
   r := glsigma.sigma;
-  (glsigma.it,v)
-
-let idtac_valid = function
-    [pf] -> pf
-  | _ -> anomaly "Refiner.idtac_valid"
+  glsigma.it
 
 (* [goal_goal_list : goal sigma -> goal list sigma] *)
 let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
@@ -325,7 +103,7 @@ let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
 let tclNORMEVAR = norm_evar_tac
 
 (* identity tactic without any message *)
-let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
+let tclIDTAC gls = goal_goal_list gls
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls =
@@ -344,23 +122,21 @@ let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =
   let (sigr,g) = unpackage gls in
-  (sigr,[g],idtac_valid)
+  (sigr,[g])
 
-let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
+let finish_tac (sigr,gl) = repackage sigr gl
 
 (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
-let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
+let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let nf = Array.length tacfi in
   let nl = Array.length tacli in
   let ng = List.length gs in
   if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
-  let gll,pl =
-    List.split
+  let gll =
       (list_map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
-  (sigr, List.flatten gll,
-   compose p (mapshape (List.map List.length gll) pl))
+    (sigr,List.flatten gll)
 
 (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
 let thensf_tac taci tac = thens3parts_tac taci tac [||]
@@ -369,10 +145,10 @@ let thensf_tac taci tac = thens3parts_tac taci tac [||]
 let thensl_tac tac taci = thens3parts_tac [||] tac taci
 
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
-let thensi_tac tac (sigr,gs,p) =
-  let gll,pl =
-    List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in
-  (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl))
+let thensi_tac tac (sigr,gs) =
+  let gll =
+    list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
+  (sigr, List.flatten gll)
 
 let then_tac tac = thensf_tac [||] tac
 
@@ -382,7 +158,7 @@ let non_existent_goal n =
 
 (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
    the last goal (i=-1). *)
-let theni_tac i tac ((_,gl,_) as subgoals) =
+let theni_tac i tac ((_,gl) as subgoals) =
   let nsg = List.length gl in
   let k = if i < 0 then nsg + i + 1 else i in
   if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
@@ -451,42 +227,29 @@ let rec tclTHENLIST = function
 let tclMAP tacfun l =
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
-(* various progress criterions *)
-let same_goal gl subgoal =
-  eq_constr (conclusion subgoal) (conclusion gl) &&
-  eq_named_context_val (hypotheses subgoal) (hypotheses gl)
-
-
-let weak_progress gls ptree =
-  (List.length gls.it <> 1) ||
-  (not (same_goal (List.hd gls.it) ptree.it))
-
-let progress gls ptree =
-  (progress_evar_map ptree.sigma gls.sigma) ||
-  (weak_progress gls ptree)
-
+(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
+the goal unchanged *)
+let tclWEAK_PROGRESS tac ptree =
+  let rslt = tac ptree in
+  if Goal.V82.weak_progress rslt ptree then rslt
+  else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
 
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
 let tclPROGRESS tac ptree =
   let rslt = tac ptree in
-  if progress (fst rslt) ptree then rslt
+  if Goal.V82.progress rslt ptree then rslt
   else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
 
-(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails
-   if tac leaves the goal unchanged, possibly modifying sigma *)
-let tclWEAK_PROGRESS tac ptree =
-  let rslt = tac ptree in
-  if weak_progress (fst rslt) ptree then rslt
-  else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.")
-
-
 (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
    one of them being identical to the original goal *)
 let tclNOTSAMEGOAL (tac : tactic) goal =
+  let same_goal gls1 evd2 gl2 =
+    Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
+  in
   let rslt = tac goal in
-  let gls = (fst rslt).it in
-  if List.exists (same_goal goal.it) gls
+  let {it=gls;sigma=sigma} = rslt in
+  if List.exists (same_goal goal sigma) gls
   then errorlabstrm "Refiner.tclNOTSAMEGOAL"
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
@@ -525,9 +288,9 @@ let tclORELSE_THEN t1 t2then t2else gls =
     with e -> catch_failerror e; None
   with
     | None -> t2else gls
-    | Some (sgl,v) ->
+    | Some sgl ->
         let (sigr,gl) = unpackage sgl in
-        finish_tac (then_tac t2then  (sigr,gl,v))
+        finish_tac (then_tac t2then  (sigr,gl))
 
 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
 let tclTRY f = (tclORELSE0 f tclIDTAC)
@@ -601,14 +364,12 @@ let rec tclREPEAT_MAIN t g =
 
 (*s Tactics handling a list of goals. *)
 
-type validation_list = proof_tree list -> proof_tree list
-
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = (goal list sigma) -> (goal list sigma)
 
 (* Functions working on goal list for correct backtracking in Prolog *)
 
 let tclFIRSTLIST = tclFIRST
-let tclIDTAC_list gls = (gls, fun x -> x)
+let tclIDTAC_list gls = gls
 
 (* first_goal : goal list sigma -> goal sigma *)
 
@@ -628,286 +389,20 @@ let apply_tac_list tac glls =
   let (sigr,lg) = unpackage glls in
   match lg with
   | (g1::rest) ->
-      let (gl,p) = apply_sig_tac sigr tac g1 in
-      let n = List.length gl in
-      (repackage sigr (gl@rest),
-       fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
+      let gl = apply_sig_tac sigr tac g1 in
+      repackage sigr (gl@rest)
   | _ -> error "apply_tac_list"
 
 let then_tactic_list tacl1 tacl2 glls =
-  let (glls1,pl1) = tacl1 glls in
-  let (glls2,pl2) = tacl2 glls1 in
-  (glls2, compose pl1 pl2)
+  let glls1 = tacl1 glls in
+  let glls2 = tacl2 glls1 in
+  glls2
 
 (* Transform a tactic_list into a tactic *)
 
 let tactic_list_tactic tac gls =
-    let (glres,vl) = tac (goal_goal_list gls) in
-    (glres, compose idtac_valid vl)
-
-
-
-(* The type of proof-trees state and a few utilities
-   A proof-tree state is built from a proof-tree, a set of global
-   constraints, and a stack which allows to navigate inside the
-   proof-tree remembering how to rebuild the global proof-tree
-   possibly after modification of one of the focused children proof-tree.
-   The number in the stack corresponds to
-   either the selected subtree and the validation is a function from a
-   proof-tree list consisting only of one proof-tree to the global
-   proof-tree
-   or -1 when the move is done behind a registered tactic in which
-   case the validation corresponds to a constant function giving back
-   the original proof-tree. *)
-
-type pftreestate = {
-  tpf      : proof_tree ;
-  tpfsigma : evar_map;
-  tstack   : (int * validation) list }
-
-let proof_of_pftreestate pts = pts.tpf
-let is_top_pftreestate pts = pts.tstack = []
-let cursor_of_pftreestate pts = List.map fst pts.tstack
-let evc_of_pftreestate pts = pts.tpfsigma
-
-let top_goal_of_pftreestate pts =
-  { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
-
-let nth_goal_of_pftreestate n pts =
-  let goals = fst (frontier pts.tpf) in
-  try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
-  with Invalid_argument _ | Failure _ -> non_existent_goal n
-
-let traverse n pts = match n with
-  | 0 -> (* go to the parent *)
-      (match  pts.tstack with
-	 | [] -> error "traverse: no ancestors"
-	 | (_,v)::tl ->
-             let pf = v [pts.tpf] in
-             let pf = norm_evar_proof pts.tpfsigma pf in
-	     { tpf = pf;
-	       tstack = tl;
-	       tpfsigma = pts.tpfsigma })
-  | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
-      (match pts.tpf.ref with
-	 | Some (Nested (_,spf),_) ->
-	     let v = (fun pfl -> pts.tpf) in
-	     { tpf = spf;
-               tstack = (-1,v)::pts.tstack;
-               tpfsigma = pts.tpfsigma }
-	 | _ -> error "traverse: not a tactic-node")
-  | n -> (* when n>0, go to the nth child *)
-      let (npf,v) = descend n pts.tpf in
-      { tpf = npf;
-        tpfsigma = pts.tpfsigma;
-        tstack = (n,v):: pts.tstack }
-
-let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc }
-
-let app_tac sigr tac p =
-  let (gll,v) = tac {it=p.goal;sigma= !sigr} in
-  sigr := gll.sigma;
-  v (List.map leaf gll.it)
-
-(* modify proof state at current position *)
-
-let map_pftreestate f pts =
-  let sigr = ref pts.tpfsigma in
-  let tpf' = f sigr pts.tpf in
-  let tpf'' =
-    if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in
-  { tpf      = tpf'';
-    tpfsigma = !sigr;
-    tstack   = pts.tstack }
-
-(* solve the nth subgoal with tactic tac *)
-
-let solve_nth_pftreestate n tac =
-  map_pftreestate
-    (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
-
-let solve_pftreestate = solve_nth_pftreestate 1
-
-(* This function implements a poor man's undo at the current goal.
-   This is a gross approximation as it does not attempt to clean correctly
-   the global constraints given in tpfsigma. *)
-
-let weak_undo_pftreestate pts =
-  let pf = leaf pts.tpf.goal in
-  { tpf = pf;
-    tpfsigma = pts.tpfsigma;
-    tstack = pts.tstack }
-
-(* Gives a new proof (a leaf) of a goal gl *)
-let mk_pftreestate g =
-  { tpf      = leaf g;
-    tstack   = [];
-    tpfsigma = Evd.empty }
-
-(* Extracts a constr from a proof-tree state ; raises an error if the
-   proof is not complete or the state does not correspond to the head
-   of the proof-tree *)
-
-let extract_open_pftreestate pts =
-  extract_open_proof pts.tpfsigma pts.tpf
-
-let extract_pftreestate pts =
-  if pts.tstack <> [] then
-    errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed");
-  let pfterm,subgoals = extract_open_pftreestate pts in
-  let exl = Evarutil.non_instantiated pts.tpfsigma in
-  if subgoals <> [] or exl <> [] then
-    errorlabstrm "extract_proof"
-      (if subgoals <> [] then
-        str "Attempt to save an incomplete proof"
-      else
-        str "Attempt to save a proof with existential variables still non-instantiated");
-  let env = Global.env_of_context pts.tpf.goal.evar_hyps in
-  nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
-  (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
-  (***
-  local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
-  ***)
-(* Focus on the first leaf proof in a proof-tree state *)
-
-let rec first_unproven pts =
-  let pf = (proof_of_pftreestate pts) in
-  if is_complete_proof pf then
-    errorlabstrm "first_unproven" (str"No unproven subgoals");
-  if is_leaf_proof pf then
-    pts
-  else
-    let childnum =
-      list_try_find_i
-	(fun n pf ->
-	   if not(is_complete_proof pf) then n else failwith "caught")
-	1 (children_of_proof pf)
-    in
-    first_unproven (traverse childnum pts)
-
-(* Focus on the last leaf proof in a proof-tree state *)
-
-let rec last_unproven pts =
-  let pf = proof_of_pftreestate pts in
-  if is_complete_proof pf then
-    errorlabstrm "last_unproven" (str"No unproven subgoals");
-  if is_leaf_proof pf then
-    pts
-  else
-    let children = (children_of_proof pf) in
-    let nchilds = List.length children in
-    let childnum =
-      list_try_find_i
-        (fun n pf ->
-           if not(is_complete_proof pf) then n else failwith "caught")
-        1 (List.rev children)
-    in
-    last_unproven (traverse (nchilds-childnum+1) pts)
-
-let rec nth_unproven n pts =
-  let pf = proof_of_pftreestate pts in
-  if is_complete_proof pf then
-    errorlabstrm "nth_unproven" (str"No unproven subgoals");
-  if is_leaf_proof pf then
-    if n = 1 then
-      pts
-    else
-      errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
-  else
-    let children = children_of_proof pf in
-    let rec process i k = function
-      | [] ->
-	  errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
-      | pf1::rest ->
-	  let k1 = nb_unsolved_goals pf1 in
-	  if k1 < k then
-	    process (i+1) (k-k1) rest
-	  else
-	    nth_unproven k (traverse i pts)
-    in
-    process 1 n children
-
-let rec node_prev_unproven loc pts =
-  let pf = proof_of_pftreestate pts in
-  match cursor_of_pftreestate pts with
-    | [] -> last_unproven pts
-    | n::l ->
-	if is_complete_proof pf or loc = 1 then
-          node_prev_unproven n (traverse 0 pts)
-	else
-	  let child = List.nth (children_of_proof pf) (loc - 2) in
-	  if is_complete_proof child then
-	    node_prev_unproven (loc - 1) pts
-	  else
-	    first_unproven (traverse (loc - 1) pts)
-
-let rec node_next_unproven loc pts =
-  let pf = proof_of_pftreestate pts in
-  match cursor_of_pftreestate pts with
-    | [] -> first_unproven pts
-    | n::l ->
-	if is_complete_proof pf ||
-           loc = (List.length (children_of_proof pf)) then
-             node_next_unproven n (traverse 0 pts)
-	else if is_complete_proof (List.nth (children_of_proof pf) loc) then
-	  node_next_unproven (loc + 1) pts
-	else
-	  last_unproven(traverse (loc + 1) pts)
-
-let next_unproven pts =
-  let pf = proof_of_pftreestate pts in
-  if is_leaf_proof pf then
-    match cursor_of_pftreestate pts with
-      | [] -> error "next_unproven"
-      | n::_ -> node_next_unproven n (traverse 0 pts)
-  else
-    node_next_unproven (List.length (children_of_proof pf)) pts
-
-let prev_unproven pts =
-  let pf = proof_of_pftreestate pts in
-  if is_leaf_proof pf then
-    match cursor_of_pftreestate pts with
-      | [] -> error "prev_unproven"
-      | n::_ -> node_prev_unproven n (traverse 0 pts)
-  else
-    node_prev_unproven 1 pts
-
-let rec top_of_tree pts =
-  if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
-
-(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
-let change_rule f pts =
-  let mark_top _ pt =
-    match pt.ref with
-	Some (oldrule,l) ->
-	  {pt with ref=Some (f oldrule,l)}
-      | _ -> invalid_arg "change_rule" in
-    map_pftreestate mark_top pts
-
-let match_rule p pts =
-  match (proof_of_pftreestate pts).ref with
-      Some (r,_) -> p r
-    | None -> false
-
-let rec up_until_matching_rule p pts =
-  if is_top_pftreestate pts then
-    raise Not_found
-  else
-    let one_up = traverse 0 pts in
-      if match_rule p one_up then
-	pts
-      else
-	up_until_matching_rule p one_up
-
-let rec up_to_matching_rule p pts =
-  if match_rule p pts then
-    pts
-  else
-    if is_top_pftreestate pts then
-      raise Not_found
-    else
-      let one_up = traverse 0 pts in
-      	up_to_matching_rule p one_up
+    let glres = tac (goal_goal_list gls) in
+    glres
 
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
@@ -918,28 +413,8 @@ let pp_info = ref (fun _ _ _ -> assert false)
 let set_info_printer f = pp_info := f
 
 let tclINFO (tac : tactic) gls =
-  let (sgl,v) as res = tac gls in
-  begin try
-    let pf = v (List.map leaf (sig_it sgl)) in
-    let sign = named_context_of_val (sig_it gls).evar_hyps in
-    msgnl (hov 0 (str" == " ++
-                  !pp_info (project gls) sign pf))
-  with e when catchable_exception e ->
-    msgnl (hov 0 (str "Info failed to apply validation"))
-  end;
-  res
-
-let pp_proof = ref (fun _ _ _ -> assert false)
-let set_proof_printer f = pp_proof := f
-
-let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } =
-  (if stack = []
-   then str "Rooted proof tree is:"
-   else (str "Proof tree at occurrence [" ++
-         prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n)
-           (List.rev stack) ++ str "] is:")) ++ fnl() ++
-  !pp_proof sigma (Global.named_context()) pf ++
-  Evd.pr_evar_map sigma
+  msgnl (hov 0 (str "Warning: info is currently not working"));
+  tac gls
 
 (* Check that holes in arguments have been resolved *)
 
@@ -962,5 +437,5 @@ let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
   else
     let res = tclTHEN (tclEVARS sigma) (tac c) gl in
     if not accept_unresolved_holes then
-      check_evars (pf_env gl) (fst res).sigma sigma gl;
+      check_evars (pf_env gl) (res).sigma sigma gl;
     res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index e853c12b7..77f2e48a7 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -12,9 +12,9 @@
 open Term
 open Sign
 open Evd
-open Proof_trees
 open Proof_type
 open Tacexpr
+open Logic
 (*i*)
 
 (* The refiner (handles primitive rules and high-level tactics). *)
@@ -28,14 +28,14 @@ val pf_hyps : goal sigma -> named_context
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
-  evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
-
-type transformation_tactic = proof_tree -> (goal list * validation)
+  evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
 
 (*s Hiding the implementation of tactics. *)
 
 (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
    a single proof node. The boolean tells if the default tactic is used. *)
+(* spiwack: currently here for compatibility, abstract_operation 
+    is a second projection *)
 val abstract_operation : compound_rule -> tactic -> tactic
 val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
 val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
@@ -43,22 +43,6 @@ val abstract_extended_tactic :
   ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
-val frontier : transformation_tactic
-val list_pf : proof_tree -> goal list
-val unTAC : tactic -> goal sigma -> proof_tree sigma
-
-
-(* Install a hook frontier_map and frontier_mapi call on the new node they create *)
-val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit
-(* [frontier_map f n p] applies f on the n-th open subgoal of p and
-   rebuilds proof-tree.
-   n=1 for first goal, n negative counts from the right *)
-val frontier_map :
-  (proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree
-
-(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *)
-val frontier_mapi :
-  (int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree
 
 (*s Tacticals. *)
 
@@ -153,8 +137,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
+val tclPROGRESS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 val tclINFO          : tactic -> tactic
 
@@ -173,9 +157,7 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
 (*s Tactics handling a list of goals. *)
 
-type validation_list = proof_tree list -> proof_tree list
-
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = goal list sigma -> goal list sigma
 
 val tclFIRSTLIST       : tactic_list list -> tactic_list
 val tclIDTAC_list      : tactic_list
@@ -191,57 +173,4 @@ val goal_goal_list     : 'a sigma -> 'a list sigma
    extension of the sigma of the goal *)
 val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic
 
-(*s Functions for handling the state of the proof editor. *)
-
-type pftreestate
-
-val proof_of_pftreestate : pftreestate -> proof_tree
-val cursor_of_pftreestate : pftreestate -> int list
-val is_top_pftreestate : pftreestate -> bool
-val match_rule : (rule -> bool) -> pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> evar_map
-val top_goal_of_pftreestate : pftreestate -> goal sigma
-val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
-
-val traverse : int -> pftreestate -> pftreestate
-val map_pftreestate :
-  (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
-val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
-val solve_pftreestate : tactic -> pftreestate -> pftreestate
-
-(* a weak version of logical undoing, that is really correct only *)
-(* if there are no existential variables.                         *)
-val weak_undo_pftreestate : pftreestate -> pftreestate
-
-val mk_pftreestate : goal -> pftreestate
-val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
-val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
-val extract_pftreestate : pftreestate -> constr
-val first_unproven : pftreestate -> pftreestate
-val last_unproven : pftreestate -> pftreestate
-val nth_unproven : int -> pftreestate -> pftreestate
-val node_prev_unproven : int -> pftreestate -> pftreestate
-val node_next_unproven : int -> pftreestate -> pftreestate
-val next_unproven : pftreestate -> pftreestate
-val prev_unproven : pftreestate -> pftreestate
-val top_of_tree : pftreestate -> pftreestate
-val match_rule : (rule -> bool) -> pftreestate -> bool
-val up_until_matching_rule : (rule -> bool) ->
-  pftreestate -> pftreestate
-val up_to_matching_rule : (rule -> bool) ->
-  pftreestate -> pftreestate
-val change_rule : (rule -> rule) -> pftreestate -> pftreestate
-val change_constraints_pftreestate
-  : evar_map -> pftreestate -> pftreestate
-
-
 (*s Pretty-printers. *)
-
-(*i*)
-open Pp
-(*i*)
-val set_info_printer :
-  (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
-val set_proof_printer :
-  (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
-val print_pftreestate : pftreestate -> Pp.std_ppcmds
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 9e35abfc8..6dbdf17cb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -21,7 +21,6 @@ open Evd
 open Typing
 open Redexpr
 open Tacred
-open Proof_trees
 open Proof_type
 open Logic
 open Refiner
@@ -34,7 +33,6 @@ let re_sig it gc = { it = it; sigma = gc }
 (**************************************************************)
 
 type 'a sigma   = 'a Evd.sigma;;
-type validation = Proof_type.validation;;
 type tactic     = Proof_type.tactic;;
 
 let unpackage = Refiner.unpackage
@@ -46,7 +44,7 @@ let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
 
-let pf_concl gls = (sig_it gls).evar_concl
+let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
   List.map (fun (id,_,x) -> (id, x)) sign
@@ -123,11 +121,11 @@ let pf_matches                  = pf_apply Matching.matches_conv
 (* Tactics handling a list of goals *)
 (************************************)
 
-type transformation_tactic = proof_tree -> (goal list * validation)
+type transformation_tactic = proof_tree -> goal list 
 
 type validation_list = proof_tree list -> proof_tree list
 
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = Refiner.tactic_list 
 
 let first_goal         = first_goal
 let goal_goal_list     = goal_goal_list
@@ -138,37 +136,6 @@ let tclFIRSTLIST       = tclFIRSTLIST
 let tclIDTAC_list      = tclIDTAC_list
 
 
-(********************************************************)
-(* Functions for handling the state of the proof editor *)
-(********************************************************)
-
-type pftreestate = Refiner.pftreestate
-
-let proof_of_pftreestate    = proof_of_pftreestate
-let cursor_of_pftreestate   = cursor_of_pftreestate
-let is_top_pftreestate      = is_top_pftreestate
-let evc_of_pftreestate      = evc_of_pftreestate
-let top_goal_of_pftreestate = top_goal_of_pftreestate
-let nth_goal_of_pftreestate = nth_goal_of_pftreestate
-let traverse                = traverse
-let solve_nth_pftreestate   = solve_nth_pftreestate
-let solve_pftreestate       = solve_pftreestate
-let weak_undo_pftreestate   = weak_undo_pftreestate
-let mk_pftreestate          = mk_pftreestate
-let extract_pftreestate     = extract_pftreestate
-let extract_open_pftreestate = extract_open_pftreestate
-let first_unproven          = first_unproven
-let last_unproven           = last_unproven
-let nth_unproven            = nth_unproven
-let node_prev_unproven      = node_prev_unproven
-let node_next_unproven      = node_next_unproven
-let next_unproven           = next_unproven
-let prev_unproven           = prev_unproven
-let top_of_tree             = top_of_tree
-let frontier                = frontier
-let change_constraints_pftreestate = change_constraints_pftreestate
-
-
 (********************************************)
 (* Definition of the most primitive tactics *)
 (********************************************)
@@ -243,10 +210,18 @@ let rec pr_list f = function
   | []   -> mt ()
   | a::l1 -> (f a) ++ pr_list f l1
 
+let db_pr_goal sigma g =
+  let env = Goal.V82.env sigma g in
+  let penv = print_named_context env in
+  let pc = print_constr_env env (Goal.V82.concl sigma g) in
+  str"  " ++ hv 0 (penv ++ fnl () ++
+                   str "============================" ++ fnl ()  ++
+                   str" "  ++ pc) ++ fnl ()
+
 let pr_gls gls =
-  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
 
 let pr_glls glls =
   hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
-         prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
+         prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls))
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a808ca419..f4bb1d922 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,7 +15,6 @@ open Sign
 open Environ
 open Evd
 open Reduction
-open Proof_trees
 open Proof_type
 open Refiner
 open Redexpr
@@ -27,7 +26,6 @@ open Pattern
 (* Operations for handling terms under a local typing context. *)
 
 type 'a sigma   = 'a Evd.sigma;;
-type validation = Proof_type.validation;;
 type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
@@ -38,7 +36,7 @@ val re_sig : 'a -> evar_map -> 'a sigma
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
-  evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
+  evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) 
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
@@ -90,38 +88,6 @@ val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
-type transformation_tactic = proof_tree -> (goal list * validation)
-
-val frontier : transformation_tactic
-
-
-(*s Functions for handling the state of the proof editor. *)
-
-type pftreestate = Refiner.pftreestate
-
-val proof_of_pftreestate    : pftreestate -> proof_tree
-val cursor_of_pftreestate   : pftreestate -> int list
-val is_top_pftreestate      : pftreestate -> bool
-val evc_of_pftreestate      : pftreestate -> evar_map
-val top_goal_of_pftreestate : pftreestate -> goal sigma
-val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
-val traverse                : int -> pftreestate -> pftreestate
-val weak_undo_pftreestate   : pftreestate -> pftreestate
-val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
-val solve_pftreestate       : tactic -> pftreestate -> pftreestate
-val mk_pftreestate          : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
-val extract_pftreestate     : pftreestate -> constr
-val first_unproven          : pftreestate -> pftreestate
-val last_unproven           : pftreestate -> pftreestate
-val nth_unproven            : int -> pftreestate -> pftreestate
-val node_prev_unproven      : int -> pftreestate -> pftreestate
-val node_next_unproven      : int -> pftreestate -> pftreestate
-val next_unproven           : pftreestate -> pftreestate
-val prev_unproven           : pftreestate -> pftreestate
-val top_of_tree             : pftreestate -> pftreestate
-val change_constraints_pftreestate :
-  evar_map -> pftreestate -> pftreestate
 
 (*s The most primitive tactics. *)
 
@@ -159,7 +125,7 @@ val rename_hyp       : (identifier*identifier) list -> tactic
 
 type validation_list = proof_tree list -> proof_tree list
 
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = Refiner.tactic_list
 
 val first_goal         : 'a list sigma -> 'a sigma
 val goal_goal_list     : 'a sigma -> 'a list sigma
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index ea8ab5b62..f6b2ce452 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -36,8 +36,18 @@ let explain_logic_error = ref (fun e -> mt())
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
 (* Prints the goal *)
+
+let db_pr_goal g =
+  let env = Refiner.pf_env g in
+  let penv = print_named_context env in
+  let pc = print_constr_env env (Goal.V82.concl (Refiner.project g) (Refiner.sig_it g)) in
+  str"  " ++ hv 0 (penv ++ fnl () ++
+                   str "============================" ++ fnl ()  ++
+                   str" "  ++ pc) ++ fnl ()
+
 let db_pr_goal g =
-  msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
+  msgnl (str "Goal:" ++ fnl () ++ db_pr_goal g)
+
 
 (* Prints the commands *)
 let help () =