diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-19 10:15:27 +0100 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-19 10:15:27 +0100 |
| commit | 248d290aa9313501a857a4d3bd9f3d0dc7dc5b4f (patch) | |
| tree | 7a01258f9def516e1c228ca1bd8a5662f057c47c /engine/eConstr.ml | |
| parent | 4d8903c06fd9fd2aca793da8bb55448906347a8c (diff) | |
Define EConstr version of [push_rec_types].
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |