aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ↵Maxime Dénès
vernac Reviewed-by: maximedenes
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)Théo Zimmermann
2019-05-23Merge PR #10214: Better dune ocamldebug integrationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
2019-05-23Fixing typos - Part 2JPR
2019-05-22Better dune ocamldebug integrationGaëtan Gilbert
- use coqc instead of coqtop (since -compile doesn't work anymore this is better) - pass through extra arguments to dune-dbg - auto detect the need to pass -emacs to ocamldebug - instructions for emacs users The dune-dbg dependencies are still broken ;_;
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based ↵Hugo Herbelin
generalization + cleanups Reviewed-by: herbelin
2019-05-22Update build-system.txtFourchaux
2019-05-21Fixing typos - Part 1JPR
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged.
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Overlay for removing Instance: !type syntaxGaëtan Gilbert
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-17[nix] Update reference to nixpkgsVincent Laporte
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10164: Add aucontext debug printerPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-14Add aucontext debug printerGaëtan Gilbert
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: jfehrle Reviewed-by: vbgl
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-13Add overlay for UnicoqMaxime Dénès
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026.
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
Reviewed-by: herbelin
2019-05-10Add overlay for elpiVincent Laporte
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl
2019-05-10Add overlays for coq/coq#10052.Pierre-Marie Pédrot
2019-05-10Merge PR #10120: Clean-up: remove dead appveyor.sh file.Emilio Jesus Gallego Arias
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it.
2019-05-09Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repoMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-05-09Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlabMichael Soegtrop
2019-05-08Update release process documentation and changelog entry.Théo Zimmermann
2019-05-08Remove ltac2 add-on from Windows installer now that it is in the main Coq ↵Théo Zimmermann
package.
2019-05-08Clean-up: remove dead appveyor.sh file.Théo Zimmermann
2019-05-07Remove overlays for CompCert and VSTVincent Laporte
2019-05-07[nix-ci] Add coquelicot, improve flocqVincent Laporte
2019-05-07Add overlays for CompCert, VST, and coquelicotVincent Laporte
2019-05-07Remove ppedrot/ltac2 from CI after integration in main repoGaëtan Gilbert
2019-05-07Add overlays.Pierre-Marie Pédrot
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
Move existing entries.
2019-04-29Merge PR #9987: Fix #9180 by reverting #9249 and #8187Emilio Jesus Gallego Arias
Reviewed-by: maximedenes
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ↵Maxime Dénès
not to be used. Ack-by: ejgallego Ack-by: gares Reviewed-by: maximedenes
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-29Revert #8187Vincent Laporte
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 03:25:35 +0000