| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | Merge remote-tracking branch 'github/pr/194' into trunk |  Maxime Dénès | 2016-06-16 | |
| |\ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | Fix another missing newline |  Jason Gross | 2016-06-16 | |
| | | | | | * | | | | Fix a printing typo | Jason Gross | 2016-06-16 | |
| | |_|_|_|/ / / / |/| | | | | | | | ||||
| | | | | * | | | | Fixing the checker. |  Pierre-Marie Pédrot | 2016-06-16 | |
| | | | | * | | | | Remove the syntax changes introduced by this branch. | Pierre-Marie Pédrot | 2016-06-15 | |
| * | | | | | | | | Fix test-suite for opened bug #4813. | Pierre-Marie Pédrot | 2016-06-15 | |
| | | | | * | | | | Allow `Pretyping.search_guard` to not check guard |  Arnaud Spiwack | 2016-06-15 | |
| | | * | | | | | | ssrmatching: giving proper credits to the original author(s) |  Enrico Tassi | 2016-06-15 | |
| | | * | | | | | | Merge branch 'pr/146' into trunk | Enrico Tassi | 2016-06-15 | |
| | |/| | | | | | |/| | | | | | | | ||||
| | | * | | | | | | ssrmatching: simple test for Ltac API | Enrico Tassi | 2016-06-15 | |
| | | * | | | | | | ssrmatching: ltac argument parsing made more robust | Enrico Tassi | 2016-06-15 | |
| | | * | | | | | | ssrmatching: debug prints sent via msg_debug | Enrico Tassi | 2016-06-15 | |
| | | * | | | | | | Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching" | Enrico Tassi | 2016-06-15 | |
| * | | | | | | | | typography |  Matej Kosik | 2016-06-15 | |
| * | | | | | | | | ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpack |  Pierre Letouzey | 2016-06-15 | |
| * | | | | | | | | Makefile.build: ensure a build failure in case of a missing rule | Pierre Letouzey | 2016-06-15 | |
| * | | | | | | | | fix test-suite/ide Makefile (stupid typo) | Enrico Tassi | 2016-06-15 | |
| | | | | * | | | | Assume totality: dedicated type rather than bool | Arnaud Spiwack | 2016-06-14 | |
| * | | | | | | | | Preventive compatibility fixes for flushing. |  Emilio Jesus Gallego Arias | 2016-06-14 | |
| * | | | | | | | | Fix for bug #4784 | Emilio Jesus Gallego Arias | 2016-06-14 | |
| * | | | | | | | | Repair the build of ide/coqidetop.cmxs (fix #4812) | Pierre Letouzey | 2016-06-14 | |
| | | | | | | | * | Allow catching of EvaluatedError exceptions. | Emilio Jesus Gallego Arias | 2016-06-14 | |
| | |_|_|_|_|_|/ |/| | | | | | | ||||
| | | * | | | | | port ssrmatching plugin to the new makefile | Enrico Tassi | 2016-06-14 | |
| | | * | | | | | Merge remote-tracking branch 'origin/pr/146' into trunk | Enrico Tassi | 2016-06-14 | |
| | |/| | | | | |/| | | | | | | ||||
| | | | | | * | | Add documentation for goal selectors. |  Cyprien Mangin | 2016-06-14 | |
| * | | | | | | | Merge remote-tracking branch 'origin/pr/166' into trunk | Enrico Tassi | 2016-06-14 | |
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/pr/205' into trunk | Enrico Tassi | 2016-06-14 | |
| |\ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | -async-proofs-delegation-threshold default value set to 0.03 | Enrico Tassi | 2016-06-14 | |
| * | | | | | | | | | Merge remote-tracking branch 'origin/pr/182' into trunk | Enrico Tassi | 2016-06-14 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | test-suiet: run fake_id as before pr/173 was merged | Enrico Tassi | 2016-06-14 | |
| * | | | | | | | | | | configure: use ln on linux and cp on windows | Enrico Tassi | 2016-06-14 | |
| * | | | | | | | | | | Merge remote-tracking branch 'origin/pr/173' into trunk | Enrico Tassi | 2016-06-14 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | Ident selectors cannot be used inside an Ltac expression. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Goal selectors are now tacticals and can be used as such. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Remove the need for brackets in goal selectors. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Fix a typo in proofs/proofview.mli. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Fix usage of Pervasives in goal selectors. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Add a comment about the use of a zipper, for clarity. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Fix the pretty-printing of goal range selectors. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Add a [CList.partitioni] function. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Add test-suite file for goal selectors. | Cyprien Mangin | 2016-06-14 | |
| | | | | | | | | | * | | Add goal range selectors. | Cyprien Mangin | 2016-06-14 | |
| | |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | ||||
| * | | | | | | | | | | Merge branch "LtacProf for trunk" (PR #165). | Pierre-Marie Pédrot | 2016-06-14 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | Commenting out debugging code. | Pierre-Marie Pédrot | 2016-06-14 | |
| | * | | | | | | | | | | Correct use of printing primitives. | Pierre-Marie Pédrot | 2016-06-14 | |
| | * | | | | | | | | | | Better coding style (semantics). | Pierre-Marie Pédrot | 2016-06-14 | |
| | * | | | | | | | | | | Better coding style (syntax). | Pierre-Marie Pédrot | 2016-06-14 | |
| | * | | | | | | | | | | Adding Coq headers. | Pierre-Marie Pédrot | 2016-06-14 | |
| | * | | | | | | | | | | Moving back Ltac profiling to the Ltac folder. | Pierre-Marie Pédrot | 2016-06-14 | |
| * | | | | | | | | | | | Merge remote-tracking branch 'github/evarunsafe' into trunk |  Matthieu Sozeau | 2016-06-14 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |