Guillaume Melquiond
Guillaume Melquiond
Having `` inside `` led some browsers (e.g., Firefox) to believe that the HTML code was ill-formed. Thus, they inserted `` before ``, causing the logo to be incorrectly pushed...
Consider the following simplified testcase: ``` Kind t type. Type abs t -> t. Theorem foo : forall (T : t -> t) U V, T U = T V...
```coq (* coqc -native-compiler yes bar.v *) Fixpoint fact n := match n with S n' => n * fact n' | O => 1 end. Definition large : nat...
The terms are of type `Internal.T env_sym`, so invoking `vm_compute in` on them ends up strongly normalizing the function `env_sym`, which explodes. By using `eval vm_compute` instead, only the bodies...
These evaluations do not produce anything interesting, since the called function is just a wrapper around a function created by `Function the_loop. Admitted.` and therefore opaque. This is related to...
Especially for symbols defined inside sections, callee functions might be invoked with the exact same arguments as caller functions. A similar situation happens with recursive functions that share most of...
The compression scheme is quite naive. It is based on the observation that, in most cases, a bytecode word is a small byte followed by three nul bytes. In that...
When closures are nested inside closures, it might happen that several consecutive values from the environment of the outer closure are pushed onto the stack in order to create the...
I have been trying to generate a logarithm function using `generic_log.py` and the result seems suboptimal. Looking at the generator, there are a few things that confuse me. 1. The...
In particular, these tactics can now be used with a symbol that has some implicit arguments. Fixes / closes #18177 - [X] Added / updated **test-suite**. - [X] Added **changelog**....