diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a6d7ff65b..6d16632cd 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -149,7 +149,6 @@ let lookup_named id env = Sign.lookup_named id env.env_named_context - (* A local const is evaluable if it is defined *) let evaluable_named id env = try @@ -165,6 +164,7 @@ let push_named d env = match body with | None -> ref (VKaxiom id) | Some c -> ref (VKdef(c,env)) + in { env with env_named_context = Sign.add_named_decl d env.env_named_context; |