coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ML extraction: annotated functions

From: Éric Tanter <etanter AT dcc.uchile.cl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] ML extraction: annotated functions
Date: Thu, 23 Jul 2015 17:55:59 -0300

[forget about the print_endline example, it is bogus]

the point remains about the “over-polymorphism”, and the mismatch between the
.ml/.mli files that can prevent compilation.

-- Éric

[Coq-Club] ML extraction: annotated functions, Éric Tanter, 07/23/2015
- Re: [Coq-Club] ML extraction: annotated functions, Kenneth Adam Miller, 07/23/2015
- Re: [Coq-Club] ML extraction: annotated functions, Robbert Krebbers, 07/23/2015
  - Re: [Coq-Club] ML extraction: annotated functions, Éric Tanter, 07/23/2015
    - Re: [Coq-Club] ML extraction: annotated functions, Éric Tanter, 07/23/2015
    - Re: [Coq-Club] ML extraction: annotated functions, Robbert Krebbers, 07/23/2015
      - Re: [Coq-Club] ML extraction: annotated functions, Éric Tanter, 07/23/2015
        
        Re: [Coq-Club] ML extraction: annotated functions, Kenneth Adam Miller, 07/23/2015
        
        Re: [Coq-Club] ML extraction: annotated functions, Éric Tanter, 07/23/2015