aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-23Adding tests for Set Printing Parentheses.Hugo Herbelin
2020-02-23Cancelling precedences in Set Printing Parentheses only at border of notations.Hugo Herbelin
2020-02-23Adding a Display Parentheses menu in CoqIDE.Hugo Herbelin
2020-02-23Not iterating recursive notations more than once.Hugo Herbelin
2020-02-23parens --> parenthesesAbhishek Anand (optiplex7010@home)
2020-02-23bugfix: switched then/else: parens option false (default)=> no parensAbhishek Anand (optiplex7010@home)
2020-02-23added the new optionAbhishek Anand (optiplex7010@home)
2020-02-23patched the print functionAbhishek Anand (optiplex7010@home)
2020-02-23Remove unqualified universe attributes.Théo Zimmermann
2020-02-23Merge pull request #11629 from ppedrot/fix-11552Tej Chajed
2020-02-23Fix #11654: syntax of inductive declaration.Théo Zimmermann
2020-02-23Documenting inheritance of implicit arguments and scopes in notations.Hugo Herbelin
2020-02-23Addressing a changelog comment from Théo Zimmermann.Hugo Herbelin
2020-02-23Update doc/changelog/03-notations/11120-master+refactoring-application-printi...Hugo Herbelin
2020-02-23Apply and generalize suggestions from Théo.Hugo Herbelin
2020-02-22Merge PR #11651: [merge-script] Improve warning in case of batch merging.Emilio Jesus Gallego Arias
2020-02-22Adding a changelog item.Hugo Herbelin
2020-02-22Fixes #4690: do not allow @f in notations when f is a notation variable.Hugo Herbelin
2020-02-22New parsing/printing pattern/terms imp/scopes tests summarizing last changes.Hugo Herbelin
2020-02-22Inherit arguments scopes in pattern notations bound to some @id.Hugo Herbelin
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
2020-02-22Inherit scopes and implicit sign. in notations for partially applied pattern.Hugo Herbelin
2020-02-22Fix index bug in computing implicit signature of abbrev. in pattern printing.Hugo Herbelin
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 18:38:13 +0000