aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.ml')
-rw-r--r--proofs/tacmach.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b732e5b9d..aa54e4f9b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -23,6 +23,8 @@ 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; }
(**************************************************************)