aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.ml')
-rw-r--r--proofs/tacmach.ml8
1 files changed, 3 insertions, 5 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f3f19e854..7ecf0a9e8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -23,8 +23,6 @@ open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
-let compute env sigma c = EConstr.of_constr (compute env sigma c)
-
let re_sig it gc = { it = it; sigma = gc; }
(**************************************************************)
@@ -229,13 +227,13 @@ module New = struct
let pf_reduce_to_quantified_ind gl t =
pf_apply reduce_to_quantified_ind gl t
- let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t)
+ let pf_hnf_constr gl t = pf_apply hnf_constr gl t
let pf_hnf_type_of gl t =
- EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl 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 t
- let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t)
+ 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