forked from coq/coq
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Extraction to OCaml: use correct key to manage collision of record fi…
…eld names. Fixes coq#3846 Fixes coq#14843 Fixes coq#16677 Fixes coq#12813 When dealing with collisions by means of encapsulation in a Coq_XX module, a field name should be bound to the name of the corresponding inductive type declaration. We use Table.repr_of_r to do that, but early enough to have the relevant information on how to bind a field to the name of the inductive that declares it. (In particular, we cannot rely on the global tables in structures.ml because they are not valid when inside a functor, see coq#17321.) Note that Haskell and Scheme do not use records and it is ok on their side.
- Loading branch information
Showing
6 changed files
with
47 additions
and
12 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
(* f1 was renamed into Coq__1.f1 but Coq__1 was not defined *) | ||
(* similar to #12813, #16677 *) | ||
|
||
Record r : Type := mk { f1 : unit -> unit; f2: unit -> unit }. | ||
Set Primitive Projections. | ||
Record r' : Type := mk' { f1' : unit -> unit; f2': unit -> unit }. | ||
Unset Primitive Projections. | ||
|
||
Module M. | ||
Definition f1 (ti:unit) : unit := tt. | ||
Definition f2 (ti:unit) : unit := tt. | ||
Definition cf := mk f1 f2. | ||
|
||
Definition f1' (ti:unit) : unit := tt. | ||
Definition f2' (ti:unit) : unit := tt. | ||
Definition cf' := mk' f1' f2'. | ||
End M. | ||
|
||
Require Import Coq.extraction.Extraction. | ||
Recursive Extraction M.cf M.cf'. | ||
Extraction TestCompile M.cf M.cf'. |