← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to checker/environ.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
checker/environ.ml
111
111
  Cmap_env.find kn env.env_globals.env_constants
112
112
 
113
113
let add_constant kn cs env =
 
114
  if Cmap_env.mem kn env.env_globals.env_constants then
 
115
    Printf.ksprintf anomaly "Constant %s is already defined"
 
116
      (string_of_con kn);
114
117
  let new_constants =
115
118
    Cmap_env.add kn cs env.env_globals.env_constants in
116
119
  let new_globals =
159
162
  Mindmap_env.find kn env.env_globals.env_inductives
160
163
 
161
164
let add_mind kn mib env =
 
165
  if Mindmap_env.mem kn env.env_globals.env_inductives then
 
166
    Printf.ksprintf anomaly "Inductive %s is already defined"
 
167
      (string_of_mind kn);
162
168
  let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
163
169
  let kn1,kn2 =  user_mind kn,canonical_mind kn in
164
170
  let new_inds_eq = if kn1=kn2 then 
175
181
(* Modules *)
176
182
 
177
183
let add_modtype ln mtb env =
 
184
  if MPmap.mem ln env.env_globals.env_modtypes then
 
185
    Printf.ksprintf anomaly "Module type %s is already defined"
 
186
      (string_of_mp ln);
178
187
  let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
179
188
  let new_globals =
180
189
    { env.env_globals with
182
191
  { env with env_globals = new_globals }
183
192
 
184
193
let shallow_add_module mp mb env =
 
194
  if MPmap.mem mp env.env_globals.env_modules then
 
195
    Printf.ksprintf anomaly "Module %s is already defined"
 
196
      (string_of_mp mp);
185
197
  let new_mods = MPmap.add mp mb env.env_globals.env_modules in
186
198
  let new_globals =
187
199
    { env.env_globals with
188
200
        env_modules = new_mods } in
189
201
  { env with env_globals = new_globals }
190
202
 
 
203
let shallow_remove_module mp env =
 
204
  if not (MPmap.mem mp env.env_globals.env_modules) then
 
205
    Printf.ksprintf anomaly "Module %s is unknown"
 
206
      (string_of_mp mp);
 
207
  let new_mods = MPmap.remove mp env.env_globals.env_modules in
 
208
  let new_globals =
 
209
    { env.env_globals with
 
210
        env_modules = new_mods } in
 
211
  { env with env_globals = new_globals }
191
212
 
192
213
let lookup_module mp env =
193
214
  MPmap.find mp env.env_globals.env_modules