diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index a65b3941ef..b95068ebf4 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -695,6 +697,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 +823,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 |