aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorVincent Laporte2019-05-06 15:36:49 +0000
committerVincent Laporte2019-05-10 16:06:10 +0000
commit6e0467e746e40c10bdc110e8d21e26846219d510 (patch)
tree266cbe322995f8157bcd280b7f275f787d6e614a /pretyping
parent4e760a40f22e2d76a3d246b225d290eb5d15e9e8 (diff)
[Canonical structures] “not_canonical” annotation to field declarations
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/recordops.ml3
-rw-r--r--pretyping/recordops.mli2
2 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 331fa2d288..a23c58c062 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -44,9 +44,6 @@ type proj_kind = {
pk_canonical: bool;
}
-let mk_proj_kind pk_name pk_true_proj : proj_kind =
- { pk_name ; pk_true_proj ; pk_canonical = true }
-
type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
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;