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

7 files changed, 149 insertions, 144 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8edb16850f..2da4b61478 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -175,7 +175,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g ->
     let prov_id = pf_get_new_id hyp_id g in
     tclTHENS
-      ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
+      ((* observe_tac msg *) Proofview.V82.of_tactic (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac))))
       [tclTHENLIST
       [
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -189,7 +189,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
   let nb_intros = List.length context in
   tclTHENLIST
     [
-      tclDO nb_intros intro; (* introducing context *)
+      tclDO nb_intros (Proofview.V82.of_tactic intro); (* introducing context *)
       (fun g ->
 	 let context_hyps =
 	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
@@ -322,7 +322,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     in
     let prove_new_hyp : tactic =
       tclTHEN
-	(tclDO ctxt_size intro)
+	(tclDO ctxt_size (Proofview.V82.of_tactic intro))
 	(fun g ->
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
@@ -395,7 +395,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
 	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
 	| eq_id::eq_ids ->
 	    tclTHEN
-	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
 	      (do_rewrite eq_ids)
 	      g
   in
@@ -433,7 +433,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	      let context_length = List.length context in
 	      tclTHENLIST
 		[
-		  tclDO context_length intro;
+		  tclDO context_length (Proofview.V82.of_tactic intro);
 		  (fun g ->
 		     let context_hyps_ids =
 		       fst (list_chop ~msg:"rec hyp : context_hyps"
@@ -447,7 +447,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (assert_tac (Name rec_pte_id) t_x)
+		       (Proofview.V82.of_tactic (assert_tac (Name rec_pte_id) t_x))
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
@@ -484,7 +484,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  let prove_trivial =
 	    let nb_intro = List.length context in
 	    tclTHENLIST [
-	      tclDO nb_intro intro;
+	      tclDO nb_intro (Proofview.V82.of_tactic intro);
 	      (fun g ->
 		 let context_hyps =
 		   fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
@@ -583,9 +583,9 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
     tclTHENLIST
       [
 	(* We first introduce the variables *)
-	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
+	tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps));
 	(* Then the equation itself *)
-	intro_using heq_id;
+	Proofview.V82.of_tactic (intro_using heq_id);
 	onLastHypId (fun heq_id -> tclTHENLIST [
 	(* Then the new hypothesis *)
 	tclMAP introduction_no_check dyn_infos.rec_hyps;
@@ -636,7 +636,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
-	    pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
+	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args)));
 	    thin [hid];
 	    h_rename [prov_hid,hid]
 	  ] g
@@ -704,7 +704,7 @@ let build_proof
 		      thin dyn_infos.rec_hyps;
 		      pattern_option [Locus.AllOccurrencesBut [1],t] None;
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [h_simplest_case t;
+			 tclTHENSEQ [Proofview.V82.of_tactic (h_simplest_case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -729,7 +729,7 @@ let build_proof
 		match kind_of_term( pf_concl g) with
 		  | Prod _ ->
 		      tclTHEN
-			intro
+			(Proofview.V82.of_tactic intro)
 			(fun g' ->
 			   let (id,_,_) = pf_last_hyp g' in
 			   let new_term =
@@ -965,13 +965,13 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let prove_replacement =
     tclTHENSEQ
       [
-	tclDO (nb_params + rec_args_num + 1) intro;
+	tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
 	(* observe_tac "" *) (fun g ->
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,NoBindings));
-	      intros_reflexivity] g
+	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (h_case false (mkVar rec_id,NoBindings)));
+	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
   in
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
     (fun _ _ -> ());
-  Pfedit.by (prove_replacement);
+  Pfedit.by (Proofview.V82.tactic prove_replacement);
   Lemmas.save_named false
 
 
@@ -1019,12 +1019,12 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
-      (tclDO nb_intro_to_do intro)
+      (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro))
       (
 	fun g' ->
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
 	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
-	  tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
+	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g'
       )
       g
 
@@ -1206,9 +1206,9 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ
-	[ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params));
-	  (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates));
-	  (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches));
+	[ (* observe_tac "introducing params" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params));
+	  (* observe_tac "introducing predictes" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates));
+	  (* observe_tac "introducing branches" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches));
 	  (* observe_tac "building fixes" *) mk_fixes;
 	]
     in
@@ -1225,7 +1225,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
 	    [
-	      (* observe_tac ("introducing args") *) (tclDO nb_args intro);
+	      (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro));
 	      (fun g -> (* replacement of the function by its body *)
 		 let args = nLastDecls nb_args g in
 		 let fix_body = fix_info.body_with_param in
@@ -1289,7 +1289,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	  let nb_args = min (princ_info.nargs) (List.length ctxt) in
 	  tclTHENSEQ
 	    [
-	      tclDO nb_args intro;
+	      tclDO nb_args (Proofview.V82.of_tactic intro);
 	      (fun g -> (* replacement of the function by its body *)
 		 let args = nLastDecls nb_args g in
 		 let args_id = List.map (fun (id,_,_) -> id) args in
@@ -1386,7 +1386,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
   fun gls ->
     let eqs = List.map mkVar eqs in
     let rewrite =
-      tclFIRST (List.map Equality.rewriteRL eqs )
+      tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
     let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in
     let f_app = Array.last (snd (destApp hrec_concl)) in
@@ -1411,8 +1411,8 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl ->
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
-		    (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences
-			       true (* dep proofs also: *) true id (mkVar eq) false))
+		    (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences
+			       true (* dep proofs also: *) true id (mkVar eq) false)))
 		    gl
 	       )
 	       eqs
@@ -1543,9 +1543,9 @@ let prove_principle_for_gen
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
 	    (tclTHEN
-	       (assert_by (Name wf_thm_id)
+	       (Proofview.V82.of_tactic (assert_by (Name wf_thm_id)
 		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
-		  (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
+		  (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))))
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
@@ -1583,8 +1583,8 @@ let prove_principle_for_gen
       tclTHENSEQ
 	[
 	  generalize [lemma];
-	  h_intro hid;
-	  Elim.h_decompose_and (mkVar hid);
+	  Proofview.V82.of_tactic (h_intro hid);
+	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
 	     tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));
@@ -1606,10 +1606,10 @@ let prove_principle_for_gen
 	(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
-      (* observe_tac "" *) (assert_by
+      (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
 	 (Name acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
-	 (prove_rec_arg_acc)
+	 (Proofview.V82.tactic prove_rec_arg_acc)
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
@@ -1617,7 +1617,7 @@ let prove_principle_for_gen
       (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
-      Equality.rewriteLR (mkConst eq_ref);
+      Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
 	   let _,args = destApp (pf_concl gl') in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e5d8fe4c1f..0850d556cc 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
       (hook new_principle_type)
     ;
     (*       let _tim1 = System.get_time ()  in *)
-    Pfedit.by  (proof_tac (Array.map mkConst funs) mutr_nparams);
+    Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e65ca94f06..b317cec0d5 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -71,7 +71,7 @@ END
 TACTIC EXTEND newfuninv
    [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
      [
-       Invfun.invfun hyp fname
+       Proofview.V82.tactic (Invfun.invfun hyp fname)
      ]
 END
 
@@ -98,7 +98,7 @@ TACTIC EXTEND newfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
+       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x pat)) princl ]
 END
 (***** debug only ***)
 TACTIC EXTEND snewfunind
@@ -109,7 +109,7 @@ TACTIC EXTEND snewfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
+       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x pat)) princl ]
 END
 
 
@@ -318,10 +318,10 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)
+    (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
     (tclTHENFIRST
-      (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))
-      Tactics.reflexivity)
+      (Proofview.V82.of_tactic (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)))
+      (Proofview.V82.of_tactic Tactics.reflexivity))
     gl
 
 
@@ -432,7 +432,7 @@ TACTIC EXTEND finduction
 	  | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
 	  | _ ->
 	      let heuristic = chose_heuristic oi in
-	      finduction (Some id) heuristic tclIDTAC
+	      Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC)
       ]
 END
 
@@ -442,13 +442,13 @@ TACTIC EXTEND fauto
     [ "fauto" tactic(tac)] ->
       [
 	let heuristic = chose_heuristic None in
-	finduction None heuristic (Tacinterp.eval_tactic tac)
+	Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac)))
       ]
   |
     [ "fauto" ] ->
       [
 	let heuristic = chose_heuristic None in
-	finduction None heuristic tclIDTAC
+	Proofview.V82.tactic (finduction None heuristic tclIDTAC)
       ]
 
 END
@@ -456,7 +456,7 @@ END
 
 TACTIC EXTEND poseq
   [ "poseq" ident(x) constr(c) ] ->
-      [ poseq x c ]
+      [ Proofview.V82.tactic (poseq x c) ]
 END
 
 VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 34814c350e..4f32feb244 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -105,18 +105,18 @@ let functional_induction with_clean c princl pat =
 	    }
 	in
 	Tacticals.tclTHEN
-	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl )
+	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
 	  (Hiddentac.h_reduce flag Locusops.allHypsAndConcl)
 	  g
       else Tacticals.tclIDTAC g
     in
     Tacticals.tclTHEN
-      (choose_dest_or_ind
+      (Proofview.V82.of_tactic (choose_dest_or_ind
 	 princ_infos
 	 args_as_induction_constr
 	 princ'
 	 (None,pat)
-         None)
+         None))
       subst_and_reduce
       g
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 04cc139c01..e5b975e149 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -484,7 +484,7 @@ let jmeq_refl () =
   with e when Errors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
-  tclMAP h_intro l
+  tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) l
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
@@ -503,5 +503,5 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
 let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
   tclREPEAT
     (List.fold_right
-       (fun (eq,b) i -> tclORELSE ((if b then Equality.rewriteLR else Equality.rewriteRL) eq) i)
+       (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4f7a61fbf2..ce25f7aaf0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -399,7 +399,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in 
 					       match l with 
 						 | [] -> tclIDTAC 
-						 | _ -> h_intro_patterns l);
+						 | _ -> Proofview.V82.of_tactic (h_intro_patterns l));
 	    (* unfolding of all the defined variables introduced by this branch *)
 	    (* observe_tac "unfolding" pre_tac; *)
 	    (* $zeta$ normalizing of the conclusion *)
@@ -414,9 +414,9 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac ("toto ") tclIDTAC;
     
 	    (* introducing the the result of the graph and the equality hypothesis *)
-	    observe_tac "introducing" (tclMAP h_intro [res;hres]);
+	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres));
+	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g -> h_exact (app_constructor g) g)  
 	  ]
@@ -466,11 +466,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     in
     tclTHENSEQ
       [ 
-	observe_tac "principle" (assert_by
+	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (h_exact f_principle));
-	observe_tac "intro args_names" (tclMAP h_intro args_names);
+	  (Proofview.V82.tactic (h_exact f_principle))));
+	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
 	tclTHEN_i
@@ -741,7 +741,7 @@ and intros_with_rewrite_aux : tactic =
  		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g
+			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id); thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
 			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
@@ -759,18 +759,18 @@ and intros_with_rewrite_aux : tactic =
 		      else if isVar args.(1)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ h_intro id;
+			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);
 				     generalize_dependent_of (destVar args.(1)) id;
-				     tclTRY (Equality.rewriteLR (mkVar id));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
 		      else if isVar args.(2) 
 		      then 
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ h_intro id;
+			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);
 				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Equality.rewriteRL (mkVar id));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -778,16 +778,16 @@ and intros_with_rewrite_aux : tactic =
 			begin
 			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
-			    h_intro id;
-			    tclTRY (Equality.rewriteLR (mkVar id));
+			    Proofview.V82.of_tactic (h_intro id);
+			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 			    intros_with_rewrite
 			  ] g
 			end
 		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
-		      Tauto.tauto g
+		      Proofview.V82.of_tactic Tauto.tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			h_case false (v,NoBindings);
+			Proofview.V82.of_tactic (h_case false (v,NoBindings));
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -803,7 +803,7 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		  | _ ->
 		      let id = pf_get_new_id (Id.of_string "y") g  in
-		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+		      tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);intros_with_rewrite] g
 	      end
 	  | LetIn _ ->
 	      tclTHENSEQ[
@@ -824,12 +824,12 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      h_case false (v,NoBindings);
-	      intros;
+	      Proofview.V82.of_tactic (h_case false (v,NoBindings));
+	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
-	| _ -> reflexivity
-    with e when Errors.noncritical e -> reflexivity
+        | _ -> Proofview.V82.of_tactic reflexivity
+    with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
   let eq_ind =     Coqlib.build_coq_eq () in
   let discr_inject =
@@ -841,15 +841,15 @@ let rec reflexivity_with_destruct_cases g =
 	       match kind_of_term  (pf_type_of g (mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
-		     then Equality.discrHyp id g
+		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite]  g
+		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
   in
   (tclFIRST
-    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity;
+    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" (Proofview.V82.of_tactic reflexivity);
       observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
       (*  We reach this point ONLY if
 	  the same value is matched (at least) two times
@@ -948,8 +948,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma")
 	in
 	tclTHENSEQ[
-	  tclMAP h_intro ids;
-	  Equality.rewriteLR (mkConst eq_lemma);
+	  tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) ids;
+	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
 	  h_reduce
@@ -996,12 +996,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let params_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar params_names in
     tclTHENSEQ
-      [ tclMAP h_intro (args_names@[res;hres]);
+      [ tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
 	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
-	h_intro graph_principle_id;
+	Proofview.V82.of_tactic (h_intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -1070,8 +1070,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
            (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
-	      (proving_tac i));
+	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
+	      (proving_tac i)));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
@@ -1121,8 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
            (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i));
+	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+	      (proving_tac i)));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
@@ -1162,7 +1162,7 @@ let revert_graph kn post_tac hid g =
 		    [
 		      h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
 		      thin [hid];
-		      h_intro hid;
+		      Proofview.V82.of_tactic (h_intro hid);
 		      post_tac hid
 		    ]
 		    g
@@ -1197,7 +1197,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
 	      | App(f,f_args),_ when eq_constr f fconst ->
-		  ((fun hid -> h_symmetry (Locusops.onHyp hid)),f_args,args.(2))
+		  ((fun hid -> Proofview.V82.of_tactic (h_symmetry (Locusops.onHyp hid))),f_args,args.(2))
 	      |_,App(f,f_args) when eq_constr f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
@@ -1206,8 +1206,8 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    pre_tac hid;
 	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
-	    h_intro hid;
-	    Inv.inv FullInversion None (NamedHyp hid);
+	    Proofview.V82.of_tactic (h_intro hid);
+	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
@@ -1228,7 +1228,9 @@ let invfun qhyp f  =
     let f_correct = mkConst(Option.get finfos.correctness_lemma)
     and kn = fst finfos.graph_ind
     in
-    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
+    Proofview.V82.of_tactic (
+      Tactics.try_intros_until (fun hid -> Proofview.V82.tactic (functional_inversion kn hid (mkConst f)  f_correct)) qhyp
+    )
   with
     | Not_found ->  error "No graph found"
     | Option.IsNone  -> error "Cannot use equivalence with graph!"
@@ -1238,8 +1240,9 @@ let invfun qhyp f g =
   match f with
     | Some f -> invfun qhyp f g
     | None ->
+        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
-	  (fun hid g ->
+	  (fun hid -> Proofview.V82.tactic begin fun g ->
 	     let hyp_typ = pf_type_of g (mkVar hid)  in
 	     match kind_of_term hyp_typ with
 	       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
@@ -1276,6 +1279,7 @@ let invfun qhyp f g =
 			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
 	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
-	  )
+	  end)
 	  qhyp
+          end
 	  g
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a779680924..76095cb1c8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -383,7 +383,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
     tclTHENSEQ 
       [
 	h_intros (List.rev rev_ids);
-	intro_using teq_id;
+	Proofview.V82.of_tactic (intro_using teq_id);
 	onLastHypId (fun heq -> 
 	  tclTHENSEQ[
 	    thin to_intros;
@@ -534,15 +534,16 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
       tclTHENLIST[
-	split (ImplicitBindings [s_max]);
-	intro_then
+	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
+	Proofview.V82.of_tactic (intro_then
 	  (fun id -> 
+            Proofview.V82.tactic begin
 	    observe_tac (str "destruct_bounds_aux") 
-	      (tclTHENS (simplest_case (mkVar id))
+	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
 		 [
-		   tclTHENLIST[intro_using h_id;
-			       simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
-			       default_full_auto];
+		   tclTHENLIST[Proofview.V82.of_tactic (intro_using h_id);
+			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
+			       Proofview.V82.of_tactic default_full_auto];
 		   tclTHENLIST[
 		     observe_tac (str "clearing k ") (clear [id]);
 		     h_intros [k;h';def];
@@ -564,25 +565,25 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 			 
 			 (observe_tac (str "finishing") 
 			    (tclORELSE
-			       h_reflexivity
+			       (Proofview.V82.of_tactic h_reflexivity)
 			       (observe_tac (str "calling prove_lt") (prove_lt hyple))))])
 		   ]
 	      ]
-	      ))
+	      )end))
 	  ] g
       | (_,v_bound)::l -> 
       tclTHENLIST[
-	simplest_elim (mkVar v_bound);
+	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
 	h_clear false [v_bound];
-	tclDO 2 intro;
+	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 
 	  (fun p_hyp -> 
 	    (onNthHypId 2 
 	       (fun p ->  
 		 tclTHENLIST[
-		   simplest_elim 
-		     (mkApp(delayed_force max_constr, [| bound; mkVar p|]));
-		   tclDO 3 intro;
+		   Proofview.V82.of_tactic (simplest_elim 
+		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
+		   tclDO 3 (Proofview.V82.of_tactic intro);
 		   onNLastHypsId 3 (fun lids -> 
 		     match lids with
 		       [hle2;hle1;pmax] -> 
@@ -606,7 +607,7 @@ let terminate_app f_and_args expr_info continuation_tac infos =
       tclTHENLIST[
 	continuation_tac infos;
 	observe_tac (str "first split") 
-	  (split (ImplicitBindings [infos.info]));
+	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
 	observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
       ]
     else continuation_tac infos
@@ -617,7 +618,7 @@ let terminate_others _ expr_info continuation_tac infos =
     tclTHENLIST[
 	    continuation_tac infos;
       observe_tac (str "first split") 
-	(split (ImplicitBindings [infos.info]));
+	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
       observe_tac (str "destruct_bounds") (destruct_bounds infos)
     ]
   else continuation_tac infos
@@ -665,7 +666,7 @@ let mkDestructEq :
       (fun g2 ->
 	change_in_concl None
 	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
-      simplest_case expr], to_revert
+      Proofview.V82.of_tactic (simplest_case expr)], to_revert
 
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -711,7 +712,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	then
 	  tclTHENLIST[ 
 	    observe_tac (str "first split")
-	      (split (ImplicitBindings [new_infos.info]));
+	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 	    observe_tac (str "destruct_bounds (3)")
 	      (destruct_bounds new_infos)
 	  ]
@@ -720,11 +721,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
       ]    
     with Not_found -> 
       observe_tac (str "terminate_app_rec not found") (tclTHENS
-	(simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))
+	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
 	[		
 	  tclTHENLIST[
-	    intro_using rec_res_id;
-	    intro;
+	    Proofview.V82.of_tactic (intro_using rec_res_id);
+	    Proofview.V82.of_tactic intro;
 	    onNthHypId 1 
 	      (fun v_bound -> 
 		(onNthHypId 2 
@@ -741,7 +742,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 		       then
 			 tclTHENLIST[ 
 			   observe_tac (str "first split") 
-			     (split (ImplicitBindings [new_infos.info]));
+			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 			   observe_tac (str "destruct_bounds (2)") 
 			     (destruct_bounds new_infos)
 			 ]
@@ -836,12 +837,12 @@ let rec make_rewrite_list expr_info max = function
 	    let def_na,_,_ = destProd t in
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
-	  general_rewrite_bindings false Locus.AllOccurrences
+	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
 			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S max)]) false g) )
+			      (f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        tclTHENLIST[ (* x < S max proof *)
@@ -863,12 +864,12 @@ let make_rewrite expr_info l hp max =
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
 	 observe_tac (str "general_rewrite_bindings")
-	   (general_rewrite_bindings false Locus.AllOccurrences
+	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
 			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S (f_S max))]) false) g)
+			      (f_S (f_S max))]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (tclTHENLIST[
@@ -879,7 +880,7 @@ let make_rewrite expr_info l hp max =
 	   
 	   (list_rewrite true 
 	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
-	   (observe_tac (str "h_reflexivity") h_reflexivity)]))
+	   (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic h_reflexivity))]))
        ;
 	 tclTHENLIST[ (* x < S (S max) proof *)
 	 apply (delayed_force le_lt_SS);
@@ -893,9 +894,9 @@ let rec compute_max rew_tac max l =
     | [] -> rew_tac max
     | (_,p,_)::l -> 
       tclTHENLIST[
-	simplest_elim 
-	  (mkApp(delayed_force max_constr, [| max; mkVar p|]));
-	tclDO 3 intro;
+	Proofview.V82.of_tactic (simplest_elim 
+	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
+	tclDO 3 (Proofview.V82.of_tactic intro);
 	onNLastHypsId 3 (fun lids -> 
 	  match lids with
 	    | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l 
@@ -913,9 +914,9 @@ let rec destruct_hex expr_info acc l =
       end
     | (v,hex)::l -> 
       tclTHENLIST[
-	simplest_case (mkVar hex);
+	Proofview.V82.of_tactic (simplest_case (mkVar hex));
 	clear [hex];
-	tclDO 2 intro;
+	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 (fun hp -> 
 	  onNthHypId 2 (fun p -> 
 	    observe_tac 
@@ -928,7 +929,7 @@ let rec destruct_hex expr_info acc l =
 let rec intros_values_eq expr_info acc = 
   tclORELSE(
     tclTHENLIST[
-      tclDO 2 intro;
+      tclDO 2 (Proofview.V82.of_tactic intro);
       onNthHypId 1 (fun hex -> 
 	(onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
       )
@@ -960,13 +961,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info =
       if expr_info.is_final && expr_info.is_main_branch 
       then 
 	tclTHENLIST
-	  [ simplest_case (mkApp (expr_info.f_terminate,Array.of_list args));
+	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
 	    observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
 	  ]
       else 
 	tclTHENLIST[
-  	  simplest_case (mkApp (expr_info.f_terminate,Array.of_list args));
+  	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	  observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
 	]
   end
@@ -1049,22 +1050,22 @@ let termination_proof_header is_mes input_type ids args_id relation
 	(tclTHENS
 	   (observe_tac
 	      (str "first assert")
-	      (assert_tac
+	      (Proofview.V82.of_tactic (assert_tac
 		 (Name wf_rec_arg)
 		 (mkApp (delayed_force acc_rel,
 			 [|input_type;relation;mkVar rec_arg_id|])
 		 )
-	      )
+	      ))
 	   )
 	   [
 	     (* accesibility proof *)
 	     tclTHENS
 	       (observe_tac
 		  (str "second assert")
-		  (assert_tac
+		  (Proofview.V82.of_tactic (assert_tac
 		     (Name wf_thm)
 		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
-		  )
+		  ))
 	       )
 	       [
 		 (* interactive proof that the relation is well_founded *)
@@ -1086,7 +1087,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       ;
 		observe_tac (str "h_fix") (h_fix (Some hrec) (nargs+1));
 		h_intros args_id;
-		h_intro wf_rec_arg;
+		Proofview.V82.of_tactic (h_intro wf_rec_arg);
 		observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
 	       ]
 	   ]
@@ -1271,11 +1272,11 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	   tclTHENSEQ
 	     [
 	       h_generalize [lemma];
-	       h_intro hid;
+	       Proofview.V82.of_tactic (h_intro hid);
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
 		  tclTHEN
-		    (Elim.h_decompose_and (mkVar hid))
+		    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
 		       lid := List.rev (List.subtract Id.equal ids' ids);
@@ -1288,7 +1289,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
       (fun g ->
 	 match kind_of_term (pf_concl g) with
 	   | App(f,_) when eq_constr f (well_founded ()) ->
-	       Auto.h_auto None [] (Some [])  g
+	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
 	   | _ ->
 	       incr h_num;
 	       (observe_tac (str "finishing using")
@@ -1318,10 +1319,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     hook;
   if Indfun_common.is_strict_tcc  ()
   then
-    by (tclIDTAC)
+    by (Proofview.V82.tactic (tclIDTAC))
   else 
     begin
-      by (
+      by (Proofview.V82.tactic begin
 	fun g ->
 	  tclTHEN
 	    (decompose_and_tac)
@@ -1330,17 +1331,17 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	 	  (List.map
 	 	     (fun c ->
 	 		tclTHENSEQ
-	 		  [intros;
+	 		  [Proofview.V82.of_tactic intros;
 	 		   h_simplest_apply (interp_constr Evd.empty (Global.env()) c);
-	 		   tclCOMPLETE Auto.default_auto
+	 		   tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
 	 		  ]
 	 	     )
 	 	     using_lemmas)
 	       ) tclIDTAC)
-	    g)
+	    g end)
     end;
   try
-    by tclIDTAC; (* raises UserError _ if the proof is complete *)
+    by (Proofview.V82.tactic tclIDTAC); (* raises UserError _ if the proof is complete *)
   with UserError _ ->
     defined ()
 
@@ -1363,9 +1364,9 @@ let com_terminate
       (Global, Proof Lemma) (Environ.named_context_val env)
       (compute_terminate_type nb_args fonctional_ref) hook;
 
-    by (observe_tac (str "starting_tac") tac_start);
-    by (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
-    				   input_type relation rec_arg_num ))
+    by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start));
+    by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+    				   input_type relation rec_arg_num )))
   in
   start_proof tclIDTAC tclIDTAC;
   try
@@ -1391,8 +1392,8 @@ let start_equation (f:global_reference) (term_f:global_reference)
     h_intros x;
     unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
     observe_tac (str "simplest_case")
-      (simplest_case (mkApp (terminate_constr,
-                             Array.of_list (List.map mkVar x))));
+      (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
+                             Array.of_list (List.map mkVar x)))));
     observe_tac (str "prove_eq") (cont_tactic x)] g;;
 
 let (com_eqn : int -> Id.t ->
@@ -1410,7 +1411,7 @@ let (com_eqn : int -> Id.t ->
     (start_proof eq_name (Global, Proof Lemma)
        (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      by
-       (start_equation f_ref terminate_ref
+       (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
 	     prove_eq (fun _ -> tclIDTAC)
 	       {nb_arg=nb_arg;
@@ -1436,7 +1437,7 @@ let (com_eqn : int -> Id.t ->
 		ih = Id.of_string "______";
 	       }
 	  )
-       ); 
+       )); 
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
      Flags.silently (fun () -> Lemmas.save_named opacity) () ;