| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Replace md5sum/md5 calls by an OCaml program |  Jacques-Pascal Deplaix | 2017-12-23 |
| * | Merge PR #6465: Gitlab touchup |  Maxime Dénès | 2017-12-22 |
| |\ | |||
| * \ | Merge PR #6469: No universe constraints in Let definitions | Maxime Dénès | 2017-12-22 |
| |\ \ | |||
| * \ \ | Merge PR #6318: Separate vernac controls and regular commands. | Maxime Dénès | 2017-12-22 |
| |\ \ \ | |||
| * \ \ \ | Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ. | Maxime Dénès | 2017-12-22 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #6485: Fix badges. | Maxime Dénès | 2017-12-22 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query. | Maxime Dénès | 2017-12-22 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6222: Share computation of unifiable evars | Maxime Dénès | 2017-12-22 |
| |\ \ \ \ \ \ \ | |||
| | | | * | | | | | Fix badges. |  Théo Zimmermann | 2017-12-21 |
| | |_|/ / / / / |/| | | | | | | |||
| | | | * | | | | Update README and CONTRIBUTING to mention the wiki and FAQ. | Théo Zimmermann | 2017-12-21 |
| | |_|/ / / / |/| | | | | | |||
| * | | | | | | Merge PR #6474: Fix CI with parallel make (messed up dependencies) | Maxime Dénès | 2017-12-21 |
| |\ \ \ \ \ \ | |||
| | * | | | | | | Fix CI with parallel make (messed up dependencies) |  Gaëtan Gilbert | 2017-12-21 |
| | | | | * | | | Separate vernac controls and regular commands. | Maxime Dénès | 2017-12-20 |
| | |_|_|/ / / |/| | | | | | |||
| * | | | | | | Merge PR #6377: Removal of the FAQ LaTex document. | Maxime Dénès | 2017-12-20 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6470: Fix typo in the refman. | Maxime Dénès | 2017-12-20 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6449: Let definitions must not contain side-effects when reaching t... | Maxime Dénès | 2017-12-20 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6468: Fix order of let-in representation comment. | Maxime Dénès | 2017-12-20 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge). | Maxime Dénès | 2017-12-20 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6234: Make the micromega extraction check a regular output test. | Maxime Dénès | 2017-12-20 |
| |\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |||
| | | * | | | | | | | | | Fix ltacprof_abstract (I think because of #6411 parallel merge). | Gaëtan Gilbert | 2017-12-19 |
| | |/ / / / / / / / / |/| | | | | | | | | | |||
| | | | | * | | | | | | Fix typo in the refman. | Théo Zimmermann | 2017-12-19 |
| | |_|_|/ / / / / / |/| | | | | | | | | |||
| | | | | | | | * | | Let definitions do not create new universe constraints. |  Pierre-Marie Pédrot | 2017-12-19 |
| * | | | | | | | | | Merge PR #6400: Circle CI | Maxime Dénès | 2017-12-19 |
| |\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | Specific type for section definition entries. | Pierre-Marie Pédrot | 2017-12-19 |
| | | | | | |_|_|/ / | | | | |/| | | | | |||
| | | | * / | | | | | Fix order of let-in representation comment. |  Jasper Hugunin | 2017-12-19 |
| | |_|/ / / / / / |/| | | | | | | | |||
| | | | | | | | * | Gitlab: don't ./configure in documentation job | Gaëtan Gilbert | 2017-12-18 |
| | |_|_|_|_|_|/ |/| | | | | | | |||
| * | | | | | | | Merge PR #6436: Fix #5368: Canonical structure unification fails. | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6447: [make] More build fixes for static plugins and ocamlfind. | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6284: Warning for absolute name masking (deprecated, should become ... | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6381: A version of [time] that works on constr evaluation | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6406: Make [abstract] nodes show up in the Ltac profile | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra... | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6305: Build with windows line endings | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | * | | | Removing the FAQ, which has been moved to the GitHub wiki for this |  Matt Quinn | 2017-12-18 |
| * | | | | | | | | | | | | | | | | Merge PR #6453: [doc] Nit on the manual. | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6419: [vernac] Split `command.ml` into separate files. | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | Maxime Dénès | 2017-12-18 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | | | | | | | | | | | [flags] Make program_mode a parameter for commands in vernac. |  Emilio Jesus Gallego Arias | 2017-12-17 |
| | | * | | | | | | | | | | | | | | | | | | [vernac] Split `command.ml` into separate files. | Emilio Jesus Gallego Arias | 2017-12-17 |
| | |/ / / / / / / / / / / / / / / / / / | |||
| | | | * / / / / / / / / / / / / / / / | [doc] Nit on the manual. | Emilio Jesus Gallego Arias | 2017-12-17 |
| | |_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | | | | | Fix build file |  Jim | 2017-12-16 |
| | | | | * | | | | | | | | | | | | | | For bug 6249, Segmentation fault when building Coq on Windows 10. | Jim | 2017-12-16 |
| | | | | | | | | | | | | | | * | | | | Let definitions must not contain side-effects when reaching the kernel. | Pierre-Marie Pédrot | 2017-12-16 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | | | | | [make] More build fixes for static plugins and ocamlfind. | Emilio Jesus Gallego Arias | 2017-12-16 |
| | |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | * | [stm] [ide protocol] Allow to include several commands on query. | Emilio Jesus Gallego Arias | 2017-12-16 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | |||
| | | | * | | | | | | | | | | | | Overlay for unimath. | Gaëtan Gilbert | 2017-12-15 |
| | | | * | | | | | | | | | | | | Do dependencies in 1 command per file class. | Gaëtan Gilbert | 2017-12-15 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |