Removing various compatibility layers of tactics.

5 files changed, 47 insertions, 46 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7269c61e3..e580bccc3 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -133,7 +133,7 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t))
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 (******************************************************************)
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0d65faf12..1ddb67edd 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -27,9 +27,9 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c env evd =
-  if Termops.occur_evar evd evk (EConstr.of_constr c) then
-    Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c);
-  let evd = define evk c evd in
+  if Termops.occur_evar evd evk c then
+    Pretype_errors.error_occur_check env evd evk c;
+  let evd = define evk (EConstr.Unsafe.to_constr c) evd in
   let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
   match
     List.fold_left
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8b890f6f8..59ce8ffa6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -330,7 +330,7 @@ let meta_free_prefix sigma a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then unsafe_type_of env sigma (EConstr.of_constr c)
+  if !check then EConstr.Unsafe.to_constr (unsafe_type_of env sigma (EConstr.of_constr c))
   else EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 3641ad74d..2fab026ea 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -46,11 +46,11 @@ let test_conversion cb env sigma c1 c2 =
   let c2 = EConstr.Unsafe.to_constr c2 in
   test_conversion cb env sigma c1 c2
 
-let pf_concl gls = EConstr.Unsafe.to_constr (Goal.V82.concl (project gls) (sig_it gls))
+let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
   List.map (function LocalAssum (id,x)
-                   | LocalDef (id,_,x) -> id, x)
+                   | LocalDef (id,_,x) -> id, EConstr.of_constr x)
            sign
 
 let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
@@ -64,7 +64,7 @@ let pf_get_hyp gls id =
     raise (RefinerError (NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  id |> pf_get_hyp gls |> NamedDecl.get_type
+  id |> pf_get_hyp gls |> NamedDecl.get_type |> EConstr.of_constr
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -77,7 +77,7 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
+let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -103,7 +103,7 @@ let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
 let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
-let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
+let pf_const_value              = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))
 
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
@@ -173,7 +173,7 @@ module New = struct
     (** We only check for the existence of an [id] in [hyps] *)
     let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
-    Constrintern.construct_reference hyps id
+    EConstr.of_constr (Constrintern.construct_reference hyps id)
 
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
@@ -205,13 +205,13 @@ module New = struct
     sign
 
   let pf_get_hyp_typ id gl =
-    pf_get_hyp id gl |> NamedDecl.get_type
+    pf_get_hyp id gl |> NamedDecl.get_type |> EConstr.of_constr
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in
     let sign = Environ.named_context env in
     List.map (function LocalAssum (id,x)
-                     | LocalDef (id,_,x) -> id, x)
+                     | LocalDef (id,_,x) -> id, EConstr.of_constr x)
              sign
 
   let pf_last_hyp gl =
@@ -241,6 +241,6 @@ module New = struct
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
-  let pf_nf_evar gl t = nf_evar (project gl) t
+  let pf_nf_evar gl t = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t))
 
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f0471bf66..efc3dbf55 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Environ
+open EConstr
 open Evd
 open Proof_type
 open Redexpr
@@ -40,9 +41,9 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
-val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * EConstr.types
-val pf_hnf_type_of        : goal sigma -> EConstr.constr -> EConstr.types
+val pf_unsafe_type_of            : goal sigma -> constr -> types
+val pf_type_of            : goal sigma -> constr -> evar_map * types
+val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
@@ -50,7 +51,7 @@ val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
 val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -63,35 +64,35 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_all       : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_hnf_constr              : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_nf                      : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_nf_betaiota             : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types
-val pf_reduce_to_atomic_ind     : goal sigma -> EConstr.types -> pinductive * EConstr.types
-val pf_compute                 : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_whd_all       : goal sigma -> constr -> constr
+val pf_hnf_constr              : goal sigma -> constr -> constr
+val pf_nf                      : goal sigma -> constr -> constr
+val pf_nf_betaiota             : goal sigma -> constr -> constr
+val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> pinductive * types
+val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> EConstr.constr -> EConstr.constr
+  -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> pconstant -> constr
-val pf_conv_x      : goal sigma -> EConstr.constr -> EConstr.constr -> bool
-val pf_conv_x_leq  : goal sigma -> EConstr.constr -> EConstr.constr -> bool
+val pf_conv_x      : goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool
+val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
+val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
-val internal_cut_no_check     : bool -> Id.t -> EConstr.types -> tactic
-val refine_no_check           : EConstr.constr -> tactic
+val internal_cut_no_check     : bool -> Id.t -> types -> tactic
+val refine_no_check           : constr -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
-val internal_cut     : bool -> Id.t -> EConstr.types -> tactic
-val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic
-val refine           : EConstr.constr -> tactic
+val internal_cut     : bool -> Id.t -> types -> tactic
+val internal_cut_rev : bool -> Id.t -> types -> tactic
+val refine           : constr -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
@@ -106,11 +107,11 @@ module New : sig
 
   val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
-  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types
+  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * EConstr.types
-  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
+  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types
+  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool
 
   val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
   val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
@@ -120,16 +121,16 @@ module New : sig
   val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
   val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
 
-  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types
+  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
 
-  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types
-  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types
+  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
-  val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
 
   val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr