diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-29 16:02:46 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-29 16:02:46 +0000 |
| commit | 943e6b23229b5eed2fb8265089563ce0a25b9b44 (patch) | |
| tree | 803aa037f3413c21e76650c62e7ea9173ba3c918 /kernel/cooking.ml | |
| parent | 4490dfcb94057dd6518963a904565e3a4a354bac (diff) | |
Merging Context and Sign.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0851f682d..bb29b9645 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -18,7 +18,6 @@ open Util open Names open Term open Context -open Sign open Declarations open Environ @@ -124,7 +123,7 @@ type inline = bool type result = constant_def * constant_type * Univ.constraints * inline - * Sign.section_context option + * Context.section_context option let on_body f = function | Undef inl -> Undef inl @@ -139,13 +138,13 @@ let constr_of_def = function let cook_constant env r = let cb = r.d_from in - let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in + let hyps = Context.map_named_context (expmod_constr r.d_modlist) r.d_abstract in let body = on_body (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps) cb.const_body in let const_hyps = - Sign.fold_named_context (fun (h,_,_) hyps -> + Context.fold_named_context (fun (h,_,_) hyps -> List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with |