aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #6657: Document the Fail commandGravatar Maxime Dénès2018-02-07
|\
* \ Merge PR #6685: Use whd-all on rigid-flex conversion.Gravatar Maxime Dénès2018-02-07
|\ \
* \ \ Merge PR #6610: Points to Flocq official repository.Gravatar Maxime Dénès2018-02-07
|\ \ \
* \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \
* \ \ \ \ Merge PR #6673: Fix evar handling in native_compute conversionGravatar Maxime Dénès2018-02-07
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \ \
| | | | | * | | Points to Flocq official repository.Gravatar Théo Zimmermann2018-02-05
| |_|_|_|/ / / |/| | | | | |
| | | | | * | Respect the transparent state of the current conversion on strong weak-head.Gravatar Pierre-Marie Pédrot2018-02-05
| | | | * | | Add overlay for equations (nf_beta takes an env)Gravatar Gaëtan Gilbert2018-02-05
| | | * | | | [native_compute] Fix handling of evars in conversionGravatar Maxime Dénès2018-02-05
| | | * | | | [native_compute] Remove useless conversion to list in reification.Gravatar Maxime Dénès2018-02-05
| |_|/ / / / |/| | | | |
* | | | | | Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Gravatar Maxime Dénès2018-02-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6654: CI: Run coqchk on IrisGravatar Maxime Dénès2018-02-05
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6652: Allow vernacular controls before focus selectorGravatar Maxime Dénès2018-02-05
|\ \ \ \ \ \ \ \
| | | | | * | | | [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
| | | | |/ / / /
| | | | * / / / [toplevel] Refine start of interactive mode conditions.Gravatar Emilio Jesus Gallego Arias2018-02-05
| |_|_|/ / / / |/| | | | | |
| | | | * | | CClosure.unfold_projection: don't catch Not_found, assume env is okGravatar Gaëtan Gilbert2018-02-02
| | | | * | | Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
| | | | * | | checker: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| | | | * | | checker: remove unused per-constant reduction flags.Gravatar Gaëtan Gilbert2018-02-02
| | | | * | | kernel: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| |_|_|/ / / |/| | | | |
| | | | * | Use whd-all on rigid-flex conversion.Gravatar Pierre-Marie Pédrot2018-02-02
| |_|_|/ / |/| | | |
* | | | | Merge PR #6670: Delete duplicate lineGravatar Maxime Dénès2018-02-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...Gravatar Maxime Dénès2018-02-01
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6672: [stm] Move options to a per-document record.Gravatar Maxime Dénès2018-02-01
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6660: [lib] Respect change of options under with/without_option.Gravatar Maxime Dénès2018-02-01
|\ \ \ \ \ \ \ \
| | | | | | | * | [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
| | | | | | | * | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | | * | CI: Run coqchk on IrisGravatar Ralf Jung2018-01-31
| | | * | | | | Proofview: enter_one: add __LOC__ argument to get relevant error msgGravatar Enrico Tassi2018-01-31
| | * | | | | | [stm] Move options to a per-document record.Gravatar Emilio Jesus Gallego Arias2018-01-31
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #6601: Circle CI: fix cache selection.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m...Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6663: [toplevel] Refactor load path handling.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Delete duplicate lineGravatar Paul Steckler2018-01-30
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | |
| | | | | | * | | | | [lib] Respect change of options under with/without_option.Gravatar Emilio Jesus Gallego Arias2018-01-30
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | | * | | | | | Put default value for NJOBS in ci-common.Gravatar Gaëtan Gilbert2018-01-30
| * | | | | | | | | Adding an overlay for Equations.Gravatar Pierre-Marie Pédrot2018-01-30
* | | | | | | | | | Merge PR #6666: Fix reduction of primitive projections on coinductive records...Gravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Gravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6605: Safer VM interfacesGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6644: Use travis_retry on apt-get updateGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | |
| | | | | * | | | | | | | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | | | | * | | | | | | | | [cbv] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| | | | | * | | | | | | | | [native_compute] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | * | | | | | [toplevel] Refactor load path handling.Gravatar Emilio Jesus Gallego Arias2018-01-29
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 03:09:29 +0000