Pierre Rousselin
Pierre Rousselin
While trying out jscoq on the web server of my laboratory, I had a MIME type problem with `node_modules/coq-js/jscoq_worker.bc.cjs` Renaming it `node_modules/coq-js/jscoq_worker.bc.js` and changing accordingly the file name in `node_modules/ui-js/jscoq-worker-interface.js`...
DO NOTE MERGE: Waiting to be rebased on Coq/Coq#19144 once/if it is merged. Removing "Include Type" which was deprecated since 8.3. "Include" now supports "Include type
Added: - `strong_induction_le` in NOrder (not sure about this one) - `Even_Odd_induction` in NBits (not sure about capitalization) - `land_(even|odd)_(even|odd)`, `land_le_[lr]` - `ldiff_(even|odd)_(even|odd)`, `ldiff_le_l` - `le_div2_diag_l` - `le_shiftl` and `shiftr_le`...
- A COQBIN variable, if set and non-null is prepended to the PATH in `configure.ac`. The variables COQC, COQDOC and COQTOP now contain an absolute path. - I have also...
It's more or less standard that the `COQBIN` environment variable sets the directory where `coq` executables are to be found (this is especially convenient with a dev build). This should...
In [this (great) tutorial](https://ocaml.org/docs/basic-data-types#user-defined-types), the link just before the "Record" part is broken: [another tutorial](https://ocaml.org/docs/docs/labels#more-variants-polymorphic-variants) gives a 404.
Rendered: https://github.com/Villetaneuse/ceps/blob/clean_up_Reals/text/000-clean-up-Reals.md
We add two axioms in NatInt to restrict the models to exactly the integers and the natural numbers (with `pred 0 = 0`). This allows us to prove lemmas such...
This makes it possible e.g. to ```coq Search (nat -> nat -> nat) [is:Fixpoint | is:Definition]. ``` - [x] Added / updated **test-suite**. - [x] Added **changelog**. - [x] Added...
Search categories for constants with opaque (lemmas, etc) and transparent (definition, ...) bodies
### Is your feature request related to a problem? It should be possible to search for - "logical" constants (`Lemma`s, `Theorems`, ...) - "definitional" constants (`Definition`s, `Fixpoint`s, ...) without knowing...