| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | * | | | | | | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | | Moving UTF-8 related functions to Unicode module. | Pierre-Marie Pédrot | 2016-06-14 | |
| | | * | | | | | | | | | | Revert "Strip some trailing spaces" | Pierre-Marie Pédrot | 2016-06-13 | |
| * | | | | | | | | | | | | Univs: more robust Universe/Constraint decls #4816 | Matthieu Sozeau | 2016-06-13 | |
| * | | | | | | | | | | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-13 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | | STM classification: VernacTimeout may contain an "internal command". |  Maxime Dénès | 2016-06-13 | |
| | | | | | | * | | | | | | | Print Assumptions and co. can "pierce opacity". | Maxime Dénès | 2016-06-13 | |
| | |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | ||||
| | * | | | | | | | | | | | evar_conv: Refine occur_rigidly |  Matthieu Sozeau | 2016-06-13 | |
| | * | | | | | | | | | | | Tentatively fixing misguiding error message with "binder" type in |  Hugo Herbelin | 2016-06-13 | |
| * | | | | | | | | | | | | For the record, an example one would like to see working. | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Minor simplification in evarconv. | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Another fix to #4782 (a typing error not captured when dealing with bindings). | Hugo Herbelin | 2016-06-12 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |