From 4e760a40f22e2d76a3d246b225d290eb5d15e9e8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 6 May 2019 14:05:09 +0000
Subject: [Canonical structures] Some projections may not be canonical

---
 vernac/record.ml  | 2 +-
 vernac/record.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index f489707eb3..9b0fbea148 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -368,7 +368,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
+      (nfi - 1, i, Recordops.mk_proj_kind fi (is_local_assum decl) :: kinds, sp_projs, subst))
       (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
diff --git a/vernac/record.mli b/vernac/record.mli
index d6e63901cd..51ab7487d7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ val declare_projections :
   bool list ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
-    (Name.t * bool) list * Constant.t option list
+    Recordops.proj_kind list * Constant.t option list
 
 val declare_structure_entry : Recordops.struc_tuple -> unit
 
-- 
cgit v1.2.3