aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
2019-06-18Merge PR #9977: [dune] Support for coqide as an ocamldebug target.Gaëtan Gilbert
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ...Maxime Dénès
2019-06-17Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of #1...Clément Pit-Claudel
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Merge PR #10320: Update headers to the new year.Clément Pit-Claudel
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-17Update copyright years outside of headers.Théo Zimmermann
2019-06-17Clean-up CREDITS file.Théo Zimmermann
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-17Update py-style headers to new year.Théo Zimmermann
2019-06-17Update c-style headers to new year.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Update change-header script to support updating more than just files with ml-...Théo Zimmermann
2019-06-17Adding overlays.Pierre-Marie Pédrot
2019-06-17Clean up the code adding monomorphic global constraints in Safe_typing.Pierre-Marie Pédrot
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-17Merge PR #10226: Simplify implicit_quantifiersEmilio Jesus Gallego Arias
2019-06-17Merge PR #10382: Ensuring that regular expression filtering in CI (iris) work...Gaëtan Gilbert
2019-06-17[dune] Support for coqide as an ocamldebug target.Emilio Jesus Gallego Arias
2019-06-17Merge PR #10332: test suite: don't try to coqchk failed testsEnrico Tassi
2019-06-17Merge PR #10368: Update, expand, and document plugin tutorial 2Enrico Tassi
2019-06-17[ci] Overlays for #9645Emilio Jesus Gallego Arias
2019-06-17[proof] Respond to a comment by Pierre-MarieEmilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 07:34:00 +0000