Add "compare" function and got error message

[XuJiandong]

I just append a function "compare" to one of the module:

let compare _ _ = 0 (* implementation removed*)

In order to support Map, Something like this:

module PathMap = Map.Make(Path)

But got error message below. Is there any more explanation or solution to this?

  38 |   | Tunivar of string option
  39 |   | Tpoly of type_expr * type_expr list
> 40 |   | Tpackage of Path.t * Longident.t list * type_expr list
  41 | 
  42 | and row_desc =
  43 |     { row_fields: (label * row_field) list;


It is unclear which name this signature has. At least two similar
signatures found, namely:

* Stdlib__map.OrderedType
* Stdlib__set.OrderedType

We were looking for a module signature name for the following shape:
[ compare ]
(a shape is a list of names of values and sub-modules)

We use the concept of shape to find the name of a signature for Coq.

[clarus]

Yes, the two signatures Stdlib__map.OrderedType and Stdlib__set.OrderedType are actually the same, so coq-of-ocaml gets confused. I think this error is fine then because both choices are the same.

[clarus]

By the way, does the generated code for this example looks fine?

[XuJiandong]

yes, the content seems OK. But when "set" is not used, it still generate errors:

 $ cat main.ml 

(*open Path*)

module PathMap = Map.Make(Path)

 $ cat path.ml
type t = int

let compare _ _ = 0

 $ cat Main.v 
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Definition PathMap := Stdlib.Map.Make (existT (A := Set) _ _ (|Test123.Path|)).

[clarus]

What if you add a dummy definition to 'path.ml', and recompile everything?

[clarus]

Like 'let dummy = ()'

[XuJiandong]

Definition dummy : unit := tt.

is generated, and still get error from 'coq-of-ocaml main.ml'

[clarus]

What do you get for 'main.ml' then? The hope is to change the interface of 'path.ml' so that it doesn't think it is a record but a plain module.