diff options
| author | Vincent Laporte | 2019-05-06 14:05:09 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-10 16:06:10 +0000 |
| commit | 4e760a40f22e2d76a3d246b225d290eb5d15e9e8 (patch) | |
| tree | bc38af588c44ae04490a0d4febf17cec79323991 /vernac | |
| parent | 2f2658c5a318fb8a8c00caf4d1aca9fbc2d060d0 (diff) | |
[Canonical structures] Some projections may not be canonical
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 2 | ||||
| -rw-r--r-- | vernac/record.mli | 2 |
2 files changed, 2 insertions, 2 deletions
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 |