Source file classes.ml
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
open Names
open EConstr
open CErrors
open Util
open Typeclasses_errors
open Typeclasses
open Libnames
open Globnames
open Constrintern
open Constrexpr
open Context.Rel.Declaration
open Class_tactics
open Libobject
module RelDecl = Context.Rel.Declaration
let set_typeclass_transparency ~locality c b =
Hints.add_hints ~locality [typeclasses_db]
(Hints.HintsTransparencyEntry (Hints.HintsReferences c, b))
let warn_deprecated_tc_transparency_without_locality =
CWarnings.create ~name:"deprecated-typeclasses-transparency-without-locality" ~category:Deprecation.Version.v8_15
Pp.(fun () -> strbrk
"The default value for Typeclasses Opaque and Typeclasses \
Transparent locality is currently \"local\" in a section and \
\"global\" otherwise, but is scheduled to change in a future \
release. For the time being, adding typeclass transparency hints outside of \
sections without specifying an explicit locality attribute is \
therefore deprecated. It is recommended to use \"export\" whenever \
possible. Use the attributes #[local], #[global] and #[export] \
depending on your choice. For example: \"#[export] Typeclasses Transparent foo.\". \
This is supported since Coq 8.15.")
let default_tc_transparency_locality () =
if Lib.sections_are_opened () then Hints.Local
else
let () = warn_deprecated_tc_transparency_without_locality () in
Hints.SuperGlobal
let tc_transparency_locality = Attributes.hint_locality ~default:default_tc_transparency_locality
let set_typeclass_transparency_com ~locality refs b =
let refs = List.map
(fun x -> Tacred.evaluable_of_global_reference
(Global.env ())
(Smartlocate.global_with_alias x))
refs
in
set_typeclass_transparency ~locality refs b
let add_instance_hint gr ~locality info =
let inst = Hints.hint_globref gr in
Flags.silently (fun () ->
Hints.add_hints ~locality [typeclasses_db]
(Hints.HintsResolveEntry
[info, false, inst])) ()
type locality = Hints.hint_locality = Local | Export | SuperGlobal
type instance = {
class_name : GlobRef.t;
instance : GlobRef.t;
info : Typeclasses.hint_info;
locality : Hints.hint_locality;
}
let add_instance_base inst =
let locality = match inst.locality with
| Local -> Local
| SuperGlobal ->
if Lib.sections_are_opened () then Local
else SuperGlobal
| Export ->
if Lib.sections_are_opened () then Local
else Export
in
add_instance_hint inst.instance ~locality
inst.info
let perform_instance i =
let i = { is_class = i.class_name; is_info = i.info; is_impl = i.instance } in
Typeclasses.load_instance i
let cache_instance inst =
perform_instance inst;
add_instance_base inst
let load_instance _ inst = match inst.locality with
| Local -> assert false
| SuperGlobal -> perform_instance inst
| Export -> ()
let open_instance i inst = match inst.locality with
| Local -> assert false
| SuperGlobal -> perform_instance inst
| Export -> if Int.equal i 1 then perform_instance inst
let subst_instance (subst, inst) =
{ inst with
class_name = fst (subst_global subst inst.class_name);
instance = fst (subst_global subst inst.instance) }
let discharge_instance inst =
match inst.locality with
| Local -> None
| SuperGlobal | Export ->
assert (not (isVarRef inst.instance));
Some inst
let classify_instance inst = match inst.locality with
| Local -> Dispose
| SuperGlobal | Export -> Substitute
let instance_input : instance -> obj =
declare_object
{ (default_object "type classes instances state") with
cache_function = cache_instance;
load_function = load_instance;
open_function = simple_open ~cat:Hints.hint_cat open_instance;
classify_function = classify_instance;
discharge_function = discharge_instance;
subst_function = subst_instance }
let default_locality () =
if Lib.sections_are_opened () then Local
else Export
let instance_locality =
Attributes.hint_locality ~default:default_locality
module Event = struct
type t =
| NewClass of typeclass
| NewInstance of instance
end
type observer = string
let observers = ref CString.Map.empty
let active_observers = Summary.ref ~name:"active typeclass observers" []
let register_observer ~name ?(override=false) o =
if not override && CString.Map.mem name !observers then
CErrors.anomaly Pp.(str "Typeclass observer " ++ str name ++ str " already registered.");
observers := CString.Map.add name o !observers;
name
let deactivate_observer name =
active_observers := List.remove String.equal name !active_observers
let activate_observer name =
assert (CString.Map.mem name !observers);
deactivate_observer name;
active_observers := name :: !active_observers
let observe event =
List.iter (fun name -> (CString.Map.get name !observers) event) !active_observers
let add_instance cl info global impl =
let () = match global with
| Local -> ()
| SuperGlobal ->
if Lib.sections_are_opened () && isVarRef impl then
CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable.")
| Export ->
if Lib.sections_are_opened () && isVarRef impl then
CErrors.user_err (Pp.str "The export attribute cannot be applied to an instance referring to a section variable.")
in
let i = {
class_name = cl.cl_impl;
info = info ;
locality = global ;
instance = impl;
} in
Lib.add_leaf (instance_input i);
observe (Event.NewInstance { class_name = cl.cl_impl; instance = impl; info; locality = global })
let warning_not_a_class =
CWarnings.create ~name:"not-a-class" (fun (n, ty) ->
let env = Global.env () in
let evd = Evd.from_env env in
Pp.(str "Ignored instance declaration for “"
++ Nametab.pr_global_env Id.Set.empty n
++ str "”: “"
++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty)
++ str "” is not a class")
)
let declare_instance ?(warn = false) env sigma info local glob =
let ty, _ = Typeops.type_of_global_in_context env glob in
let info = Option.default {hint_priority = None; hint_pattern = None} info in
match class_of_constr env sigma (EConstr.of_constr ty) with
| Some (rels, ((tc,_), args) as _cl) ->
add_instance tc info local glob
| None -> if warn then warning_not_a_class (glob, ty)
let cache_class c = load_class c
let subst_class (subst,cl) =
let do_subst_con c = Mod_subst.subst_constant subst c
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
let do_subst_meth m =
let c = Option.Smart.map do_subst_con m.meth_const in
if c == m.meth_const then m
else
{
meth_name = m.meth_name;
meth_info = m.meth_info;
meth_const = c;
}
in
let do_subst_projs projs = List.Smart.map do_subst_meth projs in
{ cl_univs = cl.cl_univs;
cl_impl = do_subst_gr cl.cl_impl;
cl_context = do_subst_ctx cl.cl_context;
cl_props = do_subst_ctx cl.cl_props;
cl_projs = do_subst_projs cl.cl_projs;
cl_strict = cl.cl_strict;
cl_unique = cl.cl_unique }
let discharge_class cl =
try
let info = Lib.section_segment_of_reference cl.cl_impl in
let info, _, cl_univs' = Cooking.lift_poly_univs info cl.cl_univs in
let nprops = List.length cl.cl_props in
let props, context = List.chop nprops (Discharge.cook_rel_context info (cl.cl_props @ cl.cl_context)) in
let discharge_proj x = x in
{ cl_univs = cl_univs';
cl_impl = cl.cl_impl;
cl_context = context;
cl_props = props;
cl_projs = List.Smart.map discharge_proj cl.cl_projs;
cl_strict = cl.cl_strict;
cl_unique = cl.cl_unique
}
with Not_found ->
cl
let rebuild_class cl =
try
let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
set_typeclass_transparency ~locality:Hints.Local [cst] false; cl
with e when CErrors.noncritical e -> cl
let class_input : typeclass -> obj =
declare_object
{ (default_object "type classes state") with
cache_function = cache_class;
load_function = (fun _ -> cache_class);
classify_function = (fun x -> Substitute);
discharge_function = (fun a -> Some (discharge_class a));
rebuild_function = rebuild_class;
subst_function = subst_class }
let add_class cl =
Lib.add_leaf (class_input cl);
observe (Event.NewClass cl)
let intern_info {hint_priority;hint_pattern} =
let env = Global.env() in
let sigma = Evd.from_env env in
let hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) hint_pattern in
{hint_priority;hint_pattern}
(** TODO: add subinstances *)
let existing_instance ?loc glob c info =
let info = Option.default Hints.empty_hint_info info in
let info = intern_info info in
let env = Global.env() in
let sigma = Evd.from_env env in
let instance, _ = Typeops.type_of_global_in_context env c in
let ctx, r = Term.decompose_prod_decls instance in
match class_of_constr (Environ.push_rel_context ctx env) sigma (EConstr.of_constr r) with
| Some (_, ((tc,u), _)) -> add_instance tc info glob c
| None -> user_err ?loc (Pp.str "Constant does not build instances of a declared type class.")
let type_ctx_instance ~program_mode env sigma ctx inst subst =
let open Vars in
let rec aux (sigma, subst, instctx) l = function
decl :: ctx ->
let t' = substl subst (RelDecl.get_type decl) in
let (sigma, c'), l =
match decl with
| LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l
| LocalDef (_,b,_) -> (sigma, substl subst b), l
in
let d = RelDecl.get_name decl, Some c', t' in
aux (sigma, c' :: subst, d :: instctx) l ctx
| [] -> sigma, subst
in aux (sigma, subst, []) inst (List.rev ctx)
let id_of_class cl =
let open GlobRef in
match cl.cl_impl with
| ConstRef kn -> Label.to_id @@ Constant.label kn
| IndRef (kn,i) ->
let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
mip.(0).Declarations.mind_typename
| _ -> assert false
let instance_hook info global ?hook cst =
let info = intern_info info in
let env = Global.env () in
let sigma = Evd.from_env env in
declare_instance env sigma (Some info) global cst;
(match hook with Some h -> h cst | None -> ())
let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype =
let kind = Decls.(IsDefinition Instance) in
let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) () in
let info = Declare.Info.make ~kind ~poly ~udecl () in
let kn = Declare.declare_definition ~cinfo ~info ~opaque:false ~body:term sigma in
instance_hook iinfo global ?hook kn
let do_declare_instance sigma ~locality ~poly k u ctx ctx' pri udecl impargs subst name =
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst k.cl_context
in
let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let sigma, entry = Declare.prepare_parameter ~poly sigma ~udecl ~types:termtype in
let cst = Declare.declare_constant ~name
~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
let cst = (GlobRef.ConstRef cst) in
Impargs.maybe_declare_manual_implicits false cst impargs;
instance_hook pri locality cst
let declare_instance_program pm env sigma ~locality ~poly name pri impargs udecl term termtype =
let hook { Declare.Hook.S.scope; dref; _ } =
let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
let pri = intern_info pri in
let env = Global.env () in
let sigma = Evd.from_env env in
declare_instance env sigma (Some pri) locality (GlobRef.ConstRef cst)
in
let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
let hook = Declare.Hook.make hook in
let uctx = Evd.evar_universe_context sigma in
let kind = Decls.IsDefinition Decls.Instance in
let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
let info = Declare.Info.make ~udecl ~poly ~kind ~hook () in
let pm, _ =
Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
in pm
let declare_instance_open sigma ?hook ~tac ~locality ~poly id pri impargs udecl ids term termtype =
let future_goals, sigma = Evd.pop_future_goals sigma in
let gls = List.rev (Evd.FutureGoals.comb future_goals) in
let sigma = Evd.push_future_goals sigma in
let kind = Decls.(IsDefinition Instance) in
let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri locality ?hook dref)) in
let info = Declare.Info.make ~hook ~kind ~udecl ~poly () in
let termtype = Evarutil.nf_evar sigma termtype in
let cinfo = Declare.CInfo.make ~name:id ~impargs ~typ:termtype () in
let lemma = Declare.Proof.start ~cinfo ~info sigma in
let lemma =
match term with
| Some term ->
let init_refine =
Tacticals.tclTHENLIST [
Refine.refine ~typecheck:false (fun sigma -> sigma, term);
Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
Tactics.reduce_after_refine;
]
in
let lemma, _ = Declare.Proof.by init_refine lemma in
lemma
| None ->
let lemma, _ = Declare.Proof.by (Tactics.auto_intros_tac ids) lemma in
lemma
in
match tac with
| Some tac ->
let lemma, _ = Declare.Proof.by tac lemma in
lemma
| None ->
lemma
let do_instance_subst_constructor_and_ty subst k u ctx =
let subst =
List.fold_left2 (fun subst' s decl ->
if is_local_assum decl then s :: subst' else subst')
[] subst (k.cl_props @ k.cl_context)
in
let (app, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr ctx in
let term = it_mkLambda_or_LetIn (Option.get app) ctx in
term, termtype
let do_instance_resolve_TC termtype sigma env =
let sigma = Evarutil.nf_evar_map sigma in
let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
let sigma = Evarutil.nf_evar_map_undefined sigma in
let sigma = Evd.minimize_universes sigma in
Pretyping.check_evars env sigma termtype;
termtype, sigma
let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
let props, rest =
List.fold_left
(fun (props, rest) decl ->
if is_local_assum decl then
try
let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
| Name id, {CAst.v=id'} -> Id.equal id id'
| Anonymous, _ -> false
in
let (loc_mid, c) = List.find is_id rest in
let rest' = List.filter (fun v -> not (is_id v)) rest
in
let {CAst.loc;v=mid} = get_id loc_mid in
List.iter (fun m ->
if Name.equal m.meth_name (Name mid) then
Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) m.meth_const) k.cl_projs;
c :: props, rest'
with Not_found ->
((CAst.make @@ CHole (None)) :: props), rest
else props, rest)
([], props) k.cl_props
in
match rest with
| (n, _) :: _ ->
unbound_method env' sigma k.cl_impl (get_id n)
| _ ->
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
let sigma, res =
type_ctx_instance ~program_mode
(push_rel_context ctx' env') sigma kcl_props props subst in
res, sigma
let interp_props ~program_mode env' cty k u ctx ctx' subst sigma = function
| (true, { CAst.v = CRecord fs; loc }) ->
check_duplicate ?loc fs;
let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in
let term, termtype =
do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
term, termtype, sigma
| (_, term) ->
let sigma, def =
interp_casted_constr_evars ~program_mode env' sigma term cty in
let termtype = it_mkProd_or_LetIn cty ctx in
let term = it_mkLambda_or_LetIn def ctx in
term, termtype, sigma
let do_instance_interactive env env' sigma ?hook ~tac ~locality ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
let term, termtype, sigma = match opt_props with
| Some props ->
on_pi1 (fun x -> Some x)
(interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props)
| None ->
let term, termtype =
if List.is_empty k.cl_props then
let term, termtype =
do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
Some term, termtype
else
None, it_mkProd_or_LetIn cty ctx
in
let termtype, sigma = do_instance_resolve_TC termtype sigma env in
term, termtype, sigma
in
Flags.silently (fun () ->
declare_instance_open sigma ?hook ~tac ~locality ~poly
id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
()
let do_instance env env' sigma ?hook ~locality ~poly cty k u ctx ctx' pri decl imps subst id props =
let term, termtype, sigma =
interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props
in
let termtype, sigma = do_instance_resolve_TC termtype sigma env in
Pretyping.check_evars_are_solved ~program_mode:false env sigma;
declare_instance_constant pri locality imps ?hook id decl poly sigma term termtype
let do_instance_program ~pm env env' sigma ?hook ~locality ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
let term, termtype, sigma =
match opt_props with
| Some props ->
interp_props ~program_mode:true env' cty k u ctx ctx' subst sigma props
| None ->
let subst, sigma =
do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in
let term, termtype =
do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
term, termtype, sigma in
let termtype, sigma = do_instance_resolve_TC termtype sigma env in
if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then
let () = declare_instance_constant pri locality imps ?hook id decl poly sigma term termtype in
pm
else
declare_instance_program pm env sigma ~locality ~poly id pri imps decl term termtype
let interp_instance_context ~program_mode env ctx pl tclass =
let sigma, decl = interp_univ_decl_opt env pl in
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let sigma, (c', imps') = interp_type_evars_impls ~flags ~impls env' sigma tclass in
let imps = imps @ imps' in
let ctx', c = decompose_prod_decls sigma c' in
let ctx'' = ctx' @ ctx in
let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
let u_s = EInstance.kind sigma u in
let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
let args = List.map of_constr args in
let cl_context = List.map (Termops.map_rel_decl of_constr) cl.cl_context in
let _, args =
List.fold_right (fun decl (args, args') ->
match decl with
| LocalAssum _ -> (List.tl args, List.hd args :: args')
| LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
cl_context (args, [])
in
let sigma = Evarutil.nf_evar_map sigma in
let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
sigma, cl, u, c', ctx', ctx, imps, args, decl
let new_instance_common ~program_mode env instid ctx cl =
let ({CAst.loc;v=instid}, pl) = instid in
let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
interp_instance_context ~program_mode env ctx pl cl
in
let id =
match instid with
| Name id -> id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
let new_instance_interactive ~locality ~poly instid ctx cl
?(tac:unit Proofview.tactic option) ?hook
pri opt_props =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
new_instance_common ~program_mode:false env instid ctx cl in
id, do_instance_interactive env env' sigma ?hook ~tac ~locality ~poly
cty k u ctx ctx' pri decl imps subst id opt_props
let new_instance_program ~locality ~pm ~poly instid ctx cl opt_props ?hook pri =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
new_instance_common ~program_mode:true env instid ctx cl in
let pm =
do_instance_program ~pm env env' sigma ?hook ~locality ~poly
cty k u ctx ctx' pri decl imps subst id opt_props in
pm, id
let new_instance ~locality ~poly instid ctx cl props ?hook pri =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
new_instance_common ~program_mode:false env instid ctx cl in
do_instance env env' sigma ?hook ~locality ~poly
cty k u ctx ctx' pri decl imps subst id props;
id
let declare_new_instance ~locality ~program_mode ~poly instid ctx cl pri =
let env = Global.env() in
let ({CAst.loc;v=instid}, pl) = instid in
let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
interp_instance_context ~program_mode env ctx pl cl
in
do_declare_instance sigma ~locality ~poly k u ctx ctx' pri decl imps subst instid
let refine_att =
let open Attributes in
let open Notations in
attribute_of_list ["refine",single_key_parser ~name:"refine" ~key:"refine" ()] >>= function
| None -> return false
| Some () -> return true
module Internal = struct
let add_instance = add_instance
end