| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | * | | | more complete not-fully-applied error messages, #6145 |  Paul Steckler | 2017-11-28 | |
| | | | * | | | | | | | | Add PR backport script. |  Théo Zimmermann | 2017-11-28 | |
| | |_|/ / / / / / / / |/| | | | | | | | | | ||||
| | | | | * | | | | | | [ci] [vst] Shorten compilation time to avoid Travis timeouts. |  Emilio Jesus Gallego Arias | 2017-11-28 | |
| | |_|_|/ / / / / / |/| | | | | | | | | ||||
| | | | | | | | | * | Use safe demarshalling in the checker. |  Pierre-Marie Pédrot | 2017-11-28 | |
| | | | | | | | | * | Use large arrays in the checker demarshaller. | Pierre-Marie Pédrot | 2017-11-28 | |
| | |_|_|_|_|_|_|/ |/| | | | | | | | ||||
| | | | | | * | | | CI: use -byte-only in [warnings] jobs. |  Gaëtan Gilbert | 2017-11-28 | |
| | | | | | * | | | Fix native compute for byte compiled Coq. | Gaëtan Gilbert | 2017-11-28 | |
| | | | * | | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | 2017-11-28 | |
| | |_|/ / / / / |/| | | | | | | ||||
| | | | | * | | | Travis: do not build stdlib in [warnings] jobs. | Gaëtan Gilbert | 2017-11-28 | |
| | |_|_|/ / / |/| | | | | | ||||
| * | | | | | | Merge PR #6259: Add PR merge script. |  Maxime Dénès | 2017-11-28 | |
| |\ \ \ \ \ \ | ||||
| | * | | | | | | Add PR merge script. | Maxime Dénès | 2017-11-28 | |
| * | | | | | | | Merge PR #1033: Universe binder improvements | Maxime Dénès | 2017-11-28 | |
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile. | Maxime Dénès | 2017-11-28 | |
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge PR #6248: [api] Remove aliases of `Evar.t` | Maxime Dénès | 2017-11-28 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; up... | Maxime Dénès | 2017-11-28 | |
| |\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | ||||
| | | | | | | | | | * | allow :: and , as infix ops | Paul Steckler | 2017-11-27 | |
| | | | | | | * | | | | [vernac] Adjust `interp` to pass polymorphic in the attributes. | Emilio Jesus Gallego Arias | 2017-11-27 | |
| | | | | | | * | | | | [vernac] Add polymorphic to the type of vernac interpration options. | Emilio Jesus Gallego Arias | 2017-11-27 | |
| | | | | | | * | | | | [vernac] Start to uniformize type of vernac interpretation. | Emilio Jesus Gallego Arias | 2017-11-27 | |
| | |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| * | | | | | | | | | Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire... | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| * | | | | | | | | | Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6207: [stm] Allow delayed constant in interactive mode. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6241: [lib] Generalize Control.timeout type. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6228: Make byte on gitlab. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6226: Enhance votour | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6041: Protecting the printing of filenames with space | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6227: Linter: do not lint untracked files. | Maxime Dénès | 2017-11-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | | A cosmetic standardization: adding a space in g_constr.ml4. |  Hugo Herbelin | 2017-11-27 | |
| | | | | | | | | | | | | | | | | * | | | Releasing level "11" of "pattern". | Hugo Herbelin | 2017-11-27 | |
| | | | | | | | | | | | | | | | | * | | | Fixing associativity registered for level 10. | Hugo Herbelin | 2017-11-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | | | | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | 2017-11-26 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | Overlay for stronger restrict_universe_context. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | | * | | | Restrict universe context when declaring constants in obligations. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | * | | | | | Updating the current official writing of OCaml, updating Camlp4->Camlp5. | Hugo Herbelin | 2017-11-25 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | | Fix #5347: unify declaration of axioms with and without bound univs. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | * | | | Fix interpretation of global universes in univdecl constraints. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | * | | | Forbid repeated names in universe binders. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | * | | | Universe binders survive sections, modules and compilation. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | * | | | Allow local universe renaming in Print. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | * | | | Make restrict_universe_context stronger. | Gaëtan Gilbert | 2017-11-25 | |
| | | | | | | | | | | | | | * | | | Fix obligations handling of universes anticipating stronger restrict |  Matthieu Sozeau | 2017-11-25 | |
| | | | | | | * | | | | | | | | | | [lib] Generalize Control.timeout type. | Emilio Jesus Gallego Arias | 2017-11-24 | |
| | |_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | Use Evarutil.has_undefined_evars for tactic has_evar. | Gaëtan Gilbert | 2017-11-24 | |
| | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | In close_proof only check univ decls with the restricted context. | Gaëtan Gilbert | 2017-11-24 | |
| | | | | | | | | | | | * | | | Use Entries.constant_universes_entry more. | Gaëtan Gilbert | 2017-11-24 | |
| | | | | | | | | | | | * | | | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert | 2017-11-24 | |
| | | | | | | | | | | | * | | | restrict_universe_context: do not prune named universes. | Gaëtan Gilbert | 2017-11-24 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |