aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
2020-02-21Merge PR #11590: Fixes #9741: only printing notations do not uselessly reserv...Emilio Jesus Gallego Arias
2020-02-21Merge PR #11642: Unconditionally print explanation for universe inconsistenciesEmilio Jesus Gallego Arias
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
2020-02-21Merge PR #11142: Slightly improving strategy about when to print coercion or ...Emilio Jesus Gallego Arias
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2020-02-21Adding changelog for #11590, fixing #9741.Hugo Herbelin
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2020-02-21Tactic_matching.pattern_match_term: remove ignored "refresh" argumentGaëtan Gilbert
2020-02-21Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.Gaëtan Gilbert
2020-02-21[merge-script] Improve warning in case of batch merging.Théo Zimmermann
2020-02-21Merge PR #11648: [test-suite] Fix output tests due to merge problems.Hugo Herbelin
2020-02-20[test-suite] Fix output tests due to merge problems.Emilio Jesus Gallego Arias
2020-02-20Merge PR #11143: In Print/Check/Show, adopt the view that the attached type i...Emilio Jesus Gallego Arias
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
2020-02-21Merge PR #11329: Fixing #11114: anomaly with Extraction Implicit on records.Kazuhiko Sakaguchi
2020-02-20Unconditionally print explanation for universe inconsistenciesGaëtan Gilbert
2020-02-20Merge PR #11616: [coqdep] Tweak changelog after recent PRs.Gaëtan Gilbert
2020-02-20Merge PR #11633: Add doc/unreleased.rst to .gitignore.Gaëtan Gilbert
2020-02-20Merge PR #11630: [make] Fix makefile variable after plugin .v files moveGaëtan Gilbert
2020-02-20Merge PR #11612: CoqIDE: allow opening multiple files at onceHugo Herbelin
2020-02-20Adding changelog.Hugo Herbelin
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-20Adding a printer for GlobEnv in ocamldebug.Hugo Herbelin
2020-02-19Update copyright in refman to year 2020.Théo Zimmermann
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-19Overlays for Equations, QuickChick and Iris.Hugo Herbelin
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-19Short allusion in refman on the existence of a generic and specific format.Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2020-02-19Preparing fix to #6082 and #7766: Renaming type scope_elem and its elements.Hugo Herbelin
2020-02-19Remove the dependency in float.cmo and uint63.cmo for building votour.Hugo Herbelin
2020-02-19Add doc/unreleased.rst to .gitignore.Théo Zimmermann
2020-02-19[make] Fix makefile variable after plugin .v files moveEmilio Jesus Gallego Arias
2020-02-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-18Deprecate unsafe_type_ofGaëtan Gilbert
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:02:56 +0000