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.ml  | 5 +++++
 engine/eConstr.mli | 1 +
 2 files changed, 6 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index a65b3941ef..9ac16b5b48 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -695,6 +695,10 @@ let cast_rel_context :
   type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
   fun Refl x -> x
 
+let cast_rec_decl :
+  type a b. (a,b) eq -> (a, a) Constr.prec_declaration -> (b, b) Constr.prec_declaration =
+  fun Refl x -> x
+
 let cast_named_decl :
   type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
   fun Refl x -> x
@@ -817,6 +821,7 @@ let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d
 
 let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
 let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
+let push_rec_types d e = push_rec_types (cast_rec_decl unsafe_eq d) e
 let push_named d e = push_named (cast_named_decl unsafe_eq d) e
 let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e
 let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e
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