From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- proofs/tacmach.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/tacmach.mli') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 727efcf6d..16f6f88c1 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -110,7 +110,7 @@ module New : sig 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_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool + 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 val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list @@ -126,8 +126,8 @@ module New : sig 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 -> constr -> constr - val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr + 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 -- cgit v1.2.3