Merge pull request #103 from ppedrot/tacmach-tacticals-old

Adapt w.r.t. coq/coq#15159.

src/aac_rewrite.ml

@@ -144,7 +144,7 @@ let by_aac_reflexivity zero
   <*> tclTac_or_exn apply_tac Coq.user_error (Pp.strbrk "unification failure")
   <*> tclTac_or_exn (time_tac "vm_norm" Tactics.normalise_in_concl) Coq.anomaly "vm_compute failure"
   <*> tclORELSE Tactics.reflexivity
-	(fun _ -> Tacticals.New.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
+	(fun _ -> Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
 
 
 
@@ -169,7 +169,7 @@ let by_aac_normalise zero lift ir t t' =
   let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|])   in
   let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast in
   let apply_tac = Tactics.apply normalise_thm in
-  Tacticals.New.tclTHENLIST
+  Tacticals.tclTHENLIST
     [ Coq.tclRETYPE normalise_thm; Coq.tclRETYPE convert_to;
        convert ;
        apply_tac;
@@ -202,12 +202,12 @@ let aac_normalise =
   let open Proofview.Notations in
   let open Proofview in
   Proofview.Goal.enter (fun goal -> 
-      let ids = Tacmach.New.pf_ids_of_hyps goal in
+      let ids = Tacmach.pf_ids_of_hyps goal in
       let env = Proofview.Goal.env goal in
       tclEVARMAP >>= fun sigma ->
       let concl = Proofview.Goal.concl goal in
       let sigma,left,lift,ir,tleft,tright = aac_conclude env sigma concl in
-      Tacticals.New.tclTHENLIST
+      Tacticals.tclTHENLIST
     [
       Unsafe.tclEVARS sigma;
       by_aac_normalise left lift ir tleft tright;
@@ -273,7 +273,7 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equ
 	         right;
 	       |])
       in
-      Tacticals.New.tclTHENLIST
+      Tacticals.tclTHENLIST
         [ Coq.tclRETYPE lift_transitivity;
           Tactics.apply lift_transitivity
         ]
@@ -294,7 +294,7 @@ let core_aac_rewrite ?abort
         lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt
       in
       let rew = Coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst in
-      Tacticals.New.tclTHENS
+      Tacticals.tclTHENS
         (tclTac_or_exn (tran_tac) Coq.anomaly "Unable to make the transitivity step")
         (
 	  if rewinfo.in_left
@@ -344,7 +344,7 @@ let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
         | Some (left, right, rlt) -> left,right,rlt
       in
       let check_type x =
-        Tacmach.New.pf_conv_x goal x rlt.Coq.Relation.carrier
+        Tacmach.pf_conv_x goal x rlt.Coq.Relation.carrier
       in
       let hypinfo = Coq.Rewrite.get_hypinfo env sigma ?check_type:(Some check_type) rew ~l2r in
       let sigma,rewinfo = dispatch env sigma in_left concl hypinfo in
@@ -382,7 +382,7 @@ let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
                core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject
              with
              | NoSolutions ->
-                Tacticals.New.tclFAIL 0
+                Tacticals.tclFAIL 0
 	          (Pp.str (if occ_subterm = None && occ_sol = None
 		           then "No matching occurrence modulo AC found"
 		           else "No such solution"))

src/coq.ml

@@ -48,7 +48,7 @@ let tclEVARS sigma gl =
   { it = [gl.it]; sigma }
 
 let retype c gl =
-  let sigma, _ = Tacmach.pf_apply Typing.type_of gl c in
+  let sigma, _ = Tacmach.Old.pf_apply Typing.type_of gl c in
   tclEVARS sigma gl
 
 (* similar to retype above. No Idea when/why this is needed, I smell some ugly hack.
@@ -99,9 +99,9 @@ let cps_mk_letin
 : Proofview.V82.tac =
   fun goal ->
     let name = (Id.of_string name) in
-    let name =  Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.pf_env goal) in
+    let name =  Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.Old.pf_env goal) in
     let letin = (Proofview.V82.of_tactic (Tactics.letin_tac None  (Name name) c None nowhere)) in
-    Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))] goal
+    Tacticals.Old.tclTHENLIST [retype c; letin; (k (mkVar name))] goal
 
 let mk_letin (name:string) (c: constr) : constr Proofview.tactic =
   let open Proofview.Notations in
@@ -118,17 +118,17 @@ let mk_letin (name:string) (c: constr) : constr Proofview.tactic =
 
 type goal_sigma =  Goal.goal Evd.sigma
 let goal_update (goal : goal_sigma) evar_map : goal_sigma =
-  let it = Tacmach.sig_it goal in
-  Tacmach.re_sig it evar_map
+  let it = Tacmach.Old.sig_it goal in
+  Tacmach.Old.re_sig it evar_map
 
 let resolve_one_typeclass goal ty : constr*goal_sigma=
-  let env = Tacmach.pf_env goal in
-  let evar_map = Tacmach.project goal in
+  let env = Tacmach.Old.pf_env goal in
+  let evar_map = Tacmach.Old.project goal in
   let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in
     c, (goal_update goal em)
 
 let cps_resolve_one_typeclass ?error : types -> (constr  -> Proofview.V82.tac) -> Proofview.V82.tac = fun t k  goal  ->
-  Tacmach.pf_apply
+  Tacmach.Old.pf_apply
     (fun env em -> let em ,c =  
 		  try Typeclasses.resolve_one_typeclass env em t
 		  with Not_found ->
@@ -137,12 +137,12 @@ let cps_resolve_one_typeclass ?error : types -> (constr  -> Proofview.V82.tac) -
 		      | Some x -> CErrors.user_err x
 		    end
 		in
-		Tacticals.tclTHENLIST [tclEVARS em; k c] goal
+		Tacticals.Old.tclTHENLIST [tclEVARS em; k c] goal
     )	goal
 
 
 let nf_evar goal c : constr=
-  let evar_map = Tacmach.project goal in
+  let evar_map = Tacmach.Old.project goal in
   Evarutil.nf_evar evar_map c
 
   (* TODO: refactor following similar functions*)
@@ -541,7 +541,7 @@ let rewrite ?(abort=false) hypinfo subst =
 	    ~with_evars:true
 	    (rew,Tactypes.NoBindings)
     else
-      Tacticals.New.tclIDTAC
+      Tacticals.tclIDTAC
   in tac
 
 

src/print.ml

@@ -72,7 +72,7 @@ let print rlt ir m (context : EConstr.rel_context) : unit Proofview.tactic =
   if Search_monad.count m = 0
   then
     (
-      Tacticals.New.tclFAIL 0  (Pp.str "No subterm modulo AC")
+      Tacticals.tclFAIL 0  (Pp.str "No subterm modulo AC")
     )
   else
     let _ = Feedback.msg_notice (Pp.str "All solutions:") in
@@ -101,5 +101,5 @@ let print rlt ir m (context : EConstr.rel_context) : unit Proofview.tactic =
 	 (fun t -> Printer.pr_letype_env env sigma (Theory.Trans.raw_constr_of_t ir rlt  context  t)) m
       )
     in
-    Tacticals.New.tclIDTAC
+    Tacticals.tclIDTAC