Makes the new Proofview.tactic the basic type of Ltac.

On the compilation of Coq, we can see an increase of ~20% compile time on
my completely non-scientific tests. Hopefully this can be fixed.

There are a lot of low hanging fruits, but this is an iso-functionality commit.
With a few exceptions which were not necessary for the compilation of the theories:
- The declarative mode is not yet ported
- The timeout tactical is currently deactivated because it needs some subtle
I/O. The framework is ready to handle it, but I haven't done it yet.
-  For much the same reason, the ltac debugger is unplugged. It will be more
difficult, but will eventually be back.

A few comments:
I occasionnally used a coercion from [unit Proofview.tactic] to the old
[Prooftype.tactic]. It should work smoothely, but loses any backtracking
information: the coerced tactics has at most one success.
- It is used in autorewrite (it shouldn't be a problem there). Autorewrite's
code is fairly old and tricky
- It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes
as we might want to have various success in a "Hint Extern". But it would
require a heavy port of eauto.ml4
- It is used in typeclass eauto, but with a little help from Matthieu, it should
be easy to port the whole thing to the new tactic engine, actually simplifying
the code.
- It is used in fourier. I believe it to be inocuous.
- It is used in firstorder and congruence. I think it's ok. Their code is
somewhat intricate and I'm not sure they would be easy to actually port.
- It is used heavily in Function. And honestly, I have no idea whether it can do
harm or not.

Updates:
(11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based
architecture for Ltac matching (r16533), which avoid painfully and expensively
working around the exception-throwing control flow of the previous API.
(11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730)
rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN
apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma,
rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially
tclREPEAT, causing rewrites to be tried in the side-conditions of conditional
rewrites as well). The new implementation makes Coq faster, but it is
pretty much impossible to tell if it is significant at all.

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

15 files changed, 351 insertions, 118 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index a79c9f978..76cf41c50 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -83,6 +83,13 @@ let elim_res_pf_THEN_i clenv tac gls =
   let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in
   tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
+open Proofview.Notations
+let new_elim_res_pf_THEN_i clenv tac =
+  Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>- fun clenv' ->
+  Proofview.tclTHEN
+    (Proofview.V82.tactic (clenv_refine false clenv'))
+    (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
+
 let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
 
 
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index dd46f1ec7..d172d5c36 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -20,6 +20,7 @@ val unify : ?flags:unify_flags -> constr -> tactic
 val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
+val new_elim_res_pf_THEN_i : clausenv -> (clausenv -> unit Proofview.tactic array) -> unit Proofview.tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
 val clenv_value_cast_meta : clausenv -> constr
diff --git a/proofs/goal.ml b/proofs/goal.ml
index bb9128e1d..988c10d27 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -74,6 +74,14 @@ let rec advance sigma g =
     | Evd.Evar_defined _ -> None
     | _ -> Some g
 
+
+
+(* Equality function on goals *)
+let equal evars1 gl1 evars2 gl2 =
+  let evi1 = content evars1 gl1 in
+  let evi2 = content evars2 gl2 in
+  Evd.eq_evar_info evi1 evi2
+
 (*** Goal tactics ***)
 
 
@@ -324,6 +332,9 @@ let clear_body idents env rdefs gl info =
 
 (*** Sensitive primitives ***)
 
+(* representation of the goal in form of an {!Evd.evar_info} *)
+let info _ _ _ info = info
+
 (* [concl] is the conclusion of the current goal *)
 let concl _ _ _ info =
   Evd.evar_concl info
@@ -353,10 +364,10 @@ let plus s1 s2 env rdefs goal info =
   with UndefinedHere -> s2 env rdefs goal info
 
 (* Equality of two goals *)
-let equal { content = e1 } { content = e2 } = Evar.equal e1 e2
+let equal_pointer { content = e1 } { content = e2 } = Evar.equal e1 e2
 
 let here goal value _ _ goal' _ =
-  if equal goal goal' then
+  if equal_pointer goal goal' then
     value
   else
     raise UndefinedHere
@@ -368,7 +379,7 @@ let rec list_mem_with eq x = function
   | [] -> false
 
 let here_list goals value _ _ goal' _ =
-  if list_mem_with equal goal' goals then
+  if list_mem_with equal_pointer goal' goals then
     value
   else
     raise UndefinedHere
@@ -459,6 +470,16 @@ let rec list_map f l s =
                let (l,s) = list_map f l s in
 	       (a::l,s)
 
+(* Another instance of the generic monadic map *)
+let rec sensitive_list_map f = function
+  | [] -> return []
+  | a::l ->
+      bind (f a) begin fun a' ->
+      bind (sensitive_list_map f l) begin fun l' ->
+      return (a'::l')
+      end
+      end
+
 
 (* 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
@@ -508,12 +529,6 @@ module V82 = struct
     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
@@ -587,4 +602,8 @@ module V82 = struct
 					    t
 				       ) ~init:(concl sigma gl) env
 
+  let to_sensitive f _ rsigma g _ =
+    f { Evd.it = g ; sigma = !rsigma }
+  let change_evar_map sigma _ rsigma _ _ =
+    (rsigma := sigma)
 end
diff --git a/proofs/goal.mli b/proofs/goal.mli
index c07c7f28e..718d23ccc 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -31,6 +31,10 @@ val pr_goal : goal -> Pp.std_ppcmds
 val advance : Evd.evar_map -> goal -> goal option
 
 
+(* Equality function on goals. Return [true] if all of its hypotheses
+   and conclusion are equal. *)
+val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
+
 (*** Goal tactics ***)
 
 
@@ -126,6 +130,9 @@ val rename_hyp : Names.Id.t -> Names.Id.t -> subgoals sensitive
 
 (*** Sensitive primitives ***)
 
+(* representation of the goal in form of an {!Evd.evar_info} *)
+val info : Evd.evar_info sensitive
+
 (* [concl] is the conclusion of the current goal *)
 val concl : Term.constr sensitive
 
@@ -175,6 +182,9 @@ val list_map :
   'a list -> Evd.evar_map ->
     'b list * Evd.evar_map
 
+(* emulates List.map for [sensitive] Kleisli functions. *)
+val sensitive_list_map : ('a -> 'b sensitive) -> 'a list -> 'b list sensitive
+
 (* 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. *)
@@ -204,9 +214,6 @@ module V82 : sig
                          Evd.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
 
@@ -238,4 +245,6 @@ module V82 : sig
   (* Goal represented as a type, doesn't take into account section variables *)
   val abstract_type : Evd.evar_map -> goal -> Term.types 
 
+  val to_sensitive : (goal Evd.sigma -> 'a) -> 'a sensitive
+  val change_evar_map : Evd.evar_map -> unit sensitive
 end
diff --git a/proofs/monads.ml b/proofs/monads.ml
index 78a79909e..db1df19ef 100644
--- a/proofs/monads.ml
+++ b/proofs/monads.ml
@@ -88,7 +88,7 @@ module type Logic = sig
   (* [zero] is usually argument free, but Coq likes to explain errors,
      hence error messages should be carried around. *)
   val zero : exn -> 'a t
-  val plus : 'a t -> 'a t -> 'a t
+  val plus : 'a t -> (exn -> 'a t) -> 'a t
 (** Writing (+) for plus and (>>=) for bind, we shall require that
 
     zero+x = x
@@ -101,7 +101,7 @@ module type Logic = sig
       a result [a].  In the former case it returns [Inr e], otherwise
       it returns [Inl (a,y)] where [y] can be run to get more results
       from [x]. It is a variant of prolog's cut. *)
-  val split : 'a t -> ('a * 'a t , exn ) Util.union t
+  val split : 'a t -> ('a * (exn -> 'a t) , exn ) Util.union t
 end
 (* The [T] argument represents the "global" effect: it is not
    backtracked when backtracking occurs at a [plus]. *)
@@ -142,9 +142,9 @@ end = struct
                 }
 
   let zero e = { go = fun _ fk -> fk e }
-  (* [plus x y] ignores any error raised by [x]. *)
+
   let plus x y = { go = fun sk fk ->
-    x.go sk (fun _ -> y.go sk fk)
+    x.go sk (fun e -> (y e).go sk fk)
                  }
 
   let lift x = { go = fun sk fk ->
@@ -158,19 +158,13 @@ end = struct
 
   (* For [reflect] and [split] see the "Backtracking, Interleaving,
      and Terminating Monad Transformers" paper *)
-  let reflect : ('a*'a t , exn) Util.union -> 'a t = function
+  let reflect : ('a*(exn -> 'a t) , exn) Util.union -> 'a t = function
     | Util.Inr e -> zero e
     | Util.Inl (a,x) -> plus (return a) x
 
   let split x =
-    (* spiwack: I cannot be sure right now, but [anomaly] shouldn't be
-       reachable. If it is reachable there may be some redesign to be
-       done around success continuations. *)
-    let anomaly = Errors.make_anomaly ~label:"Monads.Logic(T).split"
-      (Pp.str "[fk] should ignore this error")
-    in
     let fk e = T.return (Util.Inr e) in
-    let sk a fk = T.return (Util.Inl (a,bind (lift (fk anomaly)) reflect)) in
+    let sk a fk = T.return (Util.Inl (a,fun e -> bind (lift (fk e)) reflect)) in
     lift (x.go sk fk)
 end
 
@@ -199,7 +193,7 @@ end = struct
     let (>>) = seq in
     get >>= fun initial ->
     lift begin
-      (T.plus (run x initial) (run y initial)) 
+      (T.plus (run x initial) (fun e -> run (y e) initial)) 
     end >>= fun { result = a ; state = final } ->
     set final >>
     return a
@@ -217,8 +211,8 @@ end = struct
     lift (T.split (run x initial)) >>= function
       | Util.Inr _ as e -> return e
       | Util.Inl (a,y) ->
-          let y' =
-            lift y >>= fun b ->
+          let y' e =
+            lift (y e) >>= fun b ->
             set b.state >>
             return b.result
           in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2b0947075..55c46a340 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,7 +36,7 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
   Proof_global.with_current_proof (fun _ p ->
     match init_tac with
     | None -> p
-    | Some tac -> Proof.run_tactic env (Proofview.V82.tactic tac) p)
+    | Some tac -> Proof.run_tactic env tac p)
 
 let cook_this_proof hook p =
   match p with
@@ -92,7 +92,6 @@ let current_proof_statement () =
 
 let solve_nth ?with_end_tac gi tac pr =
   try 
-    let tac = Proofview.V82.tactic tac in
     let tac = match with_end_tac with
       | None -> tac
       | Some etac -> Proofview.tclTHEN tac etac in
@@ -156,6 +155,16 @@ let solve_by_implicit_tactic env sigma evk =
       when
 	Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac)
+      (try build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []))
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
+
+
+
+
+
+
+
+
+
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7df0da800..3a0c25c46 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -61,7 +61,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
 
 val start_proof :
   Id.t -> goal_kind -> named_context_val -> constr ->
-  ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   unit declaration_hook -> unit
 
 (** {6 ... } *)
@@ -135,14 +135,14 @@ val get_used_variables : unit -> Context.section_context option
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
 
-val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> tactic ->
+val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic ->
       Proof.proof -> Proof.proof
 
 (** [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
    if there is no more subgoals *)
 
-val by : tactic -> unit
+val by : unit Proofview.tactic -> unit
 
 (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
    existential variable of the current focused proof by [c] or raises a
@@ -155,12 +155,12 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
 val build_constant_by_tactic :
   Id.t -> named_context_val -> ?goal_kind:goal_kind ->
-    types -> tactic -> Entries.definition_entry
-val build_by_tactic : env -> types -> tactic -> constr
+    types -> unit Proofview.tactic -> Entries.definition_entry
+val build_by_tactic : env -> types -> unit Proofview.tactic -> constr
 
 (** Declare the default tactic to fill implicit arguments *)
 
-val declare_implicit_tactic : tactic -> unit
+val declare_implicit_tactic : unit Proofview.tactic -> unit
 
 (* Raise Exit if cannot solve *)
 val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 807d83384..3f84f6500 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -143,7 +143,7 @@ let cur_pstate () =
 let give_me_the_proof () = (cur_pstate ()).proof
 let get_current_proof_name () = (cur_pstate ()).pid
 
-let interp_tac = ref (fun _ _ -> assert false)
+let interp_tac = ref (fun _ -> assert false)
 let set_interp_tac f = interp_tac := f
 
 let with_current_proof f =
@@ -153,7 +153,7 @@ let with_current_proof f =
       let et =
         match p.endline_tactic with
         | None -> Proofview.tclUNIT ()
-        | Some tac -> Proofview.V82.tactic (!interp_tac tac) in
+        | Some tac -> !interp_tac tac in
       let p = { p with proof = f et p.proof } in
       pstates := p :: rest
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 144b59f4d..9b5015e0c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -87,7 +87,7 @@ val with_current_proof :
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit
 val set_interp_tac :
-  (Tacexpr.raw_tactic_expr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma)
+  (Tacexpr.raw_tactic_expr -> unit Proofview.tactic)
     -> unit
 
 (** Sets the section variables assumed by the proof *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 625ae74f1..ce2decc3e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -227,7 +227,7 @@ let tclIGNORE tac env = Inner.ignore (tac env)
    of [t1] have been depleted, then it behaves as [t2].  No
    interleaving at this point. *)
 let tclOR t1 t2 env =
-  Inner.plus (t1 env) (t2 env)
+  Inner.plus (t1 env) (fun _ -> t2 env)
 
 (* [tclZERO e] always fails with error message [e]*)
 let tclZERO e _ = Inner.zero e
@@ -238,9 +238,19 @@ let tclORELSE t1 t2 env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
   Inner.split (t1 env) >>= function
-    | Util.Inr _ -> t2 env
+    | Util.Inr e -> t2 e env
     | Util.Inl (a,t1') -> Inner.plus (Inner.return a) t1'
 
+(* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
+   succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
+   fails with [e], then it behaves as [f e]. *)
+let tclIFCATCH a s f env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.split (a env) >>= function
+    | Util.Inr e -> f e env
+    | Util.Inl (x,a') -> Inner.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
+
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 (* arnaud: bug if 0 goals ! *)
 let tclFOCUS i j t env =
@@ -248,22 +258,29 @@ let tclFOCUS i j t env =
   let (>>=) = Inner.bind in
   let (>>) = Inner.seq in
   Inner.get >>= fun initial ->
-  let (focused,context) = focus i j initial in
-  Inner.set focused >>
-  t (env) >>= fun result ->
-  Inner.get >>= fun next ->
-  Inner.set (unfocus context next) >>
-  Inner.return result
+  try
+    let (focused,context) = focus i j initial in
+    Inner.set focused >>
+    t (env) >>= fun result ->
+    Inner.get >>= fun next ->
+    Inner.set (unfocus context next) >>
+    Inner.return result
+  with e ->
+    (* spiwack: a priori the only possible exceptions are that of focus,
+       of course I haven't made them algebraic yet. *)
+    tclZERO e env
 
+(* arnaud: vérifier les commentaires de dispatch vis-à-vis de l'ordre
+   d'évaluation des buts. Ne pas oublier le mli *)
 (* 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. *)
+   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
 let _ = Errors.register_handler begin function
   | SizeMismatch -> Errors.error "Incorrect number of goals."
@@ -275,6 +292,7 @@ end
     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 =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
@@ -283,18 +301,18 @@ let rec tclDISPATCHGEN null join tacs env =
   match tacs,initial.comb with
   | [], [] -> tclUNIT null env
   | t::tacs , first::goals ->
-      Inner.set {initial with comb=goals} >>
-      tclDISPATCHGEN null join tacs env >>= fun x ->
-      Inner.get >>= fun step ->
-      begin match Goal.advance step.solution first with
-      | None -> Inner.return x (* If [first] has been solved by side effect: do nothing. *)
+      begin match Goal.advance initial.solution first with
+      | None -> Inner.return null (* If [first] has been solved by side effect: do nothing. *)
       | Some first ->
-          Inner.set {step with comb=[first]} >>
-          t env >>= fun y ->
-          Inner.get >>= fun step' ->
-          Inner.set {step' with comb=step'.comb@step.comb} >>
-          Inner.return (join x y)
-      end
+          Inner.set {initial with comb=[first]} >>
+          t env
+      end >>= fun y ->
+      Inner.get >>= fun step ->
+      Inner.set {step with comb=goals} >>
+      tclDISPATCHGEN null join tacs env >>= fun x ->
+      Inner.get >>= fun step' ->
+      Inner.set {step' with comb=step.comb@step'.comb} >>
+      Inner.return (join x y)
   | _ , _ -> raise SizeMismatch
 
 let unitK () () = ()
@@ -313,12 +331,20 @@ let here_s b env =
 (* see .mli for documentation. *)
 let tclDISPATCHS tacs = 
   let tacs = 
-    List.map begin fun tac -> 
+    List.map begin fun tac ->
       tclBIND tac here_s
     end tacs 
   in
   tclDISPATCHGEN Goal.null Goal.plus tacs
 
+let tclDISPATCHL tacs =
+  let tacs =
+    List.map begin fun tac ->
+      tclBIND tac (fun a -> tclUNIT [a])
+    end tacs
+  in
+  tclDISPATCHGEN [] (@) tacs
+
 let extend_to_list =
   let rec copy n x l =
     if n < 0 then raise SizeMismatch
@@ -337,25 +363,6 @@ let tclEXTEND tacs1 rtac tacs2 env =
   let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
   tclDISPATCH tacs env
 
-(* 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
-  | Errors.UserError _
-  | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
-  | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
-  (* unification errors *)
-  | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
-		   |NoOccurrenceFound _|CannotUnifyBindingType _
-		   |ActualTypeNotCoercible _
-		   |CannotFindWellTypedAbstraction _
-		   |UnsolvableImplicit _)) -> true
-  | Typeclasses_errors.TypeClassError 
-      (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
-  | _ -> false
-
-
 (* [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. *)
@@ -378,7 +385,7 @@ let list_of_sensitive s k env =
     let (tacs,defs) = list_of_sensitive s k env step in
     Inner.set { step with solution = defs; } >>
     Inner.return tacs
-  with e when catchable_exception e ->
+  with e when Errors.noncritical e ->
     tclZERO e env
 
 let tclGOALBIND s k =
@@ -417,9 +424,75 @@ let sensitive_on_proofview s env step =
   try
     let next = sensitive_on_proofview s env step in
     Inner.set next
-  with e when catchable_exception e ->
+  with e when Errors.noncritical e ->
     tclZERO e env
 
+(* spiwack: [lift_sensitive] is probably a better abstraction
+   than [tclGOALBIND]. *)
+let lift_sensitive s env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  let (>>) = Inner.seq in
+  Inner.get >>= fun step ->
+  let (res,sigma) =
+    Goal.list_map begin fun sigma g ->
+      Goal.eval s env step.solution g
+    end step.comb step.solution
+  in
+  Inner.set { step with solution=sigma } >>
+  Inner.return res
+
+(* arnaud: on pourrait regarder la liste de buts aussi, mais je
+   ne sais pas encore comment. Pour l'instant on fait au plus
+   simple. *)
+let tclPROGRESS t env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.get >>= fun initial ->
+  t env >>= fun res ->
+  Inner.get >>= fun final ->
+  let test =
+    Evd.progress_evar_map initial.solution final.solution &&
+    not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb)
+  in
+  if test then
+    tclUNIT res env
+  else
+    tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) env
+
+let tclEVARMAP _ =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.get >>= fun initial ->
+  Inner.return (initial.solution)
+
+let tclENV env =
+  Inner.return env
+
+let tclTIMEOUT n t = t
+(* arnaud: todo: restore
+(* Fails if a tactic hasn't finished after a certain amount of time *)
+
+exception TacTimeout
+
+let tclTIMEOUT n t g =
+  let timeout_handler _ = raise TacTimeout in
+  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+  ignore (Unix.alarm n);
+  let restore_timeout () =
+    ignore (Unix.alarm 0);
+    Sys.set_signal Sys.sigalrm psh
+  in
+  try
+    let res = t g in
+    restore_timeout ();
+    res
+  with
+    | TacTimeout | Loc.Exc_located(_,TacTimeout) ->
+      restore_timeout ();
+      errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
+    | e -> restore_timeout (); raise e
+*)
 
 (*** Commands ***)
 
@@ -437,6 +510,22 @@ module Notations = struct
   let (<+>) = tclOR
 end
 
+open Notations
+let rec list_map f = function
+  | [] -> tclUNIT []
+  | a::l ->
+      f a >= fun a' ->
+      list_map f l >= fun l' ->
+      tclUNIT (a'::l')
+
+let rec sensitive_list_map f = function
+  | [] -> tclUNIT (Goal.return [])
+  | a::l ->
+      f a >>== fun a' ->
+      sensitive_list_map f l >>== fun l' ->
+      tclUNIT (Goal.return (a'::l'))
+
+
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
@@ -462,7 +551,7 @@ module V82 = struct
       let (goalss,evd) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
       Inner.set { ps with solution=evd ; comb=sgs; }
-    with e when catchable_exception e ->
+    with e when Errors.noncritical e ->
       tclZERO e env
 
   let has_unresolved_evar pv =
@@ -509,4 +598,19 @@ module V82 = struct
     { pv with
 	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
 
+  let of_tactic t gls =
+    let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
+    let final = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+    { Evd.sigma = final.solution ; it = final.comb }
+
 end
+
+
+
+
+
+
+
+
+
+
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 135b7205f..6165b02a9 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -146,8 +146,13 @@ val tclOR : 'a tactic -> 'a tactic -> 'a tactic
 val tclZERO : exn -> 'a tactic
 
 (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
-   or [t2] if [t1] fails. *)
-val tclORELSE : 'a tactic -> 'a tactic -> 'a tactic
+   or [t2 e] if [t1] fails with [e]. *)
+val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
+
+(* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
+   succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
+   fails with [e], then it behaves as [f e]. *)
+val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tactic
 
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
@@ -162,7 +167,10 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
     sense in the goals immediatly built by it, and would cause an anomaly
     is used otherwise. *)
 val tclDISPATCH : unit tactic list -> unit tactic
+(* arnaud: quick hack to fix the order of goal solving to comply with Ltac.
+   it will probably have to go. *)
 val tclDISPATCHS : 'a Goal.sensitive tactic list -> 'a Goal.sensitive tactic
+val tclDISPATCHL : 'a tactic list -> 'a list 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
@@ -179,6 +187,26 @@ 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 
 
+(* [lift_sensitive s] returns the list corresponding to the evaluation
+   of [s] on each of the focused goals *)
+val lift_sensitive : 'a Goal.sensitive -> 'a list tactic
+
+(* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *)
+val tclPROGRESS : 'a tactic -> 'a tactic
+
+(* [tclEVARMAP] doesn't affect the proof, it returns the current evar_map. *)
+val tclEVARMAP : Evd.evar_map tactic
+
+(* [tclENV] doesn't affect the proof, it returns the current evar_map. *)
+val tclENV : Environ.env tactic
+
+(* [tclTIMEOUT n t] runs [t] for at most [n] seconds, succeeds if [t]
+   succeeds in the meantime, fails otherwise. *)
+(* arnaud: behaves as the identity for now *)
+val tclTIMEOUT : int -> unit tactic -> unit tactic
+
+val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
+val sensitive_list_map : ('a -> 'b Goal.sensitive tactic) -> 'a list -> 'b list Goal.sensitive tactic
 
 (*** Commands ***)
 
@@ -233,4 +261,9 @@ module V82 : sig
     
   (* Implements the Existential command *)
   val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
+
+  (* Caution: this function loses quite a bit of information. It
+     should be avoided as much as possible.  It should work as
+     expected for a tactic obtained from {!V82.tactic} though. *)
+  val of_tactic : 'a tactic -> tac
 end
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 583fcf553..42aa0cfb5 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -66,6 +66,7 @@ exception FailError of int * std_ppcmds Lazy.t
 (* The Fail tactic *)
 let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
 
+(* arnaud: pas utilisée supprimer ? *)
 let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =
@@ -312,27 +313,6 @@ let tclDO n t =
   in
   dorec n
 
-(* Fails if a tactic hasn't finished after a certain amount of time *)
-
-exception TacTimeout
-
-let tclTIMEOUT n t g =
-  let timeout_handler _ = raise TacTimeout in
-  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-  ignore (Unix.alarm n);
-  let restore_timeout () =
-    ignore (Unix.alarm 0);
-    Sys.set_signal Sys.sigalrm psh
-  in
-  try
-    let res = t g in
-    restore_timeout ();
-    res
-  with
-    | TacTimeout ->
-      restore_timeout ();
-      errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
-    | reraise -> restore_timeout (); raise reraise
 
 (* Beware: call by need of CAML, g is needed *)
 let rec tclREPEAT t g =
@@ -398,8 +378,7 @@ let set_info_printer f = pp_info := f
 
 (* Check that holes in arguments have been resolved *)
 
-let check_evars env sigma extsigma gl =
-  let origsigma = gl.sigma in
+let check_evars env sigma extsigma origsigma =
   let rest =
     Evd.fold_undefined (fun evk evi acc ->
       if Evd.is_undefined extsigma evk && not (Evd.mem origsigma evk) then
@@ -415,10 +394,14 @@ let check_evars env sigma extsigma gl =
     let evi = Evarutil.nf_evar_info sigma evi in
     Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
 
+let gl_check_evars env sigma extsigma gl =
+  let origsigma = gl.sigma in
+  check_evars env sigma extsigma origsigma
+
 let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
   if sigma == project gl then tac c gl
   else
     let res = tclTHEN (tclEVARS sigma) (tac c) gl in
     if not accept_unresolved_holes then
-      check_evars (pf_env gl) (res).sigma sigma gl;
+      gl_check_evars (pf_env gl) (res).sigma sigma gl;
     res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index c198958e3..8fc9e9e17 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -121,7 +121,6 @@ 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 tclTIMEOUT       : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
@@ -152,6 +151,11 @@ val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
 val tactic_list_tactic : tactic_list -> tactic
 val goal_goal_list     : 'a sigma -> 'a list sigma
 
+
+(* Check that holes in arguments have been resolved *)
+(* spiwack: used in [tclWITHHOLES] both newer and older copy. *)
+val check_evars : Environ.env -> evar_map -> evar_map -> evar_map -> unit
+
 (** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
    may have unresolved holes; if [solve_holes] these holes must be
    resolved after application of the tactic; [sigma] must be an
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b8f065b41..d08dfd67d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -203,3 +203,52 @@ let pr_glls glls =
   hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
          prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
 
+(* Variants of [Tacmach] functions built with the new proof engine *)
+module New = struct
+  open Proofview.Notations
+
+  let pf_apply f =
+    Goal.env >- fun env ->
+    Goal.defs >- fun sigma ->
+    Goal.return (f env sigma)
+
+  let of_old f =
+    Goal.V82.to_sensitive f
+
+  let pf_global id =
+    Goal.hyps >- fun hyps ->
+    let hyps = Environ.named_context_of_val hyps in
+    Goal.return (Constrintern.construct_reference hyps id)
+
+  let pf_ids_of_hyps =
+    Goal.hyps >- fun hyps ->
+      let hyps = Environ.named_context_of_val hyps in
+      Goal.return (ids_of_named_context hyps)
+
+  let pf_get_new_id id =
+    pf_ids_of_hyps >- fun ids ->
+    Goal.return (next_ident_away id ids)
+
+  let pf_get_hyp id =
+    Goal.hyps >- fun hyps ->
+    let hyps = Environ.named_context_of_val hyps in
+    let sign =
+      try Context.lookup_named id hyps
+      with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id))
+    in
+    Goal.return sign
+
+  let pf_get_hyp_typ id =
+    pf_get_hyp id >- fun (_,_,ty) ->
+    Goal.return ty
+
+  let pf_hyps_types =
+    Goal.env >- fun env ->
+    let sign = Environ.named_context env in
+    Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
+
+  let pf_last_hyp =
+    Goal.hyps >- fun hyps ->
+    Goal.return (List.hd (Environ.named_context_of_val hyps))
+
+end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ab59c6441..b3e442abc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -62,7 +62,7 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
 val pf_reduce :
   (env -> evar_map -> constr -> constr) ->
-    goal sigma -> constr -> constr
+  goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
 val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
@@ -74,7 +74,7 @@ val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
 val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
 val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-        -> goal sigma -> constr -> constr
+  -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> constant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
@@ -131,3 +131,24 @@ val tclIDTAC_list      : tactic_list
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
 val pr_glls   : goal list sigma -> Pp.std_ppcmds
+
+(* Variants of [Tacmach] functions built with the new proof engine *)
+module New : sig
+
+  val pf_apply : (env -> evar_map -> 'a) -> 'a Goal.sensitive
+  val pf_global : identifier -> constr Goal.sensitive
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a Goal.sensitive
+
+  val pf_get_new_id  : identifier -> identifier Goal.sensitive
+  val pf_ids_of_hyps : identifier list Goal.sensitive
+  val pf_hyps_types : (identifier * types) list Goal.sensitive
+
+  val pf_get_hyp : identifier -> named_declaration Goal.sensitive
+  val pf_get_hyp_typ        : identifier -> types Goal.sensitive
+  val pf_last_hyp           : named_declaration Goal.sensitive
+end
+
+
+
+
+