aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Maxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
2018-03-03Adding a test file for evar handling in the VM.Pierre-Marie Pédrot
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-02-28[test-suite] Add a basic test-case for `Load`.Emilio Jesus Gallego Arias
2018-02-28Merge PR #6756: Fix issue with spurious timing test failuresMaxime Dénès
2018-02-28Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-24[test-suite] Move sed scripts into bash arraysJason Gross
2018-02-24Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).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-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-21Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Maxime Dénès
2018-02-21Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...Maxime Dénès
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-20Update SearchPattern.out for numeral notationsJason Gross
2018-02-20Fixes bug #6774 (anomaly with ill-typed template polymorphism).Hugo Herbelin
2018-02-20Adding a test for wish #5532.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 05:40:56 +0000