package coq-core

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i*)
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
(*i*)

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])) ()

(* short names without opening all Hints *)
type locality = Hints.hint_locality = Local | Export | SuperGlobal

type instance = {
  class_name : GlobRef.t;
  instance : GlobRef.t;
  info : Typeclasses.hint_info;
  (* Sections where the instance should be redeclared,
     None for discard, Some 0 for none. *)
  locality : Hints.hint_locality;
}

let add_instance_base inst =
  let locality = match inst.locality with
  | Local -> Local
  | SuperGlobal ->
    (* i.e. in a section, declare the hint as local since discharge is managed
       by rebuild_instance which calls again add_instance_hint; don't ask hints
       to take discharge into account itself *)
    if Lib.sections_are_opened () then Local
    else SuperGlobal
  | Export ->
    (* Same as above for export *)
    if Lib.sections_are_opened () then Local
    else Export
  in
  add_instance_hint inst.instance ~locality
    inst.info

(*
 * instances persistent object
 *)
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)

(*
 * classes persistent object
 *)

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 -> (* not defined in the current section *)
    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.")

(* Declare everything in the parameters as implicit, and the class instance as well *)

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 =
  (* spiwack: it is hard to reorder the actions to do
     the pretyping after the proof has opened. As a
     consequence, we use the low-level primitives to code
     the refinement manually.*)
  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
  (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
     This is due to a bug in proof_global :( *)
  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
  (* spiwack: I don't know what to do with the status here. *)
  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
  (* Try resolving fields that are typeclasses automatically. *)
  let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
  let sigma = Evarutil.nf_evar_map_undefined sigma in
  (* Beware of this step, it is required as to minimize universes. *)
  let sigma = Evd.minimize_universes sigma in
  (* Check that the type is free of evars now. *)
  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
  (* The name generator should not be here *)
  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
OCaml

Innovation. Community. Security.