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 +++++ 1 file changed, 5 insertions(+) (limited to 'engine/eConstr.ml') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index a65b3941e..9ac16b5b4 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 -- cgit v1.2.3