Kenji Maillard comments

Results 11 comments of


                                            Kenji Maillard

Mutually defined functions are hard to get right with equations

Thanks for the hindsight, it indeed works well once there is even just a `by struct` annotation. For the last one, I guess the problem is just that Equations try...

Feature request: simpler syntax when there is no pattern-matching.

It would also make sense and I was thinking that there was an issue tracking that on the Coq tracker, but I don't find it. At the same time, I...

Misleading error message when deriving subterm for Prop-valued inductives

The problem with `t` here is that it is "optimized" by Coq to land in `Prop` so it is expected that we cannot derive Subterm. For reference, it can be...

Unfold equation raise `exception Constr.DestKO` when mixing SProp with wf

might be related to https://github.com/coq/coq/issues/12045

segmentation fault in utop after loading ctypes

Sorry, I forgot to precise that I am using a Gentoo linux with ocaml 4.00.1 installed from the sources. @avsm If by system compiler you mean the ocaml compiler that...

segmentation fault in utop after loading ctypes

Here is the backtrace that I got : ``` Program received signal SIGSEGV, Segmentation fault. 0x08064edc in caml_oldify_one () (gdb) thr apply all bt Thread 3 (Thread 0xb6da9b40 (LWP 3603)):...

Use the script to setup a working environment for the developer, too

and the fonts covering the symbols we need

Variable not found?

Minimizing just a tiny bit nore, the following still fails ``` let rec f x = match x with | Some s -> g s | _ -> () and...

Refactor semantics

Ok for me too

Floating point literals are badly handled by the F# extraction mechanism

Indeed integers are kept as strings but floating point numbers are interpreted directly. We might want to change that.