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

2 files changed, 57 insertions, 25 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 30ed01c499..3b8487d75d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -121,7 +121,7 @@ let start_proof_tac gls=
   tcl_change_info info gls
 
 let go_to_proof_mode () =
-  Pfedit.by start_proof_tac;
+  Pfedit.by (Proofview.V82.tactic start_proof_tac);
   let p = Proof_global.give_me_the_proof () in
   Decl_mode.focus p
 
@@ -214,7 +214,8 @@ let filter_hyps f gls =
 
 let local_hyp_prefix = Id.of_string "___"
 
-let add_justification_hyps keep items gls =
+let add_justification_hyps keep items gls = assert false
+(* arnaud: todo
   let add_aux c gls=
     match kind_of_term c with
 	Var id ->
@@ -226,6 +227,7 @@ let add_justification_hyps keep items gls =
 	    tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere)
               (thin_body [id]) gls in
     tclMAP add_aux items gls
+*)
 
 let prepare_goal items gls =
   let tokeep = ref Id.Set.empty in
@@ -235,11 +237,11 @@ let prepare_goal items gls =
        filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
 
 let my_automation_tac = ref
-  (fun gls -> anomaly (Pp.str "No automation registered"))
+  (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered")))
 
 let register_automation_tac tac = my_automation_tac:= tac
 
-let automation_tac gls = !my_automation_tac gls
+let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
 
 let justification tac gls=
     tclORELSE
@@ -253,8 +255,10 @@ let justification tac gls=
 	     daimon_tac gls
 	   end) gls
 
-let default_justification elems gls=
+let default_justification elems gls= assert false
+(* arnaud: todo
   justification (tclTHEN (prepare_goal elems) automation_tac) gls
+*)
 
 (* code for conclusion refining *)
 
@@ -452,7 +456,8 @@ let mk_stat_or_thesis info gls = function
       error "\"thesis for ...\" is not applicable here."
   | Thesis Plain -> pf_concl gls
 
-let just_tac _then cut info gls0 = 
+let just_tac _then cut info gls0 = assert false
+(* arnaud: todo
   let last_item =
     if _then then
       try [mkVar (get_last (pf_env gls0))]
@@ -471,8 +476,10 @@ let just_tac _then cut info gls0 =
       | Some tac ->
 	  (Tacinterp.eval_tactic tac) gls in
     justification (tclTHEN items_tac method_tac) gls0
+*)
 
-let instr_cut mkstat _thus _then cut gls0 =
+let instr_cut mkstat _thus _then cut gls0 = assert false
+(* arnaud:
   let info = get_its_info gls0 in
   let stat = cut.cut_stat in
   let (c_id,_) = match stat.st_label with
@@ -487,7 +494,7 @@ let instr_cut mkstat _thus _then cut gls0 =
     tclTHENS (assert_postpone c_id c_stat)
       [tclTHEN tcl_erase_info (just_tac _then cut info);
        thus_tac] gls0
-
+*)
 
 
 (* iterated equality *)
@@ -505,7 +512,8 @@ let decompose_eq id gls =
 	  else error "Previous step is not an equality."
       | _ -> error "Previous step is not an equality."
 
-let instr_rew _thus rew_side cut gls0 =
+let instr_rew _thus rew_side cut gls0 = assert false
+(* arnaud:
   let last_id =
     try get_last (pf_env gls0)
     with UserError _ -> error "No previous equality."
@@ -546,12 +554,13 @@ let instr_rew _thus rew_side cut gls0 =
 		 (tclTHENS (transitivity rhs)
 		    [exact_check (mkVar last_id);just_tac]);
 	       thus_tac new_eq] gls0
-
+*)
 
 
 (* tactics for claim/focus *)
 
-let instr_claim _thus st gls0 =
+let instr_claim _thus st gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let (id,_) = match st.st_label with
       Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false
@@ -565,10 +574,12 @@ let instr_claim _thus st gls0 =
     tclTHENS (assert_postpone id st.st_it)
       [thus_tac;
        tcl_change_info ninfo1] gls0
+*)
 
 (* tactics for assume *)
 
-let push_intro_tac coerce nam gls =
+let push_intro_tac coerce nam gls = assert false
+(* arnaud: todo
       let (hid,_) =
 	match nam with
 	    Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false
@@ -577,6 +588,7 @@ let push_intro_tac coerce nam gls =
 	  [intro_mustbe_force hid;
 	   coerce hid]
 	  gls
+*)
 
 let assume_tac hyps gls =
   List.fold_right
@@ -643,7 +655,8 @@ let rec build_applist prod = function
       let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in
 	(n,typ)::ctx,head
 
-let instr_suffices _then cut gls0 =
+let instr_suffices _then cut gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
   let ctx,hd = cut.cut_stat in
@@ -659,6 +672,7 @@ let instr_suffices _then cut gls0 =
 	   tcl_erase_info;
 	   just_tac _then cut info];
       thus_tac] gls0
+*)
 
 (* tactics for consider/given *)
 
@@ -678,7 +692,8 @@ let conjunction_arity id gls =
 	    List.length rc
       | _ -> raise Not_found
 
-let rec intron_then n ids ltac gls =
+let rec intron_then n ids ltac gls = assert false
+(* arnaud:
   if n<=0 then
     ltac ids gls
   else
@@ -686,9 +701,11 @@ let rec intron_then n ids ltac gls =
       tclTHEN
 	(intro_mustbe_force id)
 	(intron_then (pred n) (id::ids) ltac) gls
+*)
 
 
-let rec consider_match may_intro introduced available expected gls =
+let rec consider_match may_intro introduced available expected gls = assert false
+(* arnaud:
   match available,expected with
       [],[] ->
 	  tclIDTAC gls
@@ -731,8 +748,10 @@ let rec consider_match may_intro introduced available expected gls =
 			 (List.rev_append l rest_ids) expected)] gls)
 	  end
 	  gls
+*)
 
-let consider_tac c hyps gls =
+let consider_tac c hyps gls = assert false
+(* arnaud: todo
   match kind_of_term (strip_outer_cast c) with
       Var id ->
 	consider_match false [] [id] hyps gls
@@ -741,6 +760,7 @@ let consider_tac c hyps gls =
 	tclTHEN
 	  (forward None (Some (Loc.ghost, IntroIdentifier id)) c)
  	  (consider_match false [] [id] hyps) gls
+*)
 
 
 let given_tac hyps gls =
@@ -768,9 +788,11 @@ let rec build_function args body =
 	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
     | [] -> body
 
-let define_tac id args body gls =
+let define_tac id args body gls = assert false
+(* arnaud: todo:
   let t = build_function args body in
     letin_tac None (Name id) t None Locusops.nowhere gls
+*)
 
 (* tactics for reconsider *)
 
@@ -903,7 +925,8 @@ let register_nodep_subcase id= function
       end
   | _ -> anomaly (Pp.str "wrong stack state")
 
-let suppose_tac hyps gls0 =
+let suppose_tac hyps gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
@@ -916,6 +939,7 @@ let suppose_tac hyps gls0 =
 		    assume_tac hyps;
 		    clear old_clauses];
        tcl_change_info ninfo2] gls0
+*)
 
 (* suppose it is ... *)
 
@@ -1104,7 +1128,8 @@ let rec register_dep_subcase id env per_info pat = function
 	(EK_dep (start_tree env per_info.per_ind per_info.per_wf))
   | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
 
-let case_tac params pat_info hyps gls0 =
+let case_tac params pat_info hyps gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
   let et,per_info,ek,old_clauses,rest =
@@ -1125,6 +1150,7 @@ let case_tac params pat_info hyps gls0 =
 	  assume_hyps_or_theses hyps;
 	  clear old_clauses];
        tcl_change_info ninfo2] gls0
+*)
 
 (* end cases *)
 
@@ -1179,7 +1205,8 @@ let hrec_for fix_id per_info gls obj_id =
     compose_lam rc (whd_beta gls.sigma hd2)
 
 
-let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
+let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = assert false
+(* arnaud: todo
   match tree, objs  with
       Close_patt t,_ ->
 	let args0 = pop_stacks args in
@@ -1272,6 +1299,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
     | End_patt (_,_) , _ :: _  ->
 	anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
+*)
 
 let understand_my_constr c gls =
   let env = pf_env gls in
@@ -1283,13 +1311,16 @@ let understand_my_constr c gls =
   in
   Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
 
-let my_refine c gls =
+let my_refine c gls = assert false
+(* arnaud: todo
   let oc = understand_my_constr c gls in
   Refine.refine oc gls
+*)
 
 (* end focus/claim *)
 
-let end_tac et2 gls =
+let end_tac et2 gls = assert false
+(* arnaud: todo
   let info = get_its_info gls in
   let et1,pi,ek,clauses =
     match info.pm_stack with
@@ -1354,6 +1385,7 @@ let end_tac et2 gls =
 			     [mkVar c_id]  0 tree] gls0
 		  end
       end gls
+*)
 
 (* escape *)
 
@@ -1463,7 +1495,7 @@ let do_instr raw_instr pts =
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
-      Pfedit.by (tclTHEN (eval_instr instr) clean_tmp)
+      Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))
     else () end;
   postprocess pts raw_instr.instr;
   (* spiwack: this should restore a compatible semantics with
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 107b653668..d78ca84d12 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -15,9 +15,9 @@ open Decl_mode
 val go_to_proof_mode: unit -> unit
 val return_from_tactic_mode: unit -> unit
 
-val register_automation_tac: tactic -> unit
+val register_automation_tac: unit Proofview.tactic -> unit
 
-val automation_tac : tactic
+val automation_tac : unit Proofview.tactic
 
 val concl_refiner:
   Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr