aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-08When printing term together with its type, use info that term is in context.Hugo Herbelin
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-06Make the string argument of `time` print correctlyJason Gross
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-06additional statements on flat_mapOlivier Laurent
2019-12-06additional statements on map and ForallOlivier Laurent
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
2019-12-06integration of list_sum and list_maxOlivier Laurent
2019-12-06integration of statements for repeatOlivier Laurent
2019-12-06integration of statements for NoDupOlivier Laurent
2019-12-06integration of additional statements for inclOlivier Laurent
2019-12-06integration of statements for removeOlivier Laurent
2019-12-06integration of statements for InOlivier Laurent
2019-12-06integration of statements for inclOlivier Laurent
2019-12-06integration of statements for revOlivier Laurent
2019-12-06integration of statements for concat and flat_mapOlivier Laurent
2019-12-06integration of statements for seqOlivier Laurent
2019-12-06integration of statements related to last elementOlivier Laurent
2019-12-06integration of Exists_or and Forall_andOlivier Laurent
2019-12-06redundancy between skipn_node and skipn_allOlivier Laurent
2019-12-06Use standard float an integer datatypes in Votour representation.Pierre-Marie Pédrot
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-04Update doc/changelog/02-specification-language/11233-master+fix11231-missing-...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
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-03Merge PR #11175: coercion functions are never called without a term to coerceEnrico Tassi
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 21:34:50 +0000