aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2017-12-31Trim more trailing whitespace in coq-makefile timing testJason Gross
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
2017-12-20Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).Maxime Dénès
2017-12-20Merge PR #6234: Make the micromega extraction check a regular output test.Maxime Dénès
2017-12-19Fix ltacprof_abstract (I think because of #6411 parallel merge).Gaëtan Gilbert
2017-12-19Merge PR #6400: Circle CIMaxime Dénès
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-18Merge PR #6406: Make [abstract] nodes show up in the Ltac profileMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Maxime Dénès
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-15Do dependencies in 1 command per file class.Gaëtan Gilbert
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
2017-12-14Make [abstract] nodes show up in the Ltac profileJason Gross
2017-12-14Add tactics to reset and display the Ltac profileJason Gross
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-14Merge PR #6379: Fix profiling pluginMaxime Dénès
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Maxime Dénès
2017-12-14Circle CI: cat failed test suite logsGaëtan Gilbert
2017-12-13Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Maxime Dénès
2017-12-12Fix #5081 by more fine-grained LtacProf recordingJason Gross
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-11Allow LtacProf tactics to be calledJason Gross
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed
2017-12-11Fix anomaly in [Type foo] command, + print uctx like Check.Gaëtan Gilbert
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ...Maxime Dénès
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès
2017-12-03Adding a test for #6304 (bug with fix in notations).Hugo Herbelin
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-12-01Tests for global universe declarationsMatthieu Sozeau
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Maxime Dénès
2017-11-30Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Maxime Dénès
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Maxime Dénès
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-28Make the micromega extraction check a regular output test.Gaëtan Gilbert
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Maxime Dénès
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
2017-11-27Pre-isolating a notation test to avoid interferences.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 20:33:54 +0000