aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-17[equations] [proof] Remove reference to evar_mapEmilio Jesus Gallego Arias
2019-06-17[equations] [proof] Remove duplicate shrink function.Emilio Jesus Gallego Arias
2019-06-17[proof] Add proof save path for equations.Emilio Jesus Gallego Arias
2019-06-17[lemmas] Refactoring in saving goal.Emilio Jesus Gallego Arias
2019-06-17[proof] Remove terminator type, unifying regular and obligation ones.Emilio Jesus Gallego Arias
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-17[proof] drop parameter from terminator typeEmilio Jesus Gallego Arias
2019-06-17[proof] Unify obligation proof save path: Part I, declareOblEmilio Jesus Gallego Arias
2019-06-17[proofs] Store hooks in the proof object.Emilio Jesus Gallego Arias
2019-06-17Merge PR #10231: Adding location in warning telling implicit arguments differ...Emilio Jesus Gallego Arias
2019-06-16Merge PR #10385: Changelog for 8.10+beta2.Clément Pit-Claudel
2019-06-16Merge PR #10381: Fix #10090: Ltac1 destruct and Ltac2 destruct should do the ...Emilio Jesus Gallego Arias
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
2019-06-16Ensuring regexp filtering in ci works on MacOS X.Hugo Herbelin
2019-06-16Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.Pierre-Marie Pédrot
2019-06-16Merge PR #10345: Fix #10339: Anomaly in Ltac2.Emilio Jesus Gallego Arias
2019-06-16Overlays for Mtac2 and Equations.Hugo Herbelin
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-16Merge PR #10327: Fix bug #5710Pierre-Marie Pédrot
2019-06-16Merge PR #10355: [funind] Untabify; necessary to ease the review of subsequen...Pierre-Marie Pédrot
2019-06-16- added OCaml copyright header to List.v (if for no other reason than out of ...Michael Soegtrop
2019-06-15Merge PR #10040: Install byte version of coqidetop.Emilio Jesus Gallego Arias
2019-06-15[dune] Install .byte version of coqidetop like for coqtop.Théo Zimmermann
2019-06-15Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.Clément Pit-Claudel
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
2019-06-14Merge PR #10376: Add a comment documenting what fontsupport.py is.Clément Pit-Claudel
2019-06-14Add a comment documenting what fontsupport.py is.Théo Zimmermann
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
2019-06-13Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries.Clément Pit-Claudel
2019-06-13Merge PR #10373: Add missing changelog entry for #10360.Clément Pit-Claudel
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-13Update, expand, and document plugin tutorial 2Talia Ringer
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
2019-06-13Merge PR #10360: Resolve #9885 CoqIDE does not work on WindowsEmilio Jesus Gallego Arias
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building Co...Clément Pit-Claudel
2019-06-12[funind] Untabify; necessary to ease the review of subsequent work.Emilio Jesus Gallego Arias
2019-06-12Merge PR #10358: [docker] update elpi to 1.3.1Gaëtan Gilbert
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-12Merge PR #10329: Update changelog for 10302 and 10305Théo Zimmermann
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-12Fix #9455: avoid update_global_env when unchanged Global.universes()Gaëtan Gilbert
2019-06-12Merge PR #10334: Remove the side-effect role from the kernel.Enrico Tassi
2019-06-11overlayEnrico Tassi
2019-06-11Adding an overlay for Equations.Pierre-Marie Pédrot
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11Merge PR #10354: [ci] [fiat-crypto] Enable more targets on Coq CIEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 06:49:33 +0000