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

---
 pretyping/recordops.mli | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f0594d513a..565454d3b3 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -17,14 +17,22 @@ open Constr
 (** A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
+type proj_kind = {
+  pk_name: Name.t;
+  pk_true_proj: bool;
+  pk_canonical: bool;
+}
+
+val mk_proj_kind : Name.t -> bool -> proj_kind
+
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 val register_structure : Environ.env -> struc_tuple -> unit
 val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
-- 
cgit v1.2.3


From 6e0467e746e40c10bdc110e8d21e26846219d510 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 6 May 2019 15:36:49 +0000
Subject: [Canonical structures] “not_canonical” annotation to field
 declarations

---
 pretyping/recordops.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 565454d3b3..25b6cd0751 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -23,8 +23,6 @@ type proj_kind = {
   pk_canonical: bool;
 }
 
-val mk_proj_kind : Name.t -> bool -> proj_kind
-
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-- 
cgit v1.2.3