aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2018-02-20Fixing/improving notations with recursive patterns.Hugo Herbelin
2018-02-20Using name given by user to name a 'pat, if any.Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-02-20Notations: Do not consider a non-occurring variable as a binder-only variable.Hugo Herbelin
2018-02-20Adding support for re-folding notation referring to isolated "forall '(x,y), t".Hugo Herbelin
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Maxime Dénès
2018-02-19Fix #6529: nf_evar_info and check the env evars' not just the conclMatthieu Sozeau
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-16Cleaner treatment of parameters in inferCumulativityGaëtan Gilbert
2018-02-16Adding a test for the construction that was broken in Coccinelle.Pierre-Marie Pédrot
2018-02-15Adding a test for variance subtyping in the module system.Pierre-Marie Pédrot
2018-02-15Merge PR #1073: new quick2vo target: like vio2vo, but smarterMaxime Dénès
2018-02-15disable tests: vio2vo is broken in WindowsRalf Jung
2018-02-15also test vio2voRalf Jung
2018-02-15test "make quick2vo"Ralf Jung
2018-02-15Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectMaxime Dénès
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:12:58 +0000