aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | | | | | | | | * | | Adding a test for coqchk bug #6619.Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | * | | Fix #6618: coqchk fails with "ill-typed term".Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | * | | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
| | | | | * | | | | | -annotate deprecated. New options: -annot, -bin-annotGravatar Vadim Zaliva2018-01-19
| | | | | | * | | | | update location on tab switch, issue 6624Gravatar Paul Steckler2018-01-19
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | * | | | | | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
| | | * | | | | | | Fix context handling of fix and cofix in Ltac subterm matching.Gravatar Cyprien Mangin2018-01-19
| | | * | | | | | | Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
| | * | | | | | | | add flash infos about wrap, not found, no. of replacements, no. of finds, iss...Gravatar Paul Steckler2018-01-18
| |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6448: Cleanup and add debug printers a bitGravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2...Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6593: Add plugins to META.coqGravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6584: Implement the strategy mechanism in the checkerGravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| | | | | | | | | | * | | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
| | | | | | * | | | | | | | Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| | | | | | * | | | | | | | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
| | | | | | * | | | | | | | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
| | | | | | | |_|_|/ / / / | | | | | | |/| | | | | |
| | | | * | | | | | | | | Update lablgtk check to be more generalGravatar Jason Gross2018-01-16
| | | * | | | | | | | | | Rename coq.ltac to coq.plugins.ltac in META.coqGravatar Cyprien Mangin2018-01-16
| | | | * | | | | | | | | Update configure.ml to only warn on lablgtk 2.16.0Gravatar Jason Gross2018-01-16
| | | | | |/ / / / / / / | | | | |/| | | | | | |
| | | | | | | | | * | | merge-pr.sh: use git diff --quietGravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | * | | Source basic overlay before user overlays.Gravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | * | | Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | * | | Simplify logic and streamline lint-repository.shGravatar Gaëtan Gilbert2018-01-16
* | | | | | | | | | | | Merge PR #6590: Fix the wrapper around ocamldebug.Gravatar Maxime Dénès2018-01-16
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6466: Replace md5sum/md5 calls by an OCaml programGravatar Maxime Dénès2018-01-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |
| | | | | | | * | | | | | | | Add plugins to META.coqGravatar Cyprien Mangin2018-01-16
| |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | |
| | | | * | | | | | | | | | Fix the wrapper around ocamldebug.Gravatar Pierre-Marie Pédrot2018-01-15
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | |
| | * | | | | | | | | | | Avoid shell backticks and improve md5sum.ml error messagesGravatar Jacques-Pascal Deplaix2018-01-15
| * | | | | | | | | | | | More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| * | | | | | | | | | | | Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
| | | | * | | | | | | | | Actually use the strategy information in the checker.Gravatar Pierre-Marie Pédrot2018-01-14
| | | | * | | | | | | | | Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
| |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionGravatar Maxime Dénès2018-01-13
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6581: Added newline at the end of usage of coqdep.Gravatar Maxime Dénès2018-01-13
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Maxime Dénès2018-01-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6483: Strong invariants in polymorphic definitionsGravatar Maxime Dénès2018-01-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6288: Interfaces for checker and IDE.Gravatar Maxime Dénès2018-01-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | | Adding a custom Travis overlay for HoTT.Gravatar Pierre-Marie Pédrot2018-01-11
| | * | | | | | | | | | | | | | | Enforce that polymorphic definitions do not generate internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| | | * | | | | | | | | | | | | | Document test-suite PRINT_LOGS.Gravatar Gaëtan Gilbert2018-01-11
| | | * | | | | | | | | | | | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Gaëtan Gilbert2018-01-11
| |_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | Merge PR #6557: First stab at documenting the test suite.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6552: [PR template] Remove the relative link to CHANGES.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | Added newline at the end of usage of coqdep.Gravatar Bernhard Schommer2018-01-11
| |_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 13:03:53 +0000