Removing compatibility layers from Tacticals

8 files changed, 46 insertions, 38 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2ab4dced4..53c450116 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -241,10 +241,10 @@ let build_projection intype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 let refine c = refine c
@@ -491,7 +491,6 @@ let congruence_tac depth l =
 
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
-  let fc = EConstr.of_constr fc in
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2881b5333..ef8172de4 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
+      let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
@@ -127,6 +127,7 @@ let mk_open_instance id idc gl m t=
 (* tactics   *)
 
 let left_instance_tac (inst,id) continue seq=
+  let open EConstr in
   match inst with
       Phantom dom->
 	if lookup (id,None) seq then
@@ -137,8 +138,8 @@ let left_instance_tac (inst,id) continue seq=
 	       [Proofview.V82.of_tactic introf;
                 pf_constr_of_global id (fun idc ->
 		(fun gls-> Proofview.V82.of_tactic (generalize
-		   [EConstr.of_constr (mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|]))]) gls));
+		   [mkApp(idc,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -152,18 +153,19 @@ let left_instance_tac (inst,id) continue seq=
 	      pf_constr_of_global id (fun idc ->
 		fun gl->
 		  let evmap,rc,ot = mk_open_instance id idc gl m t in
+		  let ot = EConstr.of_constr ot in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
-                  let gt = EConstr.of_constr gt in
 		  let evmap, _ =
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
+              let t = EConstr.of_constr t in
 	      pf_constr_of_global id (fun idc ->
-		Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(idc,[|t|]))]))
+		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
 	  in
 	    tclTHENLIST
 	      [special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 38dae0b20..36bd91ab6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -59,16 +59,17 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)))
+  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
+  let open EConstr in
   tclIFTHENELSE
     (try
       tclTHENLIST
 	[pf_constr_of_global (find_left a seq) (fun left ->
 	  pf_constr_of_global id (fun id -> 
-	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))])));
+	    Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))])));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -95,7 +96,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim));
+      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
        clear_global id;
        tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
@@ -109,12 +110,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))
+  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
 
 (* left arrow connective rules *)
 
@@ -133,7 +134,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
        let head=mkApp ((lift p idc),[|capply|]) in
          EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
        let lp=Array.length rcs in
-       let newhyps idc =List.init lp (myterm idc) in
+       let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
 	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
@@ -142,17 +143,22 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
 	   (wrap lp false continue seq) backtrack gl
 
 let ll_arrow_tac a b c backtrack id continue seq=
+  let open EConstr in
+  let open Vars in
+  let a = EConstr.of_constr a in
+  let b = EConstr.of_constr b in
+  let c = EConstr.of_constr c in
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d idc =EConstr.of_constr (mkLambda (Anonymous,b,
-		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in
+  let d idc = mkLambda (Anonymous,b,
+		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
-      (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c)))
+      (tclTHENS (Proofview.V82.of_tactic (cut c))
 	 [tclTHENLIST
 	    [Proofview.V82.of_tactic introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc)))
-            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)));
+	  tclTHENS (Proofview.V82.of_tactic (cut cc))
+            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
 	     tclTHENLIST
 	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
 		clear_global id;
@@ -177,7 +183,7 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (tclTHENLIST [clear_global id;
                     tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
@@ -191,9 +197,9 @@ let ll_forall_tac prod backtrack id continue seq=
 	  [Proofview.V82.of_tactic intro;
            pf_constr_of_global id (fun idc ->
 	   (fun gls->
+              let open EConstr in
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-              let term = EConstr.of_constr term in
 		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index bffca6223..ec73fccb5 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -616,7 +616,7 @@ let rec fourier () =
                                    (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
                                    (Proofview.tclUNIT ());
 				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
-					  (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq))
+					  (Tacticals.New.tclTHEN (apply symeq)
 						(apply (get coq_Rinv_1))))]
 
 					 )
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7dcfd419e..c80cf4416 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -647,9 +647,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     let sym = build_coq_eq_sym () in
     Tacticals.New.pf_constr_of_global sym (fun sym ->
     Tacticals.New.pf_constr_of_global e (fun e ->
-    let e = EConstr.of_constr e in
     let eq = applist (e, [t1;c1;c2]) in
-    let sym = EConstr.of_constr sym in
     tclTHENLAST
       (replace_core clause l2r eq)
       (tclFIRST
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 89acc149c..9cf3c4187 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -11,6 +11,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Termops
 open Declarations
 open Tacmach
@@ -73,7 +74,7 @@ let nthDecl m gl =
   with Failure _ -> error "No such assumption."
 
 let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
-let nthHyp m gl   = EConstr.mkVar (nthHypId m gl)
+let nthHyp m gl   = mkVar (nthHypId m gl)
 
 let lastDecl gl   = nthDecl 1 gl
 let lastHypId gl  = nthHypId 1 gl
@@ -83,7 +84,7 @@ let nLastDecls n gl =
   try List.firstn n (pf_hyps gl)
   with Failure _ -> error "Not enough hypotheses in the goal."
 
-let nLastHypsId n gl = List.map NamedDecl.get_id (nLastDecls n gl)
+let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl)
 let nLastHyps n gl   = List.map mkVar (nLastHypsId n gl)
 
 let onNthDecl m tac gl  = tac (nthDecl m gl) gl
@@ -147,9 +148,9 @@ let ifOnHyp pred tac1 tac2 id gl =
 
 type branch_args = {
   ity        : pinductive;   (* the type we were eliminating on *)
-  largs      : EConstr.constr list; (* its arguments *)
+  largs      : constr list; (* its arguments *)
   branchnum  : int;         (* the branch number *)
-  pred       : EConstr.constr;      (* the predicate we used *)
+  pred       : constr;      (* the predicate we used *)
   nassums    : int;         (* number of assumptions/letin to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=assumption, false=let-in *)
@@ -226,6 +227,7 @@ let compute_induction_names = compute_induction_names_gen true
 
 (* Compute the let-in signature of case analysis or standard induction scheme *)
 let compute_constructor_signatures isrec ((_,k as ity),u) =
+  let open Term in
   let rec analrec c recargs =
     match kind_of_term c, recargs with
     | Prod (_,_,c), recarg::rest ->
@@ -263,7 +265,7 @@ let pf_with_evars glsev k gls =
     tclTHEN (Refiner.tclEVARS evd) (k a) gls
 
 let pf_constr_of_global gr k =
-  pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k
+  pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
 
 (* computing the case/elim combinators *)
 
@@ -565,7 +567,7 @@ module New = struct
     let gl = Proofview.Goal.assume gl in
     nthDecl m gl |> NamedDecl.get_id
   let nthHyp m gl = 
-    EConstr.mkVar (nthHypId m gl)
+    mkVar (nthHypId m gl)
 
   let onNthHypId m tac =
     Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end }
@@ -657,7 +659,7 @@ module New = struct
     let elimclause' =
       match predicate with
       | None   -> elimclause'
-      | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) p elimclause'
+      | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
     in
     let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
     let after_tac i =
@@ -726,6 +728,7 @@ module New = struct
       let env = Proofview.Goal.env gl in
       let sigma = Tacmach.New.project gl in
       let (sigma, c) = Evd.fresh_global env sigma ref in
+      let c = EConstr.of_constr c in
       Proofview.Unsafe.tclEVARS sigma <*> (tac c)
     end }
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ba5452e33..2b07d937e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -65,14 +65,14 @@ val onLastHypId      : (Id.t -> tactic) -> tactic
 val onLastHyp        : (constr -> tactic) -> tactic
 val onLastDecl       : (Context.Named.Declaration.t -> tactic) -> tactic
 val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
-val onNLastHyps      : int -> (Constr.constr list -> tactic) -> tactic
+val onNLastHyps      : int -> (constr list -> tactic) -> tactic
 val onNLastDecls     : int -> (Context.Named.t -> tactic) -> tactic
 
 val lastHypId   : goal sigma -> Id.t
 val lastHyp     : goal sigma -> constr
 val lastDecl    : goal sigma -> Context.Named.Declaration.t
 val nLastHypsId : int -> goal sigma -> Id.t list
-val nLastHyps   : int -> goal sigma -> Constr.constr list
+val nLastHyps   : int -> goal sigma -> constr list
 val nLastDecls  : int -> goal sigma -> Context.Named.t
 
 val afterHyp    : Id.t -> goal sigma -> Context.Named.t
@@ -135,7 +135,7 @@ val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
 val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
 
 val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
-val pf_constr_of_global : Globnames.global_reference -> (Constr.constr -> tactic) -> tactic
+val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
 
 val elim_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
 val case_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
@@ -267,5 +267,5 @@ module New : sig
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
 
-  val pf_constr_of_global : Globnames.global_reference -> (Constr.constr -> unit Proofview.tactic) -> unit Proofview.tactic
+  val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4dd9eea2..10582288c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4742,7 +4742,7 @@ let symmetry_red allowred =
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
-        (Tacticals.New.pf_constr_of_global eq_data.sym (EConstr.of_constr %> apply))
+        (Tacticals.New.pf_constr_of_global eq_data.sym apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end }
 
@@ -4838,8 +4838,8 @@ let transitivity_red allowred t =
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
         (match t with
-	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans (EConstr.of_constr %> eapply)
-	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [EConstr.of_constr trans;t]))
+	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
+	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
    | None,eq,eq_kind ->
       match t with
       | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")