fix canonical ff record field attribute

src/coq_elpi_builtins.ml

@@ -923,9 +923,9 @@ It undestands qualified names, e.g. "Nat.t".|})),
      begin match record_info with
      | None -> () (* regular inductive *)
      | Some field_specs -> (* record: projection... *)
-         let names, is_coercion =
-           List.(split (map (fun { name; is_coercion } -> name,
-               { Record.pf_subclass = is_coercion ; pf_canonical = true })
+         let names, flags =
+           List.(split (map (fun { name; is_coercion; is_canonical } -> name,
+               { Record.pf_subclass = is_coercion ; pf_canonical = is_canonical })
              field_specs)) in
          let is_implicit = List.map (fun _ -> []) names in
          let rsp = (mind,0) in
@@ -937,7 +937,7 @@ It undestands qualified names, e.g. "Nat.t".|})),
            Record.declare_projections rsp ~kind:Decls.Definition
              (Evd.univ_entry ~poly:false sigma)
              (Names.Id.of_string "record")
-             is_coercion is_implicit fields_as_relctx
+             flags is_implicit fields_as_relctx
          in
          Record.declare_structure_entry
            (cstr, List.rev kinds, List.rev sp_projs);

theories/tests/test_API.v

@@ -157,20 +157,26 @@ Elpi Query lp:{{
 Check myfalse.
 
 (* record *)
+
 Set Printing Universes.
 Elpi Query lp:{{
   DECL = 
     (parameter `T` {{Type}} t\
        record "eq_class" {{Type}} "mk_eq_class" (
-            field [coercion tt] "eq_f"     {{bool}} f\
-            field _          "eq_proof" {{lp:f = lp:f :> bool}} _\
+            field [canonical ff, coercion tt]     "eq_f"     {{bool}} f\
+            field _ "eq_proof" {{lp:f = lp:f :> bool}} _\
        end-record)),
  coq.say DECL,
  coq.env.add-indt DECL GR.
 }}.
 
 Print eq_class.
 Check (fun x : eq_class nat => (x : bool)).
+Axiom b : bool.
+Axiom p : b = b.
+Canonical xxx := mk_eq_class bool b p.
+Print Canonical Projections.
+Fail Check eq_refl _ : eq_f bool _ = b.
 
 
 (* inductive *)