From 248d290aa9313501a857a4d3bd9f3d0dc7dc5b4f Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Fri, 19 Jan 2018 10:15:27 +0100
Subject: Define EConstr version of [push_rec_types].

---
 engine/eConstr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 30de748a19..6fa338c73d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -251,6 +251,7 @@ end
 
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
+val push_rec_types : (t, t) Constr.prec_declaration -> env -> env
 
 val push_named : named_declaration -> env -> env
 val push_named_context : named_context -> env -> env
-- 
cgit v1.2.3