diff options
| author | gareuselesinge | 2013-10-31 14:24:43 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-31 14:24:43 +0000 |
| commit | dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e (patch) | |
| tree | f09931dac187ca9b20bb483aee7bc9beca1e78f1 /kernel/pre_env.ml | |
| parent | b0631cba10fda88eb3518153860807b10441ef34 (diff) | |
Conv_orable made functional and part of pre_env
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 9a2bb73d1f..e543c4e687 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -54,6 +54,7 @@ type env = { env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; + env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge } type named_context_val = named_context * named_vals @@ -74,6 +75,7 @@ let empty_env = { env_stratification = { env_universes = initial_universes; env_engagement = None }; + env_conv_oracle = Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge } @@ -118,6 +120,7 @@ let push_named d env = env_rel_val = env.env_rel_val; env_nb_rel = env.env_nb_rel; env_stratification = env.env_stratification; + env_conv_oracle = env.env_conv_oracle; retroknowledge = env.retroknowledge; } let lookup_named_val id env = |