aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-12-13Merge PR #11281: [vm] Untabify the VM C code.Maxime Dénès
2019-12-12Merge PR #11278: Clean libobject stuffGaëtan Gilbert
2019-12-12[vm] Untabify the VM C code.Emilio Jesus Gallego Arias
2019-12-12Merge PR #11264: Type safe summary & libobject implementationEmilio Jesus Gallego Arias
2019-12-12Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on only-p...Emilio Jesus Gallego Arias
2019-12-11Remove the unused add_leaves Libobject primitive.Pierre-Marie Pédrot
2019-12-11Remove the reliance of ring objects on the named part.Pierre-Marie Pédrot
2019-12-11Merge PR #11201: remove *.vos and *.vok file in "make clean"Enrico Tassi
2019-12-11Merge PR #11262: [hashset] Don't use deprecated Obj.truncatePierre-Marie Pédrot
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ...Pierre-Marie Pédrot
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
2019-12-10Merge PR #11269: Several cleanups and factorization in scheme declarationsEmilio Jesus Gallego Arias
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-10Merge PR #11268: dune: Add byte mode for coqchk and coqide (fix dune-dbg for ...Emilio Jesus Gallego Arias
2019-12-09dune: Add byte mode for coqchk and coqide (fix dune-dbg for dune 2)Gaëtan Gilbert
2019-12-09Type-safe implementation of libobjects.Pierre-Marie Pédrot
2019-12-09Simplify the implementation of Summary by specifying the type of ML-MODULES.Pierre-Marie Pédrot
2019-12-09Type-safe implementation of summary state.Pierre-Marie Pédrot
2019-12-09Merge PR #11255: Fix #11254: "coqtop --version" working even in the middle of...Emilio Jesus Gallego Arias
2019-12-09Fixes #11254 (not requiring coqlib to be set to report about coqtop version).Hugo Herbelin
2019-12-09Merge PR #10829: Section.t is never emptyPierre-Marie Pédrot
2019-12-09Merge PR #11234: [ide] Don't use -linkall for the GUI app.Pierre-Marie Pédrot
2019-12-09[hashset] Don't use deprecated Obj.truncateEmilio Jesus Gallego Arias
2019-12-09Merge PR #11256: [configure] [dune] Fix configure under Dune in 32bit builds.Théo Zimmermann
2019-12-07Section.t is never emptyGaëtan Gilbert
2019-12-07[configure] [dune] Fix configure under Dune in 32bit builds.Emilio Jesus Gallego Arias
2019-12-07Merge PR #11141: Moving the diversity of constr printers to a label styleEmilio Jesus Gallego Arias
2019-12-06Adding documentation in printer.mliHugo Herbelin
2019-12-06Adding overlay for Quickchick PR#145.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
2019-12-06Merge PR #11232: Remove latex files that should be regenerated by makeThéo Zimmermann
2019-12-06Merge PR #11174: [dune] Update to dune language version 2.0Théo Zimmermann
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Merge PR #11172: Interleave removal of coercions and search for notationsEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-12-04Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.Hugo Herbelin
2019-12-04Overlay for ELPIHugo Herbelin
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
2019-12-03Update doc/changelog/03-notations/11172-master+coercion-notation-interleaved-...Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03[ide] Don't use -linkall for the GUI app.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:30:23 +0000