diff options
| author | Matej Kosik | 2016-01-11 12:34:30 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-01-11 12:34:30 +0100 |
| commit | 78bad016e389cd78635d40281bfefd7136733b7e (patch) | |
| tree | 51f90da34d2444734868d7954412ac08ddc0f5c6 /kernel/typeops.ml | |
| parent | f8eb2ed4ddbe2199187696f51c42734014f4d9d0 (diff) | |
| parent | 9d991d36c07efbb6428e277573bd43f6d56788fc (diff) | |
merge
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4f32fdce83..35f53b7e7c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Environ open Entries @@ -99,7 +98,7 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - Context.fold_named_context + Context.Named.fold_outside (fun (id,b1,ty1) () -> try let (_,b2,ty2) = lookup_named id env in @@ -561,6 +560,6 @@ let infer_local_decls env decls = | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, add_rel_decl d l) - | [] -> (env, empty_rel_context) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) in inferec env decls |