aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-11Resolve #9885 CoqIDE does not work on WindowsMichael Soegtrop
2019-06-11Move type definition Nativecode.symbols to NativevaluesGaëtan Gilbert
2019-06-11Overlays for 10319Gaëtan Gilbert
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-06-11Simplify implicit_quantifiersGaëtan Gilbert
2019-06-11update elpi to 1.3.1Enrico Tassi
2019-06-10[ci] [fiat-crypto] Enable more targets on Coq CIJason Gross
2019-06-10Merge PR #9566: [proof] Move proofs that have an associated constant to `Lemmas`Pierre-Marie Pédrot
2019-06-09Merge PR #10325: Fix panel behavior as requested by #10292Pierre-Marie Pédrot
2019-06-09[ci] Overlays for move_termination_routine_outEmilio Jesus Gallego Arias
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[save_proof] Make terminator API internal.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
2019-06-09Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint jobEmilio Jesus Gallego Arias
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the v...Emilio Jesus Gallego Arias
2019-06-08Merge PR #10318: Test goal range in "only" selectorsPierre-Marie Pédrot
2019-06-08Merge PR #10263: [proofs] Remove unused API [detected by coverage]Pierre-Marie Pédrot
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-08Updated changelog.Hugo Herbelin
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
2019-06-08Command line: adding variants for Require, aligning on the vernac syntax.Hugo Herbelin
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
2019-06-07Merge PR #10330: Dune: run coqc with -w +defaultEmilio Jesus Gallego Arias
2019-06-07Merge PR #10335: simple IO CI branch is now `master`Emilio Jesus Gallego Arias
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-07Merge PR #10308: Merge the two sources of monomorphic constraints for side-ef...Gaëtan Gilbert
2019-06-07test suite: don't try to coqchk failed testsGaëtan Gilbert
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Dune: run coqc with -w +defaultGaëtan Gilbert
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-07Fix bug #5710Claude Stolze
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain...Pierre-Marie Pédrot
2019-06-06Merge PR #10278: vernac_load doesn't get a ?proof argumentEmilio Jesus Gallego Arias
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
2019-06-06Doc for per commit compile lintGaëtan Gilbert
2019-06-06CI: Test ml compilation of each commit in a PR in lint jobGaëtan Gilbert
2019-06-06Merge PR #10323: Remove old overlaysEmilio Jesus Gallego Arias
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot