Tacmach API using EConstr.

4 files changed, 49 insertions, 49 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index bc5f17bf5e..5b9322bfec 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -95,7 +95,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS (Evd.clear_metas evd'))
-    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+    (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
   end
 
 open Unification
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c5d6e3e083..829c962962 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -490,6 +490,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
   let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+  let ct = EConstr.of_constr ct in
   let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
   let indspec =
     try Tacred.find_hnf_rectype env sigma ct
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c2ebb76d7a..b732e5b9d9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -77,37 +77,36 @@ let pf_global gls id = 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
   let sigma = Sigma.Unsafe.of_evar_map (project gls) in
-  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in
+  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
   (Sigma.to_evar_map sigma, c)
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
   on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
-let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c)
 let pf_e_reduce = pf_apply
 
-let pf_whd_all         = pf_reduce' whd_all
-let pf_hnf_constr                = pf_reduce' hnf_constr
-let pf_nf                        = pf_reduce' simpl
-let pf_nf_betaiota               = pf_reduce' (fun _ -> nf_betaiota)
-let pf_compute                   = pf_reduce' compute
-let pf_unfoldn ubinds            = pf_reduce' (unfoldn ubinds)
-let pf_unsafe_type_of            = pf_reduce' unsafe_type_of
-let pf_type_of                   = pf_reduce' type_of
+let pf_whd_all         = pf_reduce whd_all
+let pf_hnf_constr                = pf_reduce hnf_constr
+let pf_nf                        = pf_reduce simpl
+let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
+let pf_compute                   = pf_reduce compute
+let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_unsafe_type_of            = pf_reduce unsafe_type_of
+let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
-let pf_conv_x gl                = pf_apply test_conversion gl Reduction.CONV
+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_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls
+let pf_hnf_type_of gls          = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls
 
-let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c)
-let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c)
+let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
+let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -116,12 +115,15 @@ let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p (EC
 let refiner = refiner
 
 let internal_cut_no_check replace id t gl =
+  let t = EConstr.Unsafe.to_constr t in
   refiner (Cut (true,replace,id,t)) gl
 
 let internal_cut_rev_no_check replace id t gl =
+  let t = EConstr.Unsafe.to_constr t in
   refiner (Cut (false,replace,id,t)) gl
 
 let refine_no_check c gl =
+  let c = EConstr.Unsafe.to_constr c in
   refiner (Refine c) gl
 
 (* Versions with consistency checks *)
@@ -159,9 +161,6 @@ module New = struct
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (project gl)
 
-  let pf_reduce f gl c =
-    f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c)
-
   let of_old f gl =
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
@@ -175,10 +174,10 @@ module New = struct
   let pf_concl = Proofview.Goal.concl
 
   let pf_unsafe_type_of gl t =
-    pf_apply unsafe_type_of gl (EConstr.of_constr t)
+    pf_apply unsafe_type_of gl t
 
   let pf_type_of gl t =
-    pf_apply type_of gl (EConstr.of_constr t)
+    pf_apply type_of gl t
 
   let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
@@ -221,18 +220,18 @@ module New = struct
     let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_all gl t = pf_reduce whd_all gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = pf_reduce hnf_constr gl t
+  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t))
+    pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t)
+  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 16f6f88c17..07d02212ca 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -40,9 +40,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 -> constr -> types
-val pf_type_of            : goal sigma -> constr -> evar_map * types
-val pf_hnf_type_of        : goal sigma -> constr -> types
+val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
+val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * types
+val pf_hnf_type_of        : goal sigma -> EConstr.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 +50,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 -> constr -> evar_map * constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -63,35 +63,35 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * 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_whd_all       : goal sigma -> EConstr.constr -> constr
+val pf_hnf_constr              : goal sigma -> EConstr.constr -> constr
+val pf_nf                      : goal sigma -> EConstr.constr -> constr
+val pf_nf_betaiota             : goal sigma -> EConstr.constr -> constr
+val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> EConstr.types -> pinductive * types
+val pf_compute                 : goal sigma -> EConstr.constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> constr -> constr
+  -> goal sigma -> EConstr.constr -> constr
 
 val pf_const_value : goal sigma -> pconstant -> constr
 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 -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
+val pf_matches     : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map
+val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool
 
 
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
-val internal_cut_no_check     : bool -> Id.t -> types -> tactic
-val refine_no_check           : constr -> tactic
+val internal_cut_no_check     : bool -> Id.t -> EConstr.types -> tactic
+val refine_no_check           : EConstr.constr -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
-val internal_cut     : bool -> Id.t -> types -> tactic
-val internal_cut_rev : bool -> Id.t -> types -> tactic
-val refine           : constr -> tactic
+val internal_cut     : bool -> Id.t -> EConstr.types -> tactic
+val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic
+val refine           : EConstr.constr -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
@@ -108,8 +108,8 @@ module New : sig
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
   val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.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 * Term.types
   val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
 
   val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
@@ -121,15 +121,15 @@ module New : sig
   val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
 
   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_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * 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_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
 
   val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
   val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
 
-  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map
 
   val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr