aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Gravatar Pierre-Marie Pédrot2018-06-14
|\
* | Tweak printing boxes for unicode bindersGravatar Ralf Jung2018-06-10
* | An attempt to clarify error message for Arguments needing "rename" flag.Gravatar Hugo Herbelin2018-05-25
* | Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
* | [ssr] import ssreflect test suite from math-compGravatar Enrico Tassi2018-05-15
* | Fixing a bug in printing the body of a located notation.Gravatar Hugo Herbelin2018-05-13
* | Making explicit that errors happen in one of five executation phases.Gravatar Hugo Herbelin2018-05-02
* | Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Gravatar Emilio Jesus Gallego Arias2018-04-09
|\ \
* \ \ Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Gravatar Maxime Dénès2018-04-09
|\ \ \
| | | * Fixes #7192 (Print Assumptions does not enter implementation of submodules).Gravatar Hugo Herbelin2018-04-07
| |_|/ |/| |
* | | Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \ \
| | * | ssr: check cleared hyps do exist (fix #7050)Gravatar Enrico Tassi2018-04-04
* | | | Fix #6404 - Print tactics called by ML tacticsGravatar Jason Gross2018-04-02
| |/ / |/| |
| * | Fix #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-03-30
|/ /
| * Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-03-29
* | Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
|/
* Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
* Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6945: Fix error with univ binders on monomorphic records.Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \
| | | * [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
| |_|/ |/| |
| | * Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-03-08
| |/ |/|
* | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \
| * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
* | | [test-suite] Add a basic test-case for `Load`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ /
* | Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Gravatar Maxime Dénès2018-02-28
|\ \
* \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \
| | * | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
| |/ / |/| |
| | * Adding mention of shelved/given-up status in "Show Existentials".Gravatar Hugo Herbelin2018-02-22
| |/ |/|
| * Update SearchPattern.out for numeral notationsGravatar Jason Gross2018-02-20
* | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
* | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
* | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
* | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* | When printing a notation with "match", more flexibility in matching equations.Gravatar Hugo Herbelin2018-02-20
* | Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
* | Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
* | Refining the strategy for glueing let-ins to a sequence of binders.Gravatar Hugo Herbelin2018-02-20
* | A (significant) simplification in printing notations with recursive binders.Gravatar Hugo Herbelin2018-02-20
* | Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
* | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
* | In printing notations with "match", reasoning up to the order of clauses.Gravatar Hugo Herbelin2018-02-20
* | Supporting recursive notations reversing the left-to-right order.Gravatar Hugo Herbelin2018-02-20
* | Allowing variables used in recursive notation to occur several times in pattern.Gravatar Hugo Herbelin2018-02-20
* | Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
* | Fixing/improving notations with recursive patterns.Gravatar Hugo Herbelin2018-02-20
* | Using name given by user to name a 'pat, if any.Gravatar Hugo Herbelin2018-02-20
* | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* | Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 15:13:57 +0000