Commit message (Expand) | Author | Age | |
---|---|---|---|
* | [ci] Test coqchk on the CompCert target. | 2017-11-30 | |
* | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts. | 2017-11-30 | |
|\ | |||
* \ | Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in... | 2017-11-30 | |
|\ \ | |||
* \ \ | Merge PR #6271: Add PR backport script. | 2017-11-29 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of... | 2017-11-29 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6199: [vernac] Uniformize type of vernac interpretation. | 2017-11-29 | |
|\ \ \ \ \ | |||
| | | * | | | Add PR backport script. | 2017-11-28 | |
| |_|/ / / |/| | | | | |||
| | | | * | [ci] [vst] Shorten compilation time to avoid Travis timeouts. | 2017-11-28 | |
| |_|_|/ |/| | | | |||
| | | * | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | 2017-11-28 | |
| |_|/ |/| | | |||
* | | | Merge PR #6259: Add PR merge script. | 2017-11-28 | |
|\ \ \ | |||
| * | | | Add PR merge script. | 2017-11-28 | |
* | | | | Merge PR #1033: Universe binder improvements | 2017-11-28 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile. | 2017-11-28 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6248: [api] Remove aliases of `Evar.t` | 2017-11-28 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; up... | 2017-11-28 | |
|\ \ \ \ \ \ \ | |||
| | | | | | * | | [vernac] Adjust `interp` to pass polymorphic in the attributes. | 2017-11-27 | |
| | | | | | * | | [vernac] Add polymorphic to the type of vernac interpration options. | 2017-11-27 | |
| | | | | | * | | [vernac] Start to uniformize type of vernac interpretation. | 2017-11-27 | |
| |_|_|_|_|/ / |/| | | | | | | |||
* | | | | | | | Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire... | 2017-11-27 | |
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | | | |||
* | | | | | | | Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar. | 2017-11-27 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6207: [stm] Allow delayed constant in interactive mode. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6241: [lib] Generalize Control.timeout type. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6228: Make byte on gitlab. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6226: Enhance votour | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6041: Protecting the printing of filenames with space | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6227: Linter: do not lint untracked files. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | * | A cosmetic standardization: adding a space in g_constr.ml4. | 2017-11-27 | |
| | | | | | | | | | | | | | | | * | Releasing level "11" of "pattern". | 2017-11-27 | |
| | | | | | | | | | | | | | | | * | Fixing associativity registered for level 10. | 2017-11-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | | | [api] Remove aliases of `Evar.t` | 2017-11-26 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | * | Overlay for stronger restrict_universe_context. | 2017-11-25 | |
| | | | | | | | | | | | | | * | Restrict universe context when declaring constants in obligations. | 2017-11-25 | |
| | | | | | | | | | | | * | | | Updating the current official writing of OCaml, updating Camlp4->Camlp5. | 2017-11-25 | |
| |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Fix #5347: unify declaration of axioms with and without bound univs. | 2017-11-25 | |
| | | | | | | | | | | | | * | Fix interpretation of global universes in univdecl constraints. | 2017-11-25 | |
| | | | | | | | | | | | | * | Forbid repeated names in universe binders. | 2017-11-25 | |
| | | | | | | | | | | | | * | Universe binders survive sections, modules and compilation. | 2017-11-25 | |
| | | | | | | | | | | | | * | Allow local universe renaming in Print. | 2017-11-25 | |
| | | | | | | | | | | | | * | Make restrict_universe_context stronger. | 2017-11-25 | |
| | | | | | | | | | | | | * | Fix obligations handling of universes anticipating stronger restrict | 2017-11-25 | |
| | | | | | * | | | | | | | | [lib] Generalize Control.timeout type. | 2017-11-24 | |
| |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |||
| | | | | | | | | * | | | | Use Evarutil.has_undefined_evars for tactic has_evar. | 2017-11-24 | |
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | |||
| | | | | | | | | | | * | In close_proof only check univ decls with the restricted context. | 2017-11-24 | |
| | | | | | | | | | | * | Use Entries.constant_universes_entry more. | 2017-11-24 | |
| | | | | | | | | | | * | When declaring constants/inductives use ContextSet if monomorphic. | 2017-11-24 | |
| | | | | | | | | | | * | restrict_universe_context: do not prune named universes. | 2017-11-24 | |
| | | | | | | | | | | * | Fix defining non primitive projections with abstracted universes. | 2017-11-24 |