aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-05 21:29:53 +0000