aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Pierre-Marie Pédrot
2018-06-10Tweak printing boxes for unicode bindersRalf Jung
2018-05-25An attempt to clarify error message for Arguments needing "rename" flag.Hugo Herbelin
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-15[ssr] import ssreflect test suite from math-compEnrico Tassi
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Emilio Jesus Gallego Arias
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-04-04ssr: check cleared hyps do exist (fix #7050)Enrico Tassi
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09Merge PR #6945: Fix error with univ binders on monomorphic records.Maxime Dénès
2018-03-08Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsMaxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Fix error with univ binders on monomorphic records.Gaëtan Gilbert
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-28[test-suite] Add a basic test-case for `Load`.Emilio Jesus Gallego Arias
2018-02-28Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Maxime Dénès
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-23Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Hugo Herbelin
2018-02-22Adding mention of shelved/given-up status in "Show Existentials".Hugo Herbelin
2018-02-20Update SearchPattern.out for numeral notationsJason Gross
2018-02-20Trying a hack to support {'pat|P} without breaking compatibility.Hugo Herbelin
2018-02-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2018-02-20Change default for notations with variables bound to both terms and binders.Hugo Herbelin
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20When printing a notation with "match", more flexibility in matching equations.Hugo Herbelin
2018-02-20Adding general support for irrefutable disjunctive patterns.Hugo Herbelin
2018-02-20Using an "as" clause when needed for printing irrefutable patterns.Hugo Herbelin
2018-02-20Refining the strategy for glueing let-ins to a sequence of binders.Hugo Herbelin
2018-02-20A (significant) simplification in printing notations with recursive binders.Hugo Herbelin
2018-02-20Respecting the ident/pattern distinction in notation modifiers.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Adding patterns in the category of binders for notations.Hugo Herbelin
2018-02-20In printing notations with "match", reasoning up to the order of clauses.Hugo Herbelin
2018-02-20Supporting recursive notations reversing the left-to-right order.Hugo Herbelin
2018-02-20Allowing variables used in recursive notation to occur several times in pattern.Hugo Herbelin
2018-02-20Allows recursive patterns for binders to be associative on the left.Hugo Herbelin
2018-02-20Fixing/improving notations with recursive patterns.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 14:24:34 +0000