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

1 files changed, 47 insertions, 572 deletions

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