diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 301c3b152..20436cbe7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -49,8 +49,9 @@ let named_context_val env = env.env_named_context,env.env_named_vals let rel_context env = env.env_rel_context let empty_context env = - env.env_rel_context = empty_rel_context - && env.env_named_context = empty_named_context + match env.env_rel_context, env.env_named_context with + | [], [] -> true + | _ -> false (* Rel context *) let lookup_rel n env = @@ -321,7 +322,7 @@ let apply_to_hyp (ctxt,vals) id f = let rec aux rtail ctxt vals = match ctxt, vals with | (idc,c,ct as d)::ctxt, v::vals -> - if idc = id then + if id_eq idc id then (f ctxt d rtail)::ctxt, v::vals else let ctxt',vals' = aux (d::rtail) ctxt vals in @@ -334,7 +335,7 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = let rec aux ctxt vals = match ctxt,vals with | (idc,c,ct as d)::ctxt, v::vals -> - if idc = id then + if id_eq idc id then let sign = ctxt,vals in push_named_context_val (f d sign) sign else @@ -348,7 +349,7 @@ let insert_after_hyp (ctxt,vals) id d check = let rec aux ctxt vals = match ctxt, vals with | (idc,c,ct)::ctxt', v::vals' -> - if idc = id then begin + if id_eq idc id then begin check ctxt; push_named_context_val d (ctxt,vals) end else |