diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b3a886f711..b3e17fa9d2 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -302,6 +302,10 @@ let next_name_away na avoid = let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in next_ident_away_from id avoid +type ext_named_context = + Vars.substl * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open Context.Named.Declaration in let replace_var_named_declaration id0 id decl = |