diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a543f195..9986f439a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -120,7 +120,7 @@ let lookup_named = lookup_named let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = - c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) @@ -469,9 +469,11 @@ let lookup_modtype mp env = (*s Judgments. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } + +type unsafe_judgment = (constr, types) punsafe_judgment let make_judge v tj = { uj_val = v; @@ -480,10 +482,12 @@ let make_judge v tj = let j_val j = j.uj_val let j_type j = j.uj_type -type unsafe_type_judgment = { - utj_val : constr; +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment + (*s Compilation of global declaration *) let compile_constant_body = Cbytegen.compile_constant_body false |