From c72bf7330bb32970616be4dddc7571f3b91c1562 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 20 Nov 2016 01:08:53 +0100
Subject: Eqdecide API using EConstr.

---
 proofs/tacmach.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/tacmach.ml')

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; }
 
 (**************************************************************)
-- 
cgit v1.2.3