aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-22Fix inheritance of argument scopes when printing notations in patterns.Hugo Herbelin
2020-02-22Use auxiliary function for externing record patterns.Hugo Herbelin
2020-02-22Inherit argument scopes in notations to expressions of the form @f.Hugo Herbelin
2020-02-22Propagate implicit arguments in all notations for partial applications.Hugo Herbelin
2020-02-22Deactivate implicit arguments in printing notations bound to "@f".Hugo Herbelin
2020-02-22Fixing printing of notations bound to an expression of the form "@f".Hugo Herbelin
2020-02-22Fixing a notation printing bug (missing a @ to reflect absence of imp. args).Hugo Herbelin
2020-02-22Fixing anomaly from #11091 (incompatible printing with notation and imp. args).Hugo Herbelin
2020-02-22Merge PR #11596: ComInductive: use lbound=Prop iff non polymorphicEmilio Jesus Gallego Arias
2020-02-22Merge PR #11639: Fixes #10917: anomaly in building return clause of n-ary pat...Emilio Jesus Gallego Arias
2020-02-22Merge PR #11638: Add debugger printer for type GlobEnv.tEmilio Jesus Gallego Arias
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
2020-02-22Simplification of type unparsing (index of variable in UnpMetaVar is unused).Hugo Herbelin
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
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-21Adding changelog for #11590, fixing #9741.Hugo Herbelin
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2020-02-21Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.Gaëtan Gilbert
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 08:37:29 +0000