Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | 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 | ||
| | | | | | | | | | | * | | | Register universe binders for record projections. | 2017-11-24 | ||
| | | | | | | | | | | * | | | Stop exposing UState.universe_context and its Evd wrapper. | 2017-11-24 | ||
| | | | | | | | | | | * | | | Separate checking univ_decls and obtaining universe binder names. | 2017-11-24 | ||
| | | | | | | | | | | * | | | Use Maps and ids for universe binders | 2017-11-24 | ||
| | | | | | | | | | | * | | | Use type Universes.universe_binders. | 2017-11-24 | ||
| |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | Merge PR #6231: Fix link to Recursive Make Considered Harmful | 2017-11-24 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | 2017-11-24 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #486: Make some functions on terms more robust w.r.t new term constr... | 2017-11-24 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | * | | | | | | | Fix deprecated syntax warning from vernacextend.mlp. | 2017-11-24 | ||
* | | | | | | | | | | | | | | | | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | 2017-11-24 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | | coq_makefile tests: build in easily removed temporary subdirectory. | 2017-11-24 | ||
| |_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | Fix coq-makefile ocamldoc call when configured with -annotate. | 2017-11-24 | ||
| |_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | Make byte on gitlab. | 2017-11-24 | ||
| | | | | | | | | | | * | | | Fixing failing mkdir in test-suite for coq-makefile. | 2017-11-24 | ||
* | | | | | | | | | | | | | | Update PR filter used by RM. | 2017-11-24 | ||
* | | | | | | | | | | | | | | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | 2017-11-24 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | Unify style of comments in file CUnix. | 2017-11-23 | ||
| | | | | | | * | | | | | | | Quote file names which have spaces in "Print LoadPath". | 2017-11-23 | ||
| | | | | | | * | | | | | | | Add a function to surround filenames containing a space with quotes. | 2017-11-23 |