aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/declare.ml
blob: 72cdabfd20a702d3396a2c8b716b7dbf99d76de3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** This module is about the low-level declaration of logical objects *)

open Pp
open CErrors
open Util
open Names
open Libnames
open Globnames
open Constr
open Declarations
open Entries
open Libobject
open Lib
open Impargs
open Safe_typing
open Cooking
open Decls
open Decl_kinds

(** flag for internal message display *)
type internal_flag =
  | UserAutomaticRequest (* kernel action, a message is displayed *)
  | InternalTacticRequest  (* kernel action, no message is displayed *)
  | UserIndividualRequest   (* user action, a message is displayed *)

(** Declaration of constants and parameters *)

type constant_obj = {
  cst_decl : global_declaration option;
  (** [None] when the declaration is a side-effect and has already been defined
      in the global environment. *)
  cst_hyps : Dischargedhypsmap.discharged_hyps;
  cst_kind : logical_kind;
  cst_locl : bool;
}

type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind

(* At load-time, the segment starting from the module name to the discharge *)
(* section (if Remark or Fact) is needed to access a construction *)
let load_constant i ((sp,kn), obj) =
  if Nametab.exists_cci sp then
    alreadydeclared (Id.print (basename sp) ++ str " already exists");
  let con = Global.constant_of_delta_kn kn in
  Nametab.push (Nametab.Until i) sp (ConstRef con);
  add_constant_kind con obj.cst_kind

(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn), obj) =
  (** Never open a local definition *)
  if obj.cst_locl then ()
  else
    let con = Global.constant_of_delta_kn kn in
    Nametab.push (Nametab.Exactly i) sp (ConstRef con);
    match (Global.lookup_constant con).const_body with
    | (Def _ | Undef _) -> ()
    | OpaqueDef lc ->
        match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with
        | Some f when Future.is_val f ->
	   Global.push_context_set false (Future.force f)
        | _ -> ()

let exists_name id =
  variable_exists id || Global.exists_objlabel (Label.of_id id)

let check_exists sp =
  let id = basename sp in
  if exists_name id then alreadydeclared (Id.print id ++ str " already exists")

let cache_constant ((sp,kn), obj) =
  let id = basename sp in
  let _,dir,_ = KerName.repr kn in
  let kn' =
    match obj.cst_decl with
    | None ->
      if Global.exists_objlabel (Label.of_id (basename sp))
      then Constant.make1 kn
      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
    | Some decl ->
      let () = check_exists sp in
      Global.add_constant dir id decl
  in
  assert (Constant.equal kn' (Constant.make1 kn));
  Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
  let cst = Global.lookup_constant kn' in
  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
  Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
  add_constant_kind (Constant.make1 kn) obj.cst_kind

let discharged_hyps kn sechyps =
  let (_,dir,_) = KerName.repr kn in
  let args = Array.to_list (instance_from_variable_context sechyps) in
  List.rev_map (Libnames.make_path dir) args

let discharge_constant ((sp, kn), obj) =
  let con = Constant.make1 kn in
  let from = Global.lookup_constant con in
  let modlist = replacement_context () in
  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
  let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
  let abstract = (named_of_variable_context hyps, subst, uctx) in
  let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
  Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; }

(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_constant cst = {
  cst_decl = None;
  cst_hyps = [];
  cst_kind = cst.cst_kind;
  cst_locl = cst.cst_locl;
}

let classify_constant cst = Substitute (dummy_constant cst)

let (inConstant : constant_obj -> obj) =
  declare_object { (default_object "CONSTANT") with
    cache_function = cache_constant;
    load_function = load_constant;
    open_function = open_constant;
    classify_function = classify_constant;
    subst_function = ident_subst_function;
    discharge_function = discharge_constant }

let declare_scheme = ref (fun _ _ -> assert false)
let set_declare_scheme f = declare_scheme := f

let update_tables c =
  declare_constant_implicits c;
  Heads.declare_head (EvalConstRef c);
  Notation.declare_ref_arguments_scope (ConstRef c)

let register_side_effect (c, role) =
  let o = inConstant {
    cst_decl = None;
    cst_hyps = [] ;
    cst_kind = IsProof Theorem;
    cst_locl = false;
  } in
  let id = Label.to_id (pi3 (Constant.repr3 c)) in
  ignore(add_leaf id o);
  update_tables c;
  match role with
  | Safe_typing.Subproof -> ()
  | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]

let declare_constant_common id cst =
  let o = inConstant cst in
  let _, kn as oname = add_leaf id o in
  pull_to_head oname;
  let c = Global.constant_of_delta_kn kn in
  update_tables c;
  c

let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
    ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
    const_entry_secctx = None;
    const_entry_type = types;
    const_entry_universes = univs;
    const_entry_opaque = opaque;
    const_entry_feedback = None;
    const_entry_inline_code = inline}

let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
  let is_poly de = match de.const_entry_universes with
  | Monomorphic_const_entry _ -> false
  | Polymorphic_const_entry _ -> true
  in
  let in_section = Lib.sections_are_opened () in
  let export, decl = (* We deal with side effects *)
    match cd with
    | DefinitionEntry de when
        export_seff ||
        not de.const_entry_opaque ||
        is_poly de ->
      (** This globally defines the side-effects in the environment. We mark
          exported constants as being side-effect not to redeclare them at
          caching time. *)
      let de, export = Global.export_private_constants ~in_section de in
      export, ConstantEntry (PureEntry, DefinitionEntry de)
    | _ -> [], ConstantEntry (EffectEntry, cd)
  in
  let () = List.iter register_side_effect export in
  let cst = {
    cst_decl = Some decl;
    cst_hyps = [] ;
    cst_kind = kind;
    cst_locl = local;
  } in
  declare_constant_common id cst

let declare_definition ?(internal=UserIndividualRequest)
  ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
  id ?types (body,univs) =
  let cb =
    definition_entry ?types ~univs ~opaque body
  in
    declare_constant ~internal ~local id
      (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)

(** Declaration of section variables and local definitions *)

type section_variable_entry =
  | SectionLocalDef of Safe_typing.private_constants definition_entry
  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)

type variable_declaration = DirPath.t * section_variable_entry * logical_kind

let cache_variable ((sp,_),o) =
  match o with
  | Inl ctx -> Global.push_context_set false ctx
  | Inr (id,(p,d,mk)) ->
  (* Constr raisonne sur les noms courts *)
  if variable_exists id then
    alreadydeclared (Id.print id ++ str " already exists");

  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
    | SectionLocalAssum ((ty,ctx),poly,impl) ->
      let () = Global.push_named_assum ((id,ty,poly),ctx) in
      let impl = if impl then Implicit else Explicit in
        impl, true, poly, ctx
    | SectionLocalDef (de) ->
      let (de, eff) = Global.export_private_constants ~in_section:true de in
      let () = List.iter register_side_effect eff in
      (** The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
      let (body, uctx), () = Future.force de.const_entry_body in
      let poly, univs = match de.const_entry_universes with
      | Monomorphic_const_entry uctx -> false, uctx
      | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
      in
      let univs = Univ.ContextSet.union uctx univs in
      (** We must declare the universe constraints before type-checking the
          term. *)
      let () = Global.push_context_set (not poly) univs in
      let se = {
        secdef_body = body;
        secdef_secctx = de.const_entry_secctx;
        secdef_feedback = de.const_entry_feedback;
        secdef_type = de.const_entry_type;
      } in
      let () = Global.push_named_def (id, se) in
      Explicit, de.const_entry_opaque,
      poly, univs in
  Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
  add_section_variable id impl poly ctx;
  Dischargedhypsmap.set_discharged_hyps sp [];
  add_variable_data id (p,opaq,ctx,poly,mk)

let discharge_variable (_,o) = match o with
  | Inr (id,_) ->
    if variable_polymorphic id then None
    else Some (Inl (variable_context id))
  | Inl _ -> Some o

type variable_obj =
    (Univ.ContextSet.t, Id.t * variable_declaration) union

let inVariable : variable_obj -> obj =
  declare_object { (default_object "VARIABLE") with
    cache_function = cache_variable;
    discharge_function = discharge_variable;
    classify_function = (fun _ -> Dispose) }

(* for initial declaration *)
let declare_variable id obj =
  let oname = add_leaf id (inVariable (Inr (id,obj))) in
  declare_var_implicits id;
  Notation.declare_ref_arguments_scope (VarRef id);
  Heads.declare_head (EvalVarRef id);
  oname

(** Declaration of inductive blocks *)

let declare_inductive_argument_scopes kn mie =
  List.iteri (fun i {mind_entry_consnames=lc} ->
    Notation.declare_ref_arguments_scope (IndRef (kn,i));
    for j=1 to List.length lc do
      Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
    done) mie.mind_entry_inds

let inductive_names sp kn mie =
  let (dp,_) = repr_path sp in
  let kn = Global.mind_of_delta_kn kn in
  let names, _ =
    List.fold_left
      (fun (names, n) ind ->
	 let ind_p = (kn,n) in
	 let names, _ =
	   List.fold_left
	     (fun (names, p) l ->
		let sp =
		  Libnames.make_path dp l
		in
		  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
	     (names, 1) ind.mind_entry_consnames in
	 let sp = Libnames.make_path dp ind.mind_entry_typename
	 in
	   ((sp, IndRef ind_p) :: names, n+1))
      ([], 0) mie.mind_entry_inds
  in names

let load_inductive i ((sp,kn),(_,mie)) =
  let names = inductive_names sp kn mie in
  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names

let open_inductive i ((sp,kn),(_,mie)) =
  let names = inductive_names sp kn mie in
  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names

let cache_inductive ((sp,kn),(dhyps,mie)) =
  let names = inductive_names sp kn mie in
  List.iter check_exists (List.map fst names);
  let id = basename sp in
  let _,dir,_ = KerName.repr kn in
  let kn' = Global.add_mind dir id mie in
  assert (MutInd.equal kn' (MutInd.make1 kn));
  let mind = Global.lookup_mind kn' in
  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
  Dischargedhypsmap.set_discharged_hyps sp dhyps;
  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names

let discharge_inductive ((sp,kn),(dhyps,mie)) =
  let mind = Global.mind_of_delta_kn kn in
  let mie = Global.lookup_mind mind in
  let repl = replacement_context () in
  let info = section_segment_of_mutual_inductive mind in
  let sechyps = info.Lib.abstr_ctx in
  Some (discharged_hyps kn sechyps,
        Discharge.process_inductive info repl mie)

let dummy_one_inductive_entry mie = {
  mind_entry_typename = mie.mind_entry_typename;
  mind_entry_arity = mkProp;
  mind_entry_template = false;
  mind_entry_consnames = mie.mind_entry_consnames;
  mind_entry_lc = []
}

(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_inductive_entry (_,m) = ([],{
  mind_entry_params = [];
  mind_entry_record = None;
  mind_entry_finite = Declarations.BiFinite;
  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
  mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
  mind_entry_private = None;
})

(* reinfer subtyping constraints for inductive after section is dischared. *)
let infer_inductive_subtyping (pth, mind_ent) =
  match mind_ent.mind_entry_universes with
  | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
    (pth, mind_ent)
  | Cumulative_ind_entry cumi ->
    begin
      let env = Global.env () in
      (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
        (pth, InferCumulativity.infer_inductive env mind_ent)
    end

type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry

let inInductive : inductive_obj -> obj =
  declare_object {(default_object "INDUCTIVE") with
    cache_function = cache_inductive;
    load_function = load_inductive;
    open_function = open_inductive;
    classify_function = (fun a -> Substitute (dummy_inductive_entry a));
    subst_function = ident_subst_function;
    discharge_function = discharge_inductive;
    rebuild_function = infer_inductive_subtyping }

let declare_projections mind =
  let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
    match spec.mind_record with
    | Some (Some (_, kns, pjs)) ->
      Array.iteri (fun i kn ->
	let id = Label.to_id (Constant.label kn) in
	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
	let kn' = declare_constant id (ProjectionEntry entry,
				       IsDefinition StructureComponent)
	in
	  assert(Constant.equal kn kn')) kns; true,true
    | Some None -> true,false
    | None -> false,false

(* for initial declaration *)
let declare_mind mie =
  let id = match mie.mind_entry_inds with
    | ind::_ -> ind.mind_entry_typename
    | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
  let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
  let mind = Global.mind_of_delta_kn kn in
  let isrecord,isprim = declare_projections mind in
  declare_mib_implicits mind;
  declare_inductive_argument_scopes mind mie;
  oname, isprim

(* Declaration messages *)

let pr_rank i = pr_nth (i+1)

let fixpoint_message indexes l =
  Flags.if_verbose Feedback.msg_info (match l with
  | [] -> anomaly (Pp.str "no recursive definition.")
  | [id] -> Id.print id ++ str " is recursively defined" ++
      (match indexes with
	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
	 | _ -> mt ())
  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
		  spc () ++ str "are recursively defined" ++
		  match indexes with
		    | Some a -> spc () ++ str "(decreasing respectively on " ++
			prvect_with_sep pr_comma pr_rank a ++
			str " arguments)"
		    | None -> mt ()))

let cofixpoint_message l =
  Flags.if_verbose Feedback.msg_info (match l with
  | [] -> anomaly (Pp.str "No corecursive definition.")
  | [id] -> Id.print id ++ str " is corecursively defined"
  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
                    spc () ++ str "are corecursively defined"))

let recursive_message isfix i l =
  (if isfix then fixpoint_message i else cofixpoint_message) l

let definition_message id =
  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")

let assumption_message id =
  (* Changing "assumed" to "declared", "assuming" referring more to
  the type of the object than to the name of the object (see
  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")

(** Global universe names, in a different summary *)

type universe_context_decl = polymorphic * Univ.ContextSet.t

let cache_universe_context (p, ctx) =
  Global.push_context_set p ctx;
  if p then Lib.add_section_context ctx

let input_universe_context : universe_context_decl -> Libobject.obj =
  declare_object
    { (default_object "Global universe context state") with
      cache_function = (fun (na, pi) -> cache_universe_context pi);
      load_function = (fun _ (_, pi) -> cache_universe_context pi);
      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
      classify_function = (fun a -> Keep a) }

let declare_universe_context poly ctx =
  Lib.add_anonymous_leaf (input_universe_context (poly, ctx))

(** Global universes are not substitutive objects but global objects
   bound at the *library* or *module* level. The polymorphic flag is
   used to distinguish universes declared in polymorphic sections, which
   are discharged and do not remain in scope. *)

type universe_source =
  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
  | UnqualifiedUniv (* other global universe *)

type universe_decl = universe_source * Nametab.universe_id

let add_universe src (dp, i) =
  let level = Univ.Level.make dp i in
  let optpoly = match src with
    | BoundUniv -> Some true
    | UnqualifiedUniv -> Some false
    | QualifiedUniv _ -> None
  in
  Option.iter (fun poly ->
      let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
      Global.push_context_set poly ctx;
      Universes.add_global_universe level poly;
      if poly then Lib.add_section_context ctx)
    optpoly

let check_exists sp =
  let depth = sections_depth () in
  let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
  if Nametab.exists_universe sp then
    alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
  else ()

let qualify_univ src (sp,i as orig) =
  match src with
  | BoundUniv | UnqualifiedUniv -> orig
  | QualifiedUniv l ->
    let sp0, id = Libnames.repr_path sp in
    let sp0 = DirPath.repr sp0 in
    Libnames.make_path (DirPath.make (l::sp0)) id, i+1

let cache_universe ((sp, _), (src, id)) =
  let sp, i = qualify_univ src (sp,1) in
  let () = check_exists sp in
  let () = Nametab.push_universe (Nametab.Until i) sp id in
    add_universe src id

let load_universe i ((sp, _), (src, id)) =
  let sp, i = qualify_univ src (sp,i) in
  let () = Nametab.push_universe (Nametab.Until i) sp id in
  add_universe src id

let open_universe i ((sp, _), (src, id)) =
  let sp, i = qualify_univ src (sp,i) in
  let () = Nametab.push_universe (Nametab.Exactly i) sp id in
  ()

let discharge_universe = function
  | _, (BoundUniv, _) -> None
  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x

let input_universe : universe_decl -> Libobject.obj =
  declare_object
    { (default_object "Global universe name state") with
      cache_function = cache_universe;
      load_function = load_universe;
      open_function = open_universe;
      discharge_function = discharge_universe;
      subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
      classify_function = (fun a -> Substitute a) }

let declare_univ_binders gr pl =
  if Global.is_polymorphic gr then
    Universes.register_universe_binders gr pl
  else
    let l = match gr with
      | ConstRef c -> Label.to_id @@ Constant.label c
      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
      | VarRef id -> id
      | ConstructRef _ ->
        anomaly ~label:"declare_univ_binders"
          Pp.(str "declare_univ_binders on an constructor reference")
    in
    Id.Map.iter (fun id lvl ->
        match Univ.Level.name lvl with
        | None -> ()
        | Some na ->
          ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
      pl

let do_universe poly l =
  let in_section = Lib.sections_are_opened () in
  let () =
    if poly && not in_section then
      user_err ~hdr:"Constraint"
                   (str"Cannot declare polymorphic universes outside sections")
  in
  let l =
    List.map (fun (l, id) ->
      let lev = Universes.new_univ_id () in
      (id, lev)) l
  in
  let src = if poly then BoundUniv else UnqualifiedUniv in
  List.iter (fun (id,lev) ->
      ignore(Lib.add_leaf id (input_universe (src, lev))))
    l

type constraint_decl = polymorphic * Univ.Constraint.t

let cache_constraints (na, (p, c)) =
  let ctx =
    Univ.ContextSet.add_constraints c
      Univ.ContextSet.empty (* No declared universes here, just constraints *)
  in cache_universe_context (p,ctx)

let discharge_constraints (_, (p, c as a)) =
  if p then None else Some a

let input_constraints : constraint_decl -> Libobject.obj =
  let open Libobject in
    declare_object
    { (default_object "Global universe constraints") with
      cache_function = cache_constraints;
      load_function = (fun _ -> cache_constraints);
      discharge_function = discharge_constraints;
      classify_function = (fun a -> Keep a) }

let loc_of_glob_level = function
  | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n
  | _ -> None

let do_constraint poly l =
  let u_of_id x =
    let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
    let loc = loc_of_glob_level x in
    loc, Universes.is_polymorphic level, level
  in
  let in_section = Lib.sections_are_opened () in
  let () =
    if poly && not in_section then
      user_err ~hdr:"Constraint"
                    (str"Cannot declare polymorphic constraints outside sections")
  in
  let check_poly ?loc p loc' p' =
    if poly then ()
    else if p || p' then
      let loc = if p then loc else loc' in
      user_err ?loc ~hdr:"Constraint"
                    (str "Cannot declare a global constraint on " ++
                    str "a polymorphic universe, use "
                    ++ str "Polymorphic Constraint instead")
  in
  let constraints = List.fold_left (fun acc (l, d, r) ->
     let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in
     check_poly ?loc:ploc p rloc p';
     Univ.Constraint.add (lu, d, ru) acc)
    Univ.Constraint.empty l
  in
    Lib.add_anonymous_leaf (input_constraints (poly, constraints))