diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:16 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:16 +0000 |
| commit | 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 (patch) | |
| tree | e7ecad4d80598956e9aeda2f5c82302ab7e0bde8 /kernel/environ.ml | |
| parent | 1d436a18f2f72b57ea09a6d27709a36b63be863a (diff) | |
More monomorphizations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |