aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-02-07Merge PR #6657: Document the Fail commandMaxime Dénès
2018-02-07Merge PR #6685: Use whd-all on rigid-flex conversion.Maxime Dénès
2018-02-07Merge PR #6610: Points to Flocq official repository.Maxime Dénès
2018-02-07Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingMaxime Dénès
2018-02-07Merge PR #6673: Fix evar handling in native_compute conversionMaxime Dénès
2018-02-06Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Maxime Dénès
2018-02-06Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Maxime Dénès
2018-02-05Points to Flocq official repository.Théo Zimmermann
2018-02-05Respect the transparent state of the current conversion on strong weak-head.Pierre-Marie Pédrot
2018-02-05Add overlay for equations (nf_beta takes an env)Gaëtan Gilbert
2018-02-05[native_compute] Fix handling of evars in conversionMaxime Dénès
2018-02-05[native_compute] Remove useless conversion to list in reification.Maxime Dénès
2018-02-05Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Maxime Dénès
2018-02-05Merge PR #6654: CI: Run coqchk on IrisMaxime Dénès
2018-02-05Merge PR #6652: Allow vernacular controls before focus selectorMaxime Dénès
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
2018-02-05[toplevel] Refine start of interactive mode conditions.Emilio Jesus Gallego Arias
2018-02-02CClosure.unfold_projection: don't catch Not_found, assume env is okGaëtan Gilbert
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-02-02checker: cleanup projection unfoldingGaëtan Gilbert
2018-02-02checker: remove unused per-constant reduction flags.Gaëtan Gilbert
2018-02-02kernel: cleanup projection unfoldingGaëtan Gilbert
2018-02-02Use whd-all on rigid-flex conversion.Pierre-Marie Pédrot
2018-02-01Merge PR #6670: Delete duplicate lineMaxime Dénès
2018-02-01Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...Maxime Dénès
2018-02-01Merge PR #6672: [stm] Move options to a per-document record.Maxime Dénès
2018-02-01Merge PR #6660: [lib] Respect change of options under with/without_option.Maxime Dénès
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-31CI: Run coqchk on IrisRalf Jung
2018-01-31Proofview: enter_one: add __LOC__ argument to get relevant error msgEnrico Tassi
2018-01-31[stm] Move options to a per-document record.Emilio Jesus Gallego Arias
2018-01-31Merge PR #6601: Circle CI: fix cache selection.Maxime Dénès
2018-01-31Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m...Maxime Dénès
2018-01-31Merge PR #6663: [toplevel] Refactor load path handling.Maxime Dénès
2018-01-31Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Maxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-30Delete duplicate linePaul Steckler
2018-01-30[lib] Respect change of options under with/without_option.Emilio Jesus Gallego Arias
2018-01-30Put default value for NJOBS in ci-common.Gaëtan Gilbert
2018-01-30Adding an overlay for Equations.Pierre-Marie Pédrot
2018-01-30Merge PR #6666: Fix reduction of primitive projections on coinductive records...Maxime Dénès
2018-01-30Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsMaxime Dénès
2018-01-30Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Maxime Dénès
2018-01-30Merge PR #6605: Safer VM interfacesMaxime Dénès
2018-01-30Merge PR #6644: Use travis_retry on apt-get updateMaxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-29[cbv] Fix evaluation of cofixpoints under primitive projections.Maxime Dénès
2018-01-29[native_compute] Fix evaluation of cofixpoints under primitive projections.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:53:53 +0000